Trait creusot_contracts::std::slice::SliceIndex

source · 
pub trait SliceIndex<T>: SliceIndex<T>
where
    T: View + ?Sized,
{
    // Required methods
    fn in_bounds(self, seq: T::ViewTy) -> bool;
    fn has_value(self, seq: T::ViewTy, out: Self::Output) -> bool;
    fn resolve_elswhere(self, old: T::ViewTy, fin: T::ViewTy) -> bool;
}

Required Methods§

source

fn in_bounds(self, seq: T::ViewTy) -> bool

logic

source

fn has_value(self, seq: T::ViewTy, out: Self::Output) -> bool

logic

source

fn resolve_elswhere(self, old: T::ViewTy, fin: T::ViewTy) -> bool

logic

Implementations on Foreign Types§

source§

impl<T> SliceIndex<[T]> for usize

source§

fn in_bounds(self, seq: Seq<T>) -> bool

logic 

pearlite! { self@ < seq.len() }

source§

fn has_value(self, seq: Seq<T>, out: T) -> bool

logic 

pearlite! { seq[self@] == out }

source§

fn resolve_elswhere(self, old: Seq<T>, fin: Seq<T>) -> bool

logic

pearlite! { forall<i : Int> 0 <= i && i != self@ && i < old.len() ==> old[i] == fin[i] }

Implementors§