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)

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)

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,

terminates

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", so this trait is not object safe.

Implementations on Foreign Types

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

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

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, T> IteratorSpec for Copied<I>

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

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(open, law)

/* Macro-generated */

ensures

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

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

logic(open, law)

proof_assert! { forall<i> 0 <= i && i < bc.len() ==> bc[i] == ab.concat(bc)[ab.len() + i] }

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(open, law)

/* Macro-generated */

ensures

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

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

logic(open, law)

proof_assert! { forall<i> 0 <= i && i < bc.len() ==> bc[i] == ab.concat(bc)[ab.len() + i] }

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(open, law)

/* Macro-generated */

ensures

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

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

logic(open, law)

/* Macro-generated */

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(open, law)

/* Macro-generated */

ensures

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

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

logic(open, law)

/* Macro-generated */

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(open, law)

/* Macro-generated */

ensures

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

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

logic(open, law)

/* Macro-generated */

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(open, law)

/* Macro-generated */

ensures

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

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

logic(open, law)

set_produces_trans(a, ab, b, bc, c);

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(open, law)

/* Macro-generated */

ensures

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

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

logic(open, law)

set_produces_trans(a, ab, b, bc, c);

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(open, law)

/* Macro-generated */

ensures

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

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

logic(open, law)

set_produces_trans(a, ab, b, bc, c);

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

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).itera() && *b == (*self).iterb()
    && ^a == (^self).itera() && ^b == (^self).iterb()
    && (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.itera().produces(p1, o.itera()) && self.iterb().produces(p2, o.iterb())

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()

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(open, law)

/* Macro-generated */

ensures

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

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

logic(open, law)

/* Macro-generated */

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(open, law)

/* Macro-generated */

ensures

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

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

logic(open, law)

/* Macro-generated */

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<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, 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, 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<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(open, law)

/* Macro-generated */

ensures

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

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

logic(open, law)

/* Macro-generated */

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(open, law)

/* Macro-generated */

ensures

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

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

logic(open, law)

proof_assert! { forall<i> 0 <= i && i < bc.len() ==> bc[i] == ab.concat(bc)[ab.len() + i] }

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<Self::Item>, 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<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)

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, 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(open, law)

/* Macro-generated */

ensures

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

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

logic(open, law)

/* Macro-generated */

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<Self::Item>, 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(open, law)

/* Macro-generated */

ensures

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

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

logic(open, law)

/* Macro-generated */

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

impl<T: DeepModel> IteratorSpec for IntoIter<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(open, law)

/* Macro-generated */

ensures

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

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

logic(open, law)

set_produces_trans(a, ab, b, bc, c);

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)

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)

Implementors

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

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

impl<K, V> IteratorSpec for FMap<K, V>

impl<T> IteratorSpec for SeqIter<T>