Trait ReadLinearizerCopy item path

pub trait ReadLinearizer<Op: ReadOperation>: Sized {
    type Completion;

    // Required methods
    proof fn apply(tracked 
        self,
        op: Op,
tracked         r: &Op::Resource,
        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§

Required Methods§

self.pre(op),

op.requires(*r, *e),

self.post(op, *e, out),

self.pre(op),

op.peek_requires(*r),

op.peek_ensures(*r),

Provided Methods§

{ Set::empty() }

{ true }

{ true }

Dyn Compatibility§

Implementors§