Struct FunctionSummary 

pub struct FunctionSummary {
    pub function_name: String,
    pub precondition: IntervalEnv,
    pub postcondition: IntervalEnv,
    pub termination: TerminationEvidence,
    pub cost: CostBound,
}

A function summary: pre/post conditions as interval environments.

Fields

function_name: String

precondition: IntervalEnv

postcondition: IntervalEnv

termination: TerminationEvidence

cost: CostBound

Implementations

impl FunctionSummary

pub fn new(name: impl Into<String>) -> Self

Create a new summary.

pub fn terminates(&self) -> bool

Return whether the function is proven to terminate.

pub fn describe(&self) -> String

Return a description of the summary.