Struct PredCell 

pub struct PredCell<T: ?Sized>(/* private fields */);

Cell over predicates

A wrapper around std::cell::Cell that allows predicates to be used to specify the contents of the cell.

Implementations

impl<T> PredCell<T>

pub const fn new(v: T, _pred: Snapshot<Mapping<T, bool>>) -> Self

See the method Cell::new documentation.

requires

_pred[v]

ensures

result@ == *_pred

pub fn set(&self, v: T)

See the method Cell::set documentation.

requires

self@[v]

pub fn swap(&self, other: &PredCell<T>)

See the method Cell::swap documentation.

requires

forall<x: T> self@[x] == other@[x]

pub const fn replace(&self, v: T) -> T

See the method Cell::replace documentation.

requires

self@[v]

ensures

self@[result]

pub fn into_inner(self) -> T

See the method Cell::into_inner documentation.

ensures

self@[result]

impl<T: Copy> PredCell<T>

pub const fn get(&self) -> T

See the method Cell::get documentation.

ensures

self@[result]

pub fn update(&self, f: impl FnOnce(T) -> T)

See the method Cell::update documentation.

requires

forall<x: T> self@[x] ==> f.precondition((x,))

requires

forall<x: T, res: T> self@[x] && f.postcondition_once((x,), res) ==> self@[res]

ensures

exists<x: T, res: T> self@[x] && f.postcondition_once((x,), res)

impl<T: ?Sized> PredCell<T>

pub const fn from_mut( t: &mut T, _pred: Snapshot<Mapping<T, bool>>, ) -> &PredCell<T>

See the method Cell::from_mut documentation.

requires

_pred[*t]

ensures

_pred[^t]

ensures

result@ == *_pred

impl<T: Default> PredCell<T>

pub fn take(&self) -> T

See the method Cell::take documentation.

requires

forall<x: T> T::default.postcondition((), x) ==> self@[x]

ensures

self@[result]

impl<T> PredCell<[T]>

pub const fn as_slice_of_cells( &self, _pred: Snapshot<Seq<Mapping<T, bool>>>, ) -> &[PredCell<T>]

See the method Cell::as_slice_of_cells documentation.

requires

forall<s: [T]> self@[s] == (_pred.len() == s@.len() && forall<i: Int> 0 <= i && i < s@.len() ==> _pred[i][s[i]])

ensures

forall<i: Int> 0 <= i && i < _pred.len() ==> result[i]@ == _pred[i]

ensures

result@.len() == _pred.len()

Trait Implementations

impl<T: ?Sized> View for PredCell<T>

fn view(self) -> Self::ViewTy

(opaque)

type ViewTy = Mapping<T, bool>