Struct Excl 

pub struct Excl<T>(pub T);

The ‘exclusive’ Resource Algebra.

Combining those resource with RA::op never yields valid elements. As such, only one version of this resource (when using Resource) will be able to exist at a given moment.

Tuple Fields

0: T

Trait Implementations

impl<T> RA for Excl<T>

fn op(self, _other: Self) -> Option<Self>

(open)

None

fn factor(self, factor: Self) -> Option<Self>

(open)

None

ensures

match result {
        Some(c) => factor.op(c) == Some(self),
        None => forall<c: Self> factor.op(c) != Some(self),
    }

fn commutative(a: Self, b: Self)

(open(pub(self)), law)

ensures

a.op(b) == b.op(a)

fn associative(a: Self, b: Self, c: Self)

(open(pub(self)), law)

ensures

a.op(b).and_then_logic(|ab: Self| ab.op(c)) == b.op(c).and_then_logic(|bc| a.op(bc))

fn core(self) -> Option<Self>

(open)

None

ensures

match result {
        Some(c) => c.op(c) == Some(c) && c.op(self) == Some(self),
        None => true
    }

fn core_is_maximal_idemp(self, i: Self)

requires

i.op(i) == Some(i)

requires

i.op(self) == Some(self)

ensures

match self.core() {
        Some(c) => i.incl(c),
        None => false,
    }

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

Inclusion of RA.

fn incl_op(self, other: Self, comb: Self)

(law, sealed)

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

(open, sealed)

fn incl_eq_op(a: Self, b: Self, x: Self) -> bool

(open, sealed)

fn update(self, x: Self) -> bool

Ensures that we can go from self to x without making composition with the frame invalid.

fn update_nondet(self, s: Set<Self>) -> bool

This is used in Resource::update_nondet.

fn incl_transitive(a: Self, b: Self, c: Self)

RA::incl is transitive.

impl<T> Update<Excl<T>> for ExclUpdate<T>

fn premise(self, _: Excl<T>) -> bool

(open)

true

fn update(self, from: Excl<T>, _: ()) -> Excl<T>

(open)

Excl(*self.0)

requires

self.premise(from)

fn frame_preserving(self, from: Excl<T>, frame: Excl<T>)

requires

self.premise(from)

requires

from.op(frame) != None

ensures

self.update(from, result).op(frame) != None

type Choice = ()