Struct LoopSpec 

pub struct LoopSpec {
    pub maintains: Vec<PreCondition>,
    pub decreases: Option<LoopVariant>,
    /* private fields */
}

Specifies the intended behavior of a loop: while or for.

Fields

maintains: Vec<PreCondition>

Loop invariants: conditions that must hold both before and after the loop’s body runs.

decreases: Option<LoopVariant>

Loop variant: an expression that decreases with each run of the loop’s body.

Implementations

impl LoopSpec

pub fn empty() -> Self

Empty spec that contains no elements.

pub fn is_empty(&self) -> bool

Returns true if the spec is empty (specifies nothing), otherwise returns false.

pub fn spec_err(&self, message: &str) -> Error

Construct an error from the whole spec.

Trait Implementations

impl Debug for LoopSpec

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

Formats the value using the given formatter.

impl Parse for LoopSpec

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