pub trait IteratorSpec: Iterator {
// Required methods
spec fn obeys_prophetic_iter_laws(&self) -> bool;
spec fn remaining(&self) -> Seq<Self::Item>;
spec fn will_return_none(&self) -> bool;
spec fn decrease(&self) -> Option<nat>;
spec fn initial_value_relation(&self, init: &Self) -> bool;
spec fn peek(&self, index: int) -> Option<Self::Item>;
}Required Methods§
Sourcespec fn obeys_prophetic_iter_laws(&self) -> bool
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.
Sourcespec fn remaining(&self) -> Seq<Self::Item>
spec fn remaining(&self) -> Seq<Self::Item>
Sequence of items that will (eventually) be returned
Sourcespec fn will_return_none(&self) -> bool
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.
Sourcespec fn decrease(&self) -> Option<nat>
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.
Sourcespec fn initial_value_relation(&self, init: &Self) -> bool
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.
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.