Trait MutOperationCopy item path

pub trait MutOperation: Sized {
    type Resource;
    type ExecResult;
    type NewState;

    // Required methods
    spec fn requires(
        self,
        pre: Self::Resource,
        new_state: Self::NewState,
        e: Self::ExecResult,
    ) -> bool;
    spec fn ensures(
        self,
        pre: Self::Resource,
        post: Self::Resource,
        new_state: Self::NewState,
    ) -> bool;

    // Provided methods
    open spec fn peek_requires(self, r: Self::Resource) -> bool { ... }
    fn peek_ensures(self, r: Self::Resource) -> bool { ... }
}

Required Associated Types§

Required Methods§

Provided Methods§

{ true }

{ true }

Dyn Compatibility§

Implementors§