Trait creusot_contracts::std::ops::FnExt

pub trait FnExt<Args: Tuple>: FnMutExt<Args> {
    // Required methods
    fn postcondition(self, _: Args, _: Self::Output) -> bool;
    fn fn_mut(self, args: Args, res_state: Self, res: Self::Output);
    fn fn_once(self, args: Args, res: Self::Output)
       where Self: Sized;
}

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

Required Methods

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

logic(prophetic)

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

law

ensures

self.postcondition_mut(args, res_state, res) == (self == res_state && self.postcondition(args, res))

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

where Self: Sized,

law

ensures

self.postcondition_once(args, res) == (resolve(&self) && self.postcondition(args, res))

Object Safety

This trait is not object safe.

Implementors

impl<Args: Tuple, F: Fn<Args>> FnExt<Args> for F