Struct Contract 

pub struct Contract {
    pub requires: Box<[Condition]>,
    pub ensures: Box<[Condition]>,
}

Fields

requires: Box<[Condition]>

ensures: Box<[Condition]>

Implementations

impl Contract

pub fn is_empty(&self) -> bool

pub fn ensures_conj(&self) -> Exp

pub fn ensures_conj_labelled(&self) -> Exp

pub fn requires_conj(&self) -> Exp

pub fn requires_conj_labelled(&self) -> Exp

pub fn requires_implies(&self, conclusion: Exp) -> Exp

pub fn subst(&mut self, subst: &HashMap<Ident, Exp>)

pub fn qfvs(&self) -> IndexSet<QName>

Trait Implementations

impl Clone for Contract

fn clone(&self) -> Contract

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Contract

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Contract

fn default() -> Contract

Returns the “default value” for a type.

impl Print for Contract

fn pretty<'a, A: DocAllocator<'a>>( &'a self, alloc: &'a A, scope: &mut Why3Scope, ) -> DocBuilder<'a, A>

where A::Doc: Clone,

fn display(&self) -> PrintDisplay<'_, Self>

where Self: Sized,