vstd::logatom

Trait ReadOperation

Source 
pub trait ReadOperation: Sized {
    type Resource;
    type ExecResult;

    // Required method
    spec fn requires(self, r: Self::Resource, e: Self::ExecResult) -> bool;

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

Required Associated Types§

Source

type Resource

Source

type ExecResult

Required Methods§

Source

spec fn requires(self, r: Self::Resource, e: Self::ExecResult) -> bool

Provided Methods§

Source

open spec fn peek_requires(self, r: Self::Resource) -> bool

{ true }
Source

open spec fn peek_ensures(self, r: Self::Resource) -> 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§