Trait DoubleEndedIteratorSpec 

pub trait DoubleEndedIteratorSpec: DoubleEndedIterator + IteratorSpec {
    // Required methods
    fn produces_back(self, visited: Seq<Self::Item>, o: Self) -> bool;
    fn completed_back(&mut self) -> bool;
    fn produces_back_refl(self);
    fn produces_back_trans(
        a: Self,
        ab: Seq<Self::Item>,
        b: Self,
        bc: Seq<Self::Item>,
        c: Self,
    );
    fn size_hint_back_spec(&self, r: (usize, Option<usize>));
}

Required Methods

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

logic(prophetic)

fn completed_back(&mut self) -> bool

logic(prophetic)

fn produces_back_refl(self)

logic(law, prophetic)

ensures

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

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

logic(law, prophetic)

requires

a.produces_back(ab, b)

requires

b.produces_back(bc, c)

ensures

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

fn size_hint_back_spec(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

forall<s: Seq<Self::Item>, i: &mut Self>
    self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len()

ensures

match r.1 {
    Some(r) => {
        forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
    }
    None => true
}

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, T> DoubleEndedIteratorSpec for Iter<'a, T>

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

logic(open)

self@.to_ref_seq() == o@.to_ref_seq().concat(visited.reverse())

fn completed_back(&mut self) -> bool

logic(open, prophetic)

self.completed()

fn produces_back_refl(self)

logic(law)

ensures

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

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

logic(law)

requires

a.produces_back(ab, b)

requires

b.produces_back(bc, c)

ensures

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

fn size_hint_back_spec(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

forall<s: Seq<Self::Item>, i: &mut Self>
    self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len()

ensures

match r.1 {
    Some(r) => {
        forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
    }
    None => true
}

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

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

logic(open)

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

fn completed_back(&mut self) -> bool

logic(open, prophetic)

self.completed()

fn produces_back_refl(self)

logic(law)

ensures

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

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

logic(law)

requires

a.produces_back(ab, b)

requires

b.produces_back(bc, c)

ensures

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

fn size_hint_back_spec(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

forall<s: Seq<Self::Item>, i: &mut Self>
    self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len()

ensures

match r.1 {
    Some(r) => {
        forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
    }
    None => true
}

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

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

logic(open)

self@.to_mut_seq() == o@.to_mut_seq().concat(visited.reverse())

fn completed_back(&mut self) -> bool

logic(open, prophetic)

self.completed()

fn produces_back_refl(self)

logic(law)

ensures

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

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

logic(law)

requires

a.produces_back(ab, b)

requires

b.produces_back(bc, c)

ensures

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

fn size_hint_back_spec(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

forall<s: Seq<Self::Item>, i: &mut Self>
    self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len()

ensures

match r.1 {
    Some(r) => {
        forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
    }
    None => true
}

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

fn completed_back(&mut self) -> bool

logic(open, prophetic)

/* Macro-generated */

fn produces_back(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_b.concat(visited_a) &&
    chain_produces_inner_back(self, visited_a, visited_b, o)

fn produces_back_refl(self)

logic(law)

ensures

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

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

logic(law, prophetic)

requires

x.produces_back(xy, y)

requires

y.produces_back(yz, z)

ensures

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

fn size_hint_back_spec(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

forall<s: Seq<Self::Item>, i: &mut Self>
    self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len()

ensures

match r.1 {
    Some(r) => {
        forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
    }
    None => true
}

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

fn completed_back(&mut self) -> bool

logic(open, prophetic)

self.iter_mut().completed()

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

logic(open, prophetic)

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

fn produces_back_refl(self)

logic(law)

ensures

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

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

logic(law)

requires

a.produces_back(ab, b)

requires

b.produces_back(bc, c)

ensures

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

fn size_hint_back_spec(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

forall<s: Seq<Self::Item>, i: &mut Self>
    self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len()

ensures

match r.1 {
    Some(r) => {
        forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
    }
    None => true
}

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

Available on crate feature nightly only.

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

logic(open)

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

fn completed_back(&mut self) -> bool

logic(open, prophetic)

self.completed()

fn produces_back_refl(self)

logic(law)

ensures

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

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

logic(law)

requires

a.produces_back(ab, b)

requires

b.produces_back(bc, c)

ensures

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

fn size_hint_back_spec(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

forall<s: Seq<Self::Item>, i: &mut Self>
    self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len()

ensures

match r.1 {
    Some(r) => {
        forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
    }
    None => true
}

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

Available on crate feature nightly only.

fn produces_back(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.start_log() == o.start_log()) &&
forall<i> 0 <= i && i < visited.len() ==>
    visited[i].deep_model() == self.end_log().deep_model() - i

fn completed_back(&mut self) -> bool

logic(open, prophetic)

self.completed()

fn produces_back_refl(self)

logic(law)

ensures

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

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

logic(law)

requires

a.produces_back(ab, b)

requires

b.produces_back(bc, c)

ensures

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

fn size_hint_back_spec(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

forall<s: Seq<Self::Item>, i: &mut Self>
    self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len()

ensures

match r.1 {
    Some(r) => {
        forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
    }
    None => true
}

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

Available on crate feature nightly only.

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

logic(open)

self@ == rhs@.concat(visited.reverse())

fn completed_back(&mut self) -> bool

logic(open, prophetic)

self.completed()

fn produces_back_refl(self)

logic(law)

ensures

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

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

logic(law)

requires

a.produces_back(ab, b)

requires

b.produces_back(bc, c)

ensures

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

fn size_hint_back_spec(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

forall<s: Seq<Self::Item>, i: &mut Self>
    self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len()

ensures

match r.1 {
    Some(r) => {
        forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
    }
    None => true
}

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

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

logic(open)

self@ == o@.concat(visited.reverse())

fn completed_back(&mut self) -> bool

logic(open, prophetic)

self.completed()

fn produces_back_refl(self)

logic(law)

ensures

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

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

logic(law)

requires

a.produces_back(ab, b)

requires

b.produces_back(bc, c)

ensures

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

fn size_hint_back_spec(&self, r: (usize, Option<usize>))

logic(law)

requires

Self::size_hint.postcondition((self,), r)

ensures

forall<s: Seq<Self::Item>, i: &mut Self>
    self.produces_back(s, *i) && i.completed_back() ==> r.0@ <= s.len()

ensures

match r.1 {
    Some(r) => {
        forall<s: Seq<Self::Item>, i: Self> self.produces_back(s, i) ==> s.len() <= r@
    }
    None => true
}

Implementors