Trait UpdatePredicate 

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> { ... }
}

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

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

The atomic pre-condition.

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

The atomic post-condition.

Provided Methods

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

{ ISet::empty() }

The outer mask of the atomic update.

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".

Implementors