Skip to main content

UpdatePredicate

vstd::atomic

Trait UpdatePredicate 

Source 
pub trait UpdatePredicate<X, Y>: Sized {
    // Required methods
    spec fn req(self, x: X) -> bool;
    spec fn ens(self, x: X, y: Y) -> bool;

    // Provided methods
    open spec fn outer_mask(self) -> ISet<int> { ... }
    fn inner_mask(self) -> ISet<int> { ... }
}
Expand description

Trait used to specify the update predicate for the AtomicUpdate.

This trait is implemented automatically by Verus when a logically atomic function is defined.

exec fn function(px: PX) -> (py: PY)
    atomically (atomic_update) {
        type PredType,

        (ax: AX) -> (ay: AY),

        requires atomic_pre(px, ax),
        ensures atomic_post(px, ax, ay),

        outer_mask Eo,
        inner_mask Ei,
    },
    requires private_pre(px),
    ensures private_post(px, ax, ay, py),

The above code snipped generates (roughly) the type and trait implementation below.

struct PredType { px: Ghost<PX> }

impl UpdatePredicate<AX, AY> for PredType {
    open spec fn req(self, x: X)       -> bool { atomic_pre  }
    open spec fn ens(self, x: X, y: Y) -> bool { atomic_post }

    open spec fn outer_mask(self) -> ISet<int> { Eo }
    open spec fn inner_mask(self) -> ISet<int> { Ei }
}

Required Methods§

Source

spec fn req(self, x: X) -> bool

The atomic pre-condition.

Source

spec fn ens(self, x: X, y: Y) -> bool

The atomic post-condition.

Provided Methods§

Source

open spec fn outer_mask(self) -> ISet<int>

{ ISet::empty() }

The outer mask of the atomic update.

Source

open spec fn inner_mask(self) -> ISet<int>

{ ISet::empty() }

The inner mask of the atomic update.

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.

Implementors§