Trait DoubleEndedIteratorSpec 

pub trait DoubleEndedIteratorSpec: DoubleEndedIterator + IteratorSpec {
    // Required methods
    fn produces_back(self, visited: Seq<Self::Item>, o: 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,
    );
}

Required Methods

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

logic(prophetic)

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)

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

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)

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

logic(open, law)

/* Macro-generated */

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

/* Macro-generated */

requires

a.produces_back(ab, b)

requires

b.produces_back(bc, c)

ensures

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

Implementors