Struct Spec 

pub struct Spec {
    pub requires: Vec<Condition>,
    pub maintains: Vec<Condition>,
    pub ensures: Vec<ConditionClosure>,
}

A spec specifies the intended behavior of a function or method.

Fields

requires: Vec<Condition>

Preconditions: conditions that must hold when the function is called.

maintains: Vec<Condition>

Invariants: conditions that must hold both when the function is called and when it returns.

ensures: Vec<ConditionClosure>

Postconditions: conditions that must hold when the function returns.

Trait Implementations

impl Debug for Spec

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

Formats the value using the given formatter.

impl Parse for Spec

fn parse(input: ParseStream<'_>) -> Result<Self>