Struct PermCellOwn 

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

Token that represents the ownership of a PermCell object.

A PermCellOwn only exists in the ghost world, and it must be used in conjunction with PermCell in order to read or write the value.

Implementations

impl<T: ?Sized> PermCellOwn<T>

pub fn id(self) -> Id

Returns the logical identity of the cell.

To use a PermCell, this and PermCell::id must agree.

(opaque)

pub fn val<'a>(self) -> &'a T

Get the logical value.

(opaque)

pub fn id_ghost(&self) -> Ghost<Id>

terminates

ghost

ensures

*result == self.id()

pub fn disjoint_lemma(own1: &mut PermCellOwn<T>, own2: &PermCellOwn<T>)

If one owns two PermCellOwns in ghost code, then they have different ids.

terminates

ghost

ensures

own1.id() != own2.id()

ensures

*own1 == ^own1

Trait Implementations

impl<T: Sized> Invariant for PermCellOwn<T>

fn invariant(self) -> bool

(open, prophetic, inline)

pearlite! { inv(self.val()) }

impl<T: ?Sized> Resolve for PermCellOwn<T>

fn resolve(self) -> bool

(open, prophetic, inline)

resolve(self.val())

fn resolve_coherence(self)

(prophetic)

requires

inv(self)

requires

structural_resolve(self)

ensures

self.resolve()

impl<T> View for PermCellOwn<T>

fn view(self) -> Self::ViewTy

(open, inline)

*self.val()

type ViewTy = T