Skip to main content

ExIterator

vstd::std_specs::iter

Trait ExIterator 

Source 
pub trait ExIterator {
    type ExternalTraitSpecificationFor: Iterator;
    type Item;

    // Required methods
    spec fn obeys_prophetic_iter_laws(&self) -> bool;
    spec fn remaining(&self) -> Seq<Self::Item>;
    spec fn will_return_none(&self) -> bool;
    exec fn next(&mut self) -> ret : Option<Self::Item>;
    spec fn decrease(&self) -> Option<nat>;
    spec fn initial_value_relation(&self, init: &Self) -> bool;
    spec fn peek(&self, index: int) -> Option<Self::Item>;
    exec fn rev(self) -> r : Rev<Self>
       where Self: Sized;
    exec fn collect<B>(self) -> collection : B
       where B: FromIterator<Self::Item>,
             Self: Sized;
}

Required Associated Types§

Source

type ExternalTraitSpecificationFor: Iterator

Source

type Item

Required Methods§

Source

spec fn obeys_prophetic_iter_laws(&self) -> bool

This iterator obeys the specifications below on next, expressed in terms of prophetic spec functions. Only iterators that terminate (i.e., eventually return None and then continue to return None) should use this interface.

Source

spec fn remaining(&self) -> Seq<Self::Item>

Sequence of items that will (eventually) be returned

Source

spec fn will_return_none(&self) -> bool

Does this iterator complete with a None after the above sequence? (As opposed to hanging indefinitely on a next() call) Trivially true for most iterators but important for iterators that apply an exec closure that may not terminate.

Source

exec fn next(&mut self) -> ret : Option<Self::Item>

ensures
final(self).obeys_prophetic_iter_laws() == old(self).obeys_prophetic_iter_laws(),
final(self).obeys_prophetic_iter_laws()
    ==> final(self).will_return_none() == old(self).will_return_none(),
final(self).obeys_prophetic_iter_laws()
    ==> (old(self).decrease() is Some <==> final(self).decrease() is Some),
final(self).obeys_prophetic_iter_laws()
    ==> ({
        if old(self).remaining().len() > 0 {
            &&& final(self).remaining() == old(self).remaining().drop_first()
            &&& ret == Some(old(self).remaining()[0])

        } else {
            final(self).remaining() == old(self).remaining() && ret == None
                && final(self).will_return_none()
        }
    }),
final(self).obeys_prophetic_iter_laws() && old(self).remaining().len() > 0
    && final(self).decrease() is Some
    ==> decreases_to!(old(self).decrease() -> 0 => final(self).decrease() -> 0),

Advances the iterator and returns the next value.

Source

spec fn decrease(&self) -> Option<nat>

Value used by default for the decreases clause when no explicit decreases clause is provided (the user can override this with an explicit decreases clause). If there’s no appropriate metric to decrease, this can return None, and the user will have to provide an explicit decreases clause.

Source

spec fn initial_value_relation(&self, init: &Self) -> bool

Invariant relating the iterator to the initial expression that created it (e.g., my_vec.iter()). This allows for more ergonomic/intuitive invariants. When the analysis can infer a spec initial value (by discovering a when_used_as_spec annotation), the analysis places the value in init.

Source

spec fn peek(&self, index: int) -> Option<Self::Item>

Source

exec fn rev(self) -> r : Rev<Self>
where Self: Sized,

Source

exec fn collect<B>(self) -> collection : B
where B: FromIterator<Self::Item>, Self: Sized,

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.

Implementors§