Trait creusot_contracts::std::iter::Iterator

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

law

ensures

self.produces(Seq::EMPTY, self)

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

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

where Self: Sized, F: FnMut(Self::Item, Snapshot<Seq<Self::Item>>) -> B,

requires

forall<e : Self::Item, i2 : Self>
                    self.produces(Seq::singleton(e), i2) ==>
                    func.precondition((e, Snapshot::new(Seq::EMPTY)))

requires

MapInv::<Self, _, F>::reinitialize()

requires

MapInv::<Self, Self::Item, F>::preservation(self, func)

ensures

result == MapInv { iter: self, func, produced: Snapshot::new(Seq::EMPTY) }

Object Safety

This trait is not object safe.

Implementations on Foreign Types

impl<I: Iterator + ?Sized> Iterator for &mut I

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

logic(prophetic)

pearlite! { (*self).produces(visited, *o) && ^self == ^o }

fn completed(&mut self) -> bool

logic(prophetic)

pearlite! { (*self).completed() && ^*self == ^^self }

fn produces_refl(self)

law

ensures

self.produces(Seq::EMPTY, self)

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

law

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

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

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

logic(prophetic)

pearlite! { self@ == visited.concat(o@) }

fn completed(&mut self) -> bool

logic(prophetic)

pearlite! { self.resolve() && self@ == Seq::EMPTY }

fn produces_refl(self)

law

ensures

self.produces(Seq::EMPTY, self)

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

law

requires

a.produces(ab, b)

requires

b.produces(bc, c)

ensures

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

Implementors

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

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

impl<'a, I, T> Iterator for Copied<I>

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

impl<'a, T> Iterator for creusot_contracts::std::collections::vec_deque::Iter<'a, T>

impl<'a, T> Iterator for creusot_contracts::std::option::Iter<'a, T>

impl<'a, T> Iterator for creusot_contracts::std::option::IterMut<'a, T>

impl<'a, T> Iterator for creusot_contracts::std::slice::Iter<'a, T>

impl<'a, T> Iterator for creusot_contracts::std::slice::IterMut<'a, T>

impl<A: Iterator, B: Iterator> Iterator for Zip<A, B>

impl<B, I, F> Iterator for Map<I, F>

where I: Iterator, Self: Iterator<Item = B>, F: FnMut(I::Item) -> B,

impl<I> Iterator for Enumerate<I>

where I: Iterator,

impl<I, F> Iterator for Filter<I, F>

where I: Iterator, F: FnMut(&I::Item) -> bool,

impl<I: Iterator> Iterator for Fuse<I>

impl<I: Iterator> Iterator for Skip<I>

impl<I: Iterator> Iterator for Take<I>

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

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

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

impl<T> Iterator for creusot_contracts::std::option::IntoIter<T>

impl<T> Iterator for Empty<T>

impl<T> Iterator for Once<T>

impl<T, A: Allocator> Iterator for creusot_contracts::std::vec::IntoIter<T, A>

impl<T: Clone> Iterator for Repeat<T>