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§
type Completion
Required Methods§
Sourceproof fn apply(tracked
self,
op: Op,
tracked r: &mut Op::Resource,
new_state: Op::NewState,
e: &Op::ExecResult,
) -> tracked out : Self::Completion
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),
ensuresop.ensures(*old(r), *r, new_state),
self.post(op, *e, out),
Provided Methods§
Sourceopen spec fn namespaces(self) -> Set<int>
open spec fn namespaces(self) -> Set<int>
{ Set::empty() }
Sourceopen spec fn post(self, op: Op, r: Op::ExecResult, c: Self::Completion) -> bool
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.