Trait SliceIndexSpec 

pub trait SliceIndexSpec<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

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

Implementations on Foreign Types

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

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

(open, inline)

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

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

(open, inline)

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

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

(open, inline)

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

impl<T> SliceIndexSpec<[T]> for Range<usize>

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

(open)

pearlite! { self.start@ <= self.end@ && self.end@ <= seq.len() }

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

(open)

pearlite! { seq.subsequence(self.start@, self.end@) == out@ }

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

(open)

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

impl<T> SliceIndexSpec<[T]> for RangeFrom<usize>

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

(open)

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

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

(open)

pearlite! { seq.subsequence(self.start@, seq.len()) == out@ }

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

(open)

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

impl<T> SliceIndexSpec<[T]> for RangeFull

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

(open)

pearlite! { true }

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

(open)

pearlite! { seq == out@ }

fn resolve_elswhere(self, _old: Seq<T>, _fin: Seq<T>) -> bool

(open)

pearlite! { true }

impl<T> SliceIndexSpec<[T]> for RangeInclusive<usize>

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

(opaque)

ensures

self.end_log()@ < seq.len() && self.start_log()@ <= self.end_log()@+1 ==> result

ensures

self.end_log()@ >= seq.len() ==> !result

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

(open)

pearlite! {
    if self.is_empty_log() { out@ == Seq::empty() }
    else { seq.subsequence(self.start_log()@, self.end_log()@ + 1) == out@ }
}

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

(open)

pearlite! {
    forall<i> 0 <= i
        && (i < self.start_log()@ || self.end_log()@ < i || self.is_empty_log())
        && i < old.len()
        ==> old[i] == fin[i]
}

impl<T> SliceIndexSpec<[T]> for RangeTo<usize>

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

(open)

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

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

(open)

pearlite! { seq.subsequence(0, self.end@) == out@ }

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

(open)

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

impl<T> SliceIndexSpec<[T]> for RangeToInclusive<usize>

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

(open)

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

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

(open)

pearlite! { seq.subsequence(0, self.end@ + 1) == out@ }

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

(open)

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

Implementors