Trait IteratorSpec 

pub trait IteratorSpec: 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, 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)

logic(law, prophetic)

ensures

self.produces(Seq::empty(), self)

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

logic(law, prophetic)

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, F>

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

ghost

requires

forall<e, i2> self.produces(Seq::singleton(e), i2) && inv(e) ==>
     func.precondition((e, Snapshot::new(Seq::empty())))

requires

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

requires

MapInv::<Self, 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".

Implementations on Foreign Types

impl<'a, I: IteratorSpec<Item = &'a T>, T: Clone + 'a> IteratorSpec for Cloned<I>

fn completed(&mut self) -> bool

logic(open, prophetic)

exists<inner: &mut _> *inner == self.iter() && ^inner == (^self).iter() && inner.completed()

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

logic(open, prophetic)

exists<s: Seq<&'a T>>
       self.iter().produces(s, o.iter())
    && visited.len() == s.len()
    && forall<i> 0 <= i && i < s.len() ==> T::clone.postcondition((s[i],), visited[i])

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<'a, I: IteratorSpec<Item = &'a T>, T: Copy + 'a> IteratorSpec for Copied<I>

fn completed(&mut self) -> bool

logic(open, prophetic)

exists<inner: &mut _> *inner == self.iter() && ^inner == (^self).iter() && inner.completed()

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

logic(open, prophetic)

exists<s: Seq<&'a T>>
       self.iter().produces(s, o.iter())
    && visited.len() == s.len()
    && forall<i> 0 <= i && i < s.len() ==> visited[i] == *s[i]

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

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

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

logic(open, prophetic, inline)

/* Macro-generated */

fn completed(&mut self) -> bool

logic(open, prophetic)

resolve(self) && self@.is_empty()

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

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

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

logic(open, prophetic, inline)

/* Macro-generated */

fn completed(&mut self) -> bool

logic(open, prophetic)

resolve(self) && self@.is_empty()

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

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

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

logic(open, prophetic)

set_produces(self, visited, o)

fn completed(&mut self) -> bool

logic(open, prophetic)

(self@).is_empty()

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(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> IteratorSpec for Difference<'a, T, S>

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

logic(open, prophetic)

set_produces(self, visited, o)

fn completed(&mut self) -> bool

logic(open, prophetic)

resolve(self) && (self@).is_empty()

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(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> IteratorSpec for Intersection<'a, T, S>

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

logic(open, prophetic)

set_produces(self, visited, o)

fn completed(&mut self) -> bool

logic(open, prophetic)

resolve(self) && (self@).is_empty()

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

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

fn completed(&mut self) -> bool

logic(open, prophetic)

resolve(self) && (*self@)@ == Seq::empty()

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

logic(open)

self@.to_ref_seq() == visited.concat(tl@.to_ref_seq())

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

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

fn completed(&mut self) -> bool

logic(open, prophetic)

resolve(self) && self@ == Seq::empty()

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

logic(open)

self@ == visited.concat(tl@)

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<'a, T> IteratorSpec for IterMut<'a, T>

fn completed(&mut self) -> bool

logic(open, prophetic)

resolve(self) && (*self@)@ == Seq::empty()

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

logic(open)

self@.to_mut_seq() == visited.concat(tl@.to_mut_seq())

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<A: IteratorSpec, B: IteratorSpec<Item = A::Item>> IteratorSpec for Chain<A, B>

fn completed(&mut self) -> bool

logic(open, prophetic)

/* Macro-generated */

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

logic(open, prophetic, inline)

exists<visited_a: Seq<A::Item>, visited_b: Seq<B::Item>>
    visited == visited_a.concat(visited_b) &&
    chain_produces_inner(self, visited_a, visited_b, o)

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

fn produces_trans( x: Self, xy: Seq<Self::Item>, y: Self, yz: Seq<Self::Item>, z: Self, )

logic(law, prophetic)

requires

x.produces(xy, y)

requires

y.produces(yz, z)

ensures

x.produces(xy.concat(yz), z)

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

fn completed(&mut self) -> bool

logic(open, prophetic)

exists<a: &mut A, b: &mut B>
       *a == (*self).iter_a() && *b == (*self).iter_b()
    && ^a == (^self).iter_a() && ^b == (^self).iter_b()
    && (a.completed() && resolve(b)
        || exists<x: A::Item> inv(x) && (*a).produces(Seq::singleton(x), ^a) &&
                              resolve(x) && (*b).completed())

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

logic(open, prophetic)

exists<p1: Seq<_>, p2: Seq<_>>
       p1.len() == p2.len() && p2.len() == visited.len()
    && (forall<i> 0 <= i && i < visited.len() ==> visited[i] == (p1[i], p2[i]))
    && self.iter_a().produces(p1, o.iter_a()) && self.iter_b().produces(p2, o.iter_b())

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<I: DoubleEndedIteratorSpec> IteratorSpec for Rev<I>

fn completed(&mut self) -> bool

logic(open, prophetic)

self.iter_mut().completed_back()

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

logic(open, prophetic)

self.iter().produces_back(visited, o.iter())

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

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

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

logic(open, prophetic)

(*self).produces(visited, *o) && ^self == ^o

fn completed(&mut self) -> bool

logic(open, prophetic)

(*self).completed() && ^*self == ^^self

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<I: IteratorSpec, B, F: FnMut(I::Item) -> B> IteratorSpec for Map<I, F>

fn completed(&mut self) -> bool

logic(open, prophetic)

(exists<inner: &mut _> *inner == self.iter() && ^inner == (^self).iter() && inner.completed())
&& (*self).func() == (^self).func()

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

logic(open, prophetic, inline)

/* Macro-generated */

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<I: IteratorSpec, B, F: FnMut(I::Item) -> Option<B>> IteratorSpec for FilterMap<I, F>

fn completed(&mut self) -> bool

logic(open, prophetic)

(exists<s: Seq<_>, e: &mut I > self.iter().produces(s, *e) && e.completed() &&
    forall<i> 0 <= i && i < s.len() ==> (*self).func().postcondition_mut((s[i],), (^self).func(), None))
&& (*self).func() == (^self).func()

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

logic(open, prophetic)

/* Macro-generated */

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<I: IteratorSpec, F: FnMut(&I::Item) -> bool> IteratorSpec for Filter<I, F>

fn completed(&mut self) -> bool

logic(open, prophetic)

(exists<s: Seq<_>, e: &mut I > self.iter().produces(s, *e) && e.completed() &&
    forall<i> 0 <= i && i < s.len() ==> (*self).func().postcondition_mut((&s[i],), (^self).func(), false))
&& (*self).func() == (^self).func()

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

logic(open, prophetic)

/* Macro-generated */

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<I: IteratorSpec> IteratorSpec for Enumerate<I>

fn completed(&mut self) -> bool

logic(open, prophetic)

exists<inner: &mut _> *inner == self.iter() && ^inner == (^self).iter()
    && inner.completed()
    && self.n()@ == (^self).n()@

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

logic(open, prophetic)

visited.len() == o.n()@ - self.n()@
&& exists<s: Seq<I::Item>>
       self.iter().produces(s, o.iter())
    && visited.len() == s.len()
    && forall<i> 0 <= i && i < s.len() ==> visited[i].0@ == self.n()@ + i && visited[i].1 == s[i]

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<I: IteratorSpec> IteratorSpec for Fuse<I>

fn completed(&mut self) -> bool

logic(open, prophetic)

(self@ == None || exists<it:&mut I> it.completed() && self@ == Some(*it)) &&
(^self)@ == None

fn produces(self, prod: Seq<Self::Item>, other: Self) -> bool

logic(open, prophetic)

/* Macro-generated */

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<I: IteratorSpec> IteratorSpec for Skip<I>

fn completed(&mut self) -> bool

logic(open, prophetic)

/* Macro-generated */

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

logic(open, prophetic)

visited == Seq::empty() && self == o ||
o.n()@ == 0 && visited.len() > 0 &&
exists<s: Seq<Self::Item>>
       s.len() == self.n()@
    && self.iter().produces(s.concat(visited), o.iter())
    && forall<i> 0 <= i && i < s.len() ==> resolve(s[i])

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<I: IteratorSpec> IteratorSpec for Take<I>

fn completed(&mut self) -> bool

logic(open, prophetic)

self.n()@ == 0 && resolve(self) ||
(*self).n()@ > 0 && (*self).n()@ == (^self).n()@ + 1 && self.iter_mut().completed()

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

logic(open, prophetic)

self.n()@ == o.n()@ + visited.len() && self.iter().produces(visited, o.iter())

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

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

Available on crate feature nightly only.

fn completed(&mut self) -> bool

logic(open, prophetic)

resolve(self) && self.start.deep_model() >= self.end.deep_model()

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

logic(open)

self.end == o.end && self.start.deep_model() <= o.start.deep_model()
&& (visited.len() > 0 ==> o.start.deep_model() <= o.end.deep_model())
&& visited.len() == o.start.deep_model() - self.start.deep_model()
&& forall<i> 0 <= i && i < visited.len() ==>
    visited[i].deep_model() == self.start.deep_model() + i

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

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

Available on crate feature nightly only.

fn completed(&mut self) -> bool

logic(open, prophetic)

self.is_empty_log() && (^self).is_empty_log()

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

logic(open)

visited.len() == range_inclusive_len(self) - range_inclusive_len(o) &&
(self.is_empty_log() ==> o.is_empty_log()) &&
(o.is_empty_log() || self.end_log() == o.end_log()) &&
forall<i> 0 <= i && i < visited.len() ==>
    visited[i].deep_model() == self.start_log().deep_model() + i

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<K: DeepModel, V, A: Allocator> IteratorSpec for IntoIter<K, V, A>

Available on crate feature nightly only.

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

logic(open, prophetic, inline)

/* Macro-generated */

fn completed(&mut self) -> bool

logic(open, prophetic)

resolve(self) && self@.is_empty()

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<T, A: Allocator> IteratorSpec for IntoIter<T, A>

Available on crate feature nightly only.

fn completed(&mut self) -> bool

logic(open, prophetic)

resolve(self) && self@ == Seq::empty()

fn produces(self, visited: Seq<T>, rhs: Self) -> bool

logic(open)

self@ == visited.concat(rhs@)

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

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

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

logic(open, prophetic)

self@ == visited.concat(o@)

fn completed(&mut self) -> bool

logic(open, prophetic)

resolve(self) && self@ == Seq::empty()

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

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

fn completed(&mut self) -> bool

logic(open)

false

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

logic(open, prophetic)

self == o &&
forall<i> 0 <= i && i < visited.len() ==> T::clone.postcondition((&self@,), visited[i])

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<T: DeepModel, A: Allocator> IteratorSpec for IntoIter<T, A>

Available on crate feature nightly only.

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

logic(open, prophetic)

set_produces(self, visited, o)

fn completed(&mut self) -> bool

logic(open, prophetic)

(self@).is_empty()

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<T> IteratorSpec for Empty<T>

fn completed(&mut self) -> bool

logic(open, prophetic)

resolve(self)

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

logic(open)

visited == Seq::empty() && self == o

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<T> IteratorSpec for IntoIter<T>

fn completed(&mut self) -> bool

logic(open, prophetic)

(*self)@ == None && resolve(self)

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

logic(open)

visited == Seq::empty() && self == o ||
exists<e: Self::Item> self@ == Some(e) && visited == Seq::singleton(e) && o@ == None

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<T> IteratorSpec for Iter<'_, T>

fn completed(&mut self) -> bool

logic(open, prophetic)

(*self)@ == None && resolve(self)

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

logic(open)

visited == Seq::empty() && self == o ||
exists<e: Self::Item> self@ == Some(e) && visited == Seq::singleton(e) && o@ == None

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<T> IteratorSpec for IterMut<'_, T>

fn completed(&mut self) -> bool

logic(open, prophetic)

(*self)@ == None && resolve(self)

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

logic(open)

visited == Seq::empty() && self == o ||
exists<e: Self::Item> self@ == Some(e) && visited == Seq::singleton(e) && o@ == None

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<T> IteratorSpec for Once<T>

fn completed(&mut self) -> bool

logic(open, prophetic)

(*self)@ == None && resolve(self)

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

logic(open, prophetic)

visited == Seq::empty() && self == o ||
exists<e: Self::Item> self@ == Some(e) && visited == Seq::singleton(e) && o@ == None

fn produces_refl(self)

logic(law)

ensures

self.produces(Seq::empty(), self)

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

logic(law)

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

Implementors

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

impl<K, V> IteratorSpec for creusot_std::logic::fmap::Iter<K, V>

impl<T> IteratorSpec for creusot_std::logic::seq::Iter<T>