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§
type Resource
type ExecResult
Required Methods§
Sourcespec fn requires(self, r: Self::Resource, e: Self::ExecResult) -> bool
spec fn requires(self, r: Self::Resource, e: Self::ExecResult) -> bool
Provided Methods§
Sourceopen spec fn peek_requires(self, r: Self::Resource) -> bool
open spec fn peek_requires(self, r: Self::Resource) -> bool
{ true }
Sourceopen spec fn peek_ensures(self, r: Self::Resource) -> bool
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.