Trait Iterator

pub trait Iterator: Iterator {
    // Required methods
    fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool;
    fn completed(&mut self) -> bool;
    fn produces_refl(self);
    fn produces_trans(
        a: Self,
        ab: Seq<Self::Item>,
        b: Self,
        bc: Seq<Self::Item>,
        c: Self,
    );

    // Provided method
    fn map_inv<B, F>(self, func: F) -> MapInv<Self, Self::Item, F>
       where Self: Sized,
             F: FnMut(Self::Item, Snapshot<Seq<Self::Item>>) -> B { ... }
}

Required Methods

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

logic(prophetic)

fn completed(&mut self) -> bool

logic(prophetic)

fn produces_refl(self)

law

ensures

self.produces(Seq::EMPTY, self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

law

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

Provided Methods

fn map_inv<B, F>(self, func: F) -> MapInv<Self, Self::Item, F>

where Self: Sized, F: FnMut(Self::Item, Snapshot<Seq<Self::Item>>) -> B,

requires

forall<e : Self::Item, i2 : Self>
                    self.produces(Seq::singleton(e), i2) ==>
                    func.precondition((e, Snapshot::new(Seq::EMPTY)))

requires

MapInv::<Self, _, F>::reinitialize()

requires

MapInv::<Self, Self::Item, F>::preservation(self, func)

ensures

result == MapInv { iter: self, func, produced: Snapshot::new(Seq::EMPTY) }

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementations on Foreign Types

impl<'a, K: DeepModel, V> Iterator for Iter<'a, K, V>

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

logic(prophetic)

// `self@` equals the union of `visited` (viewed as a finite map) and `o@`
pearlite! {
    self@.len() == visited.len() + o@.len()
    && (forall<k: &K, v: &V> visited.contains((k, v))
        ==> self@.get(k.deep_model()) == Some(*v) && o@.get(k.deep_model()) == None)
    && (forall<k: K::DeepModelTy, v: V> o@.get(k) == Some(v)
        ==> self@.get(k) == Some(v) && !exists<k2: &K, v2: &V> k2.deep_model() == k && visited.contains((k2, v2)))
    && (forall<k: K::DeepModelTy, v: V> self@.get(k) == Some(v)
        ==> (exists<k2: &K> k2.deep_model() == k && visited.contains((k2, &v))) || o@.get(k) == Some(v))
    && (forall<i1: Int, i2: Int>
        0 <= i1 && i1 < visited.len() && 0 <= i2 && i2 < visited.len()
        && visited[i1].0.deep_model() == visited[i2].0.deep_model()
        ==> i1 == i2)
}

fn completed(&mut self) -> bool

logic(prophetic)

pearlite! { self.resolve() && self@.is_empty() }

fn produces_refl(self)

law

ensures

self.produces(Seq::EMPTY, self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

law

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<'a, K: DeepModel, V> Iterator for IterMut<'a, K, V>

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

logic(prophetic)

// self@ equals the union of visited (viewed as a fmap) and o@
pearlite! {
    self@.len() == visited.len() + o@.len()
    && (forall<k: K, v: &mut V> visited.contains((&k, v))
        ==> self@.get(k.deep_model()) == Some(v) && o@.get(k.deep_model()) == None)
    && (forall<k: K::DeepModelTy, v: &mut V> o@.get(k) == Some(v)
        ==> self@.get(k) == Some(v) && !exists<k2: &K, v2: &mut V> k2.deep_model() == k && visited.contains((k2, v2)))
    && (forall<k: K::DeepModelTy, v: &mut V> self@.get(k) == Some(v)
        ==> (exists<k1: &K> k1.deep_model() == k && visited.contains((k1, v))) || o@.get(k) == Some(v))
    && (forall<i1: Int, i2: Int>
        0 <= i1 && i1 < visited.len() && 0 <= i2 && i2 < visited.len()
        && visited[i1].0.deep_model() == visited[i2].0.deep_model()
        ==> i1 == i2)
}

fn completed(&mut self) -> bool

logic(prophetic)

pearlite! { self.resolve() && self@.is_empty() }

fn produces_refl(self)

law

ensures

self.produces(Seq::EMPTY, self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

law

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<'a, T> Iterator for Iter<'a, T>

fn completed(&mut self) -> bool

logic(prophetic)

pearlite! { self.resolve() && (*self@)@ == Seq::EMPTY }

fn produces(self, visited: Seq<Self::Item>, tl: Self) -> bool

logic

pearlite! {
    self@.to_ref_seq() == visited.concat(tl@.to_ref_seq())
}

fn produces_refl(self)

law

ensures

self.produces(Seq::EMPTY, self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

law

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<'a, T: DeepModel> Iterator for Iter<'a, T>

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

logic(prophetic)

set_produces(self, visited, o)

fn completed(&mut self) -> bool

logic(prophetic)

pearlite! { (self@).is_empty() }

fn produces_refl(self)

law

ensures

self.produces(Seq::EMPTY, self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

law

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<'a, T: Eq + Hash + DeepModel, S: BuildHasher> Iterator for Difference<'a, T, S>

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

logic(prophetic)

set_produces(self, visited, o)

fn completed(&mut self) -> bool

logic(prophetic)

pearlite! { self.resolve() && (self@).is_empty() }

fn produces_refl(self)

law

ensures

self.produces(Seq::EMPTY, self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

law

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<'a, T: Eq + Hash + DeepModel, S: BuildHasher> Iterator for Intersection<'a, T, S>

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

logic(prophetic)

set_produces(self, visited, o)

fn completed(&mut self) -> bool

logic(prophetic)

pearlite! { self.resolve() && (self@).is_empty() }

fn produces_refl(self)

law

ensures

self.produces(Seq::EMPTY, self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

law

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<I: Iterator + ?Sized> Iterator for &mut I

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

logic(prophetic)

pearlite! { (*self).produces(visited, *o) && ^self == ^o }

fn completed(&mut self) -> bool

logic(prophetic)

pearlite! { (*self).completed() && ^*self == ^^self }

fn produces_refl(self)

law

ensures

self.produces(Seq::EMPTY, self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

law

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<K: DeepModel, V> Iterator for IntoIter<K, V>

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

logic(prophetic)

// self@ equals the union of visited (viewed as a fmap) and o@
pearlite! {
    self@.len() == visited.len() + o@.len()
    && (forall<k: K, v: V> visited.contains((k, v))
        ==> self@.get(k.deep_model()) == Some(v) && o@.get(k.deep_model()) == None)
    && (forall<k: K::DeepModelTy, v: V> o@.get(k) == Some(v)
        ==> self@.get(k) == Some(v) && !exists<k2: K, v2: V> k2.deep_model() == k && visited.contains((k2, v2)))
    && (forall<k: K::DeepModelTy, v: V> self@.get(k) == Some(v)
        ==> (exists<k1: K> k1.deep_model() == k && visited.contains((k1, v))) || o@.get(k) == Some(v))
    && (forall<i1: Int, i2: Int>
        0 <= i1 && i1 < visited.len() && 0 <= i2 && i2 < visited.len()
        && visited[i1].0.deep_model() == visited[i2].0.deep_model()
        ==> i1 == i2)
}

fn completed(&mut self) -> bool

logic(prophetic)

pearlite! { self.resolve() && self@.is_empty() }

fn produces_refl(self)

law

ensures

self.produces(Seq::EMPTY, self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

law

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<T, const N: usize> Iterator for IntoIter<T, N>

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

logic(prophetic)

pearlite! { self@ == visited.concat(o@) }

fn completed(&mut self) -> bool

logic(prophetic)

pearlite! { self.resolve() && self@ == Seq::EMPTY }

fn produces_refl(self)

law

ensures

self.produces(Seq::EMPTY, self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

law

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

impl<T: DeepModel> Iterator for IntoIter<T>

fn produces(self, visited: Seq<Self::Item>, o: Self) -> bool

logic(prophetic)

set_produces(self, visited, o)

fn completed(&mut self) -> bool

logic(prophetic)

pearlite! { (self@).is_empty() }

fn produces_refl(self)

law

ensures

self.produces(Seq::EMPTY, self)

fn produces_trans( a: Self, ab: Seq<Self::Item>, b: Self, bc: Seq<Self::Item>, c: Self, )

law

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

a.produces(ab.concat(bc), c)

Implementors

impl<'a, I, T> Iterator for Cloned<I>

where I: Iterator<Item = &'a T>, T: Clone + 'a,

impl<'a, I, T> Iterator for Copied<I>

where I: Iterator<Item = &'a T>, T: Copy + 'a,

impl<'a, T> Iterator for creusot_contracts::std::slice::Iter<'a, T>

impl<'a, T> Iterator for creusot_contracts::std::slice::IterMut<'a, T>

impl<A: Iterator, B: Iterator> Iterator for Zip<A, B>

impl<B, I, F> Iterator for Map<I, F>

where I: Iterator, Self: Iterator<Item = B>, F: FnMut(I::Item) -> B,

impl<I> Iterator for Enumerate<I>

where I: Iterator,

impl<I, B, F> Iterator for FilterMap<I, F>

where I: Iterator, F: FnMut(I::Item) -> Option<B>,

impl<I, F> Iterator for Filter<I, F>

where I: Iterator, F: FnMut(&I::Item) -> bool,

impl<I: DoubleEndedIterator> Iterator for Rev<I>

impl<I: Iterator> Iterator for Fuse<I>

impl<I: Iterator> Iterator for Skip<I>

impl<I: Iterator> Iterator for Take<I>

impl<I: Iterator, B, F: FnMut(I::Item, Snapshot<Seq<I::Item>>) -> B> Iterator for MapInv<I, I::Item, F>

impl<Idx: DeepModel<DeepModelTy = Int> + Step> Iterator for Range<Idx>

impl<Idx: DeepModel<DeepModelTy = Int> + Step> Iterator for RangeInclusive<Idx>

impl<T> Iterator for creusot_contracts::std::option::IntoIter<T>

impl<T> Iterator for creusot_contracts::std::option::Iter<'_, T>

impl<T> Iterator for creusot_contracts::std::option::IterMut<'_, T>

impl<T> Iterator for Empty<T>

impl<T> Iterator for Once<T>

impl<T, A: Allocator> Iterator for creusot_contracts::std::vec::IntoIter<T, A>

impl<T: Clone> Iterator for Repeat<T>