Trait creusot_contracts::std::ops::FnMutExt

pub trait FnMutExt<Args: Tuple>: FnOnceExt<Args> {
    // Required methods
    fn postcondition_mut(self, _: Args, _: Self, _: Self::Output) -> bool;
    fn unnest(self, _: Self) -> bool;
    fn postcondition_mut_unnest(
        self,
        args: Args,
        res_state: Self,
        res: Self::Output,
    );
    fn unnest_refl(self);
    fn unnest_trans(self, b: Self, c: Self);
    fn fn_mut_once(self, args: Args, res: Self::Output)
       where Self: Sized;
}

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

logic(prophetic)

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

logic(prophetic)

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

law

requires

self.postcondition_mut(args, res_state, res)

ensures

self.unnest(res_state)

fn unnest_refl(self)

law

ensures

self.unnest(self)

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

law

requires

self.unnest(b)

requires

b.unnest(c)

ensures

self.unnest(c)

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

where Self: Sized,

law

ensures

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

Object Safety

This trait is not object safe.

Implementors

impl<Args: Tuple, F: FnMut<Args>> FnMutExt<Args> for F