vstd::std_specs::core

Trait IndexSetTrustedSpec

Source
pub trait IndexSetTrustedSpec<Idx>: IndexMut<Idx> + TrustedSpecSealed {
    // Required methods
    spec fn spec_index_set_requires(&self, index: Idx) -> bool;
    spec fn spec_index_set_ensures(
        &self,
        new_container: &Self,
        index: Idx,
        val: Self::Output,
    ) -> bool
       where Self::Output: Sized;
}

Required Methods§

Source

spec fn spec_index_set_requires(&self, index: Idx) -> bool

Source

spec fn spec_index_set_ensures( &self, new_container: &Self, index: Idx, val: Self::Output, ) -> bool
where Self::Output: Sized,

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.

Implementations on Foreign Types§

Source§

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

Source§

open spec fn spec_index_set_requires(&self, index: usize) -> bool

{ 0 <= index < self@.len() }
Source§

open spec fn spec_index_set_ensures( &self, new_container: &Self, index: usize, val: T, ) -> bool

{ new_container@ == self@.update(index as int, val) }
Source§

impl<T, A: Allocator> IndexSetTrustedSpec<usize> for Vec<T, A>

Source§

open spec fn spec_index_set_requires(&self, index: usize) -> bool

{ 0 <= index < self.len() }
Source§

open spec fn spec_index_set_ensures( &self, new_container: &Self, index: usize, val: T, ) -> bool

{ new_container@ === self@.update(index as int, val) }
Source§

impl<T, const N: usize> IndexSetTrustedSpec<usize> for [T; N]

Source§

open spec fn spec_index_set_requires(&self, index: usize) -> bool

{ 0 <= index < N }
Source§

open spec fn spec_index_set_ensures( &self, new_container: &Self, index: usize, val: T, ) -> bool

{ new_container@ === self@.update(index as int, val) }

Implementors§