Struct SyncView 

pub struct SyncView(/* private fields */);

A witness to the current view, containing all the events observed by this thread.

In Cosmo, SyncView corresponds to the notation ↑V In Relaxed RustBelt, SyncView corresponds to the notation V.cur

Implementations

impl SyncView

pub fn new() -> Ghost<Self>

ghost

pub fn weaken(&mut self, to: Snapshot<SyncView>)

ghost

requires

*to <= *self

ensures

^self == *to

pub fn meet(self, other: Self) -> Self

logic(opaque)

ensures

self >= result

ensures

other >= result

ensures

forall<r> self >= r ==> other >= r ==> result >= r

Trait Implementations

impl Clone for SyncView

fn clone(&self) -> Self

ensures

result == *self

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Copy for SyncView

impl From<ReleaseSyncView> for SyncView

fn from(value: ReleaseSyncView) -> Self

ghost

ensures

result == value@

impl From<SyncView> for AcquireSyncView

fn from(value: SyncView) -> Self

ghost

ensures

result@ == value

impl PartialOrdLogic for SyncView

fn lt_log(self, _: Self) -> bool

logic(opaque)

fn irreflexive(self)

logic(law)

ensures

!(self < self)

fn transitive(x: Self, y: Self, z: Self)

logic(law)

requires

x < y

requires

y < z

ensures

x < z

fn le_lt_log(self, other: Self)

logic(law)

ensures

(self <= other) == (self < other || self == other)

fn gt_log(self, other: Self) -> bool

The logical > operation.

fn le_log(self, other: Self) -> bool

The logical <= operation.

fn ge_log(self, other: Self) -> bool

The logical >= operation.

fn partial_cmp_log(self, other: Self) -> Option<Ordering>

logic(open, sealed)