Trait ExSliceIndex 

pub trait ExSliceIndex<T>
where
    T: ?Sized,
{
    type ExternalTraitSpecificationFor: SliceIndex<T>;
    type Output: ?Sized;

    // Required methods
    spec fn in_bounds(&self, slice: &T) -> bool;
    spec fn index_postcondition(&self, slice: &T, r: &Self::Output) -> bool;
    spec fn index_mut_postcondition(
        &self,
        old_slice: &T,
        final_slice: &T,
        immediate_output: &Self::Output,
        final_output: &Self::Output,
    ) -> bool;
    exec fn index(self, slice: &T) -> r : &Self::Output;
    exec fn index_mut(self, slice: &mut T) -> r : &mut Self::Output;
    exec fn get(self, slice: &T) -> r : Option<&Self::Output>;
    exec fn get_mut(self, slice: &mut T) -> r : Option<&mut Self::Output>;
}

Required Associated Types

type ExternalTraitSpecificationFor: SliceIndex<T>

type Output: ?Sized

Required Methods

spec fn in_bounds(&self, slice: &T) -> bool

spec fn index_postcondition(&self, slice: &T, r: &Self::Output) -> bool

spec fn index_mut_postcondition( &self, old_slice: &T, final_slice: &T, immediate_output: &Self::Output, final_output: &Self::Output, ) -> bool

exec fn index(self, slice: &T) -> r : &Self::Output

requires

self.in_bounds(slice),

ensures

self.index_postcondition(slice, r),

exec fn index_mut(self, slice: &mut T) -> r : &mut Self::Output

requires

self.in_bounds(slice),

ensures

self.index_mut_postcondition(&*old(slice), &*final(slice), r, &*final(r)),

exec fn get(self, slice: &T) -> r : Option<&Self::Output>

ensures

match r {
    None => !self.in_bounds(slice),
    Some(x) => self.in_bounds(slice) && self.index_postcondition(slice, x),
},

exec fn get_mut(self, slice: &mut T) -> r : Option<&mut Self::Output>

ensures

match r {
    None => !self.in_bounds(old(slice)) && &*final(slice) == &*old(slice),
    Some(x) => (
        &&& self.in_bounds(old(slice))
        &&& self.index_mut_postcondition(&*old(slice), &*final(slice), x, &*final(x))

    ),
},

Dyn Compatibility

This trait is dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety".

Implementors