Enum Command 

pub enum Command {
    Skip,
    Assign(String, String),
    Seq(Box<Command>, Box<Command>),
    If(String, Box<Command>, Box<Command>),
    While(String, Assertion, Box<Command>),
}

A simple imperative command in a while-language.

Variants

Skip

Skip (no-op).

Assign(String, String)

Assignment: x := e.

Seq(Box<Command>, Box<Command>)

Sequence: C1; C2.

If(String, Box<Command>, Box<Command>)

Conditional: if b then C1 else C2.

While(String, Assertion, Box<Command>)

While loop: while b do C.

Implementations

impl Command

pub fn wp(&self, q: &Assertion) -> Assertion

Compute the weakest precondition of self with respect to postcondition q.

For Skip, wp(skip, Q) = Q. For Assign(x, e), wp(x := e, Q) = Q[e/x]. For Seq(C1, C2), wp(C1; C2, Q) = wp(C1, wp(C2, Q)). For If(b, C1, C2), wp = (b → wp(C1, Q)) ∧ (¬b → wp(C2, Q)). For While(b, I, C), we return I as the loop invariant approximation.

pub fn generate_vcs(&self, q: &Assertion) -> Vec<VerificationCondition>

Generate verification conditions for this command given a postcondition q.

Trait Implementations

impl Clone for Command

fn clone(&self) -> Command

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for Command

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

Formats the value using the given formatter.

impl Eq for Command

impl PartialEq for Command

fn eq(&self, other: &Command) -> bool

Equality operator ==.

fn ne(&self, other: &Rhs) -> bool

Inequality operator !=.

impl StructuralPartialEq for Command