Trait FnMutExt 

pub trait FnMutExt<Args: Tuple>: FnOnceExt<Args> {
    // Required methods
    fn postcondition_mut(self, _: Args, _: Self, _: Self::Output) -> bool;
    fn hist_inv(self, _: Self) -> bool;
    fn postcondition_mut_hist_inv(
        self,
        args: Args,
        res_state: Self,
        res: Self::Output,
    );
    fn hist_inv_refl(self);
    fn hist_inv_trans(self, b: Self, c: Self);
    fn fn_mut_once(self, args: Args, res: Self::Output);
}

FnMutExt is an extension trait for the FnMut trait, used for adding a specification to closures. It should not be used directly.

Required Methods

fn postcondition_mut(self, _: Args, _: Self, _: Self::Output) -> bool

(prophetic)

fn hist_inv(self, _: Self) -> bool

(prophetic)

fn postcondition_mut_hist_inv( self, args: Args, res_state: Self, res: Self::Output, )

(law)

requires

self.postcondition_mut(args, res_state, res)

ensures

self.hist_inv(res_state)

fn hist_inv_refl(self)

(law)

ensures

self.hist_inv(self)

fn hist_inv_trans(self, b: Self, c: Self)

(law)

requires

self.hist_inv(b)

requires

b.hist_inv(c)

ensures

self.hist_inv(c)

fn fn_mut_once(self, args: Args, res: Self::Output)

(law)

ensures

self.postcondition_once(args, res) ==
              exists<res_state: Self> self.postcondition_mut(args, res_state, res) && resolve(res_state)

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

impl<Args: Tuple, F: ?Sized + FnMut<Args>> FnMutExt<Args> for F

Available on crate feature nightly only.