pub struct Contract { /* private fields */ }Expand description
Contract builder for complex contracts
Implementations§
Source§impl Contract
impl Contract
pub fn new() -> Self
pub fn requires(self, condition: bool, description: &str) -> Self
pub fn ensures(self, condition: bool, description: &str) -> Self
pub fn invariant(self, condition: bool, description: &str) -> Self
pub fn check_preconditions(&self)
pub fn check_postconditions(&self)
pub fn check_invariants(&self)
Trait Implementations§
Auto Trait Implementations§
impl Freeze for Contract
impl RefUnwindSafe for Contract
impl Send for Contract
impl Sync for Contract
impl Unpin for Contract
impl UnsafeUnpin for Contract
impl UnwindSafe for Contract
Blanket Implementations§
Source§impl<T> BorrowMut<T> for Twhere
T: ?Sized,
impl<T> BorrowMut<T> for Twhere
T: ?Sized,
Source§fn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
Source§impl<T> Instrument for T
impl<T> Instrument for T
Source§fn instrument(self, span: Span) -> Instrumented<Self>
fn instrument(self, span: Span) -> Instrumented<Self>
Source§fn in_current_span(self) -> Instrumented<Self>
fn in_current_span(self) -> Instrumented<Self>
Source§impl<T> IntoEither for T
impl<T> IntoEither for T
Source§fn into_either(self, into_left: bool) -> Either<Self, Self>
fn into_either(self, into_left: bool) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left is true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read moreSource§fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
fn into_either_with<F>(self, into_left: F) -> Either<Self, Self>
Converts
self into a Left variant of Either<Self, Self>
if into_left(&self) returns true.
Converts self into a Right variant of Either<Self, Self>
otherwise. Read more