vstd::logatom

Trait MutLinearizer

Source 
pub trait MutLinearizer<Op: MutOperation>: Sized {
    type Completion;

    // Required methods
    proof fn apply(tracked 
        self,
        op: Op,
tracked         r: &mut Op::Resource,
        new_state: Op::NewState,
        e: &Op::ExecResult,
    ) -> tracked out : Self::Completion;
    proof fn peek(tracked &self, op: Op, tracked r: &Op::Resource);

    // Provided methods
    open spec fn namespaces(self) -> Set<int> { ... }
    fn pre(self, op: Op) -> bool { ... }
    fn post(self, op: Op, r: Op::ExecResult, c: Self::Completion) -> bool { ... }
}

Required Associated Types§

Source

type Completion

Required Methods§

Source

proof fn apply(tracked self, op: Op, tracked r: &mut Op::Resource, new_state: Op::NewState, e: &Op::ExecResult, ) -> tracked out : Self::Completion

requires
self.pre(op),
op.requires(*old(r), new_state, *e),
ensures
op.ensures(*old(r), *r, new_state),
self.post(op, *e, out),
Source

proof fn peek(tracked &self, op: Op, tracked r: &Op::Resource)

requires
self.pre(op),
op.peek_requires(*r),
ensures
op.peek_ensures(*r),

Provided Methods§

Source

open spec fn namespaces(self) -> Set<int>

{ Set::empty() }
Source

open spec fn pre(self, op: Op) -> bool

{ true }
Source

open spec fn post(self, op: Op, r: Op::ExecResult, c: Self::Completion) -> bool

{ true }

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§