Struct HoareTriple 

pub struct HoareTriple {
    pub pre: Assertion,
    pub command: String,
    pub post: Assertion,
    pub total: bool,
}

A Hoare triple {P} C {Q}.

Fields

pre: Assertion

Pre-condition.

command: String

Program command (as a string).

post: Assertion

Post-condition.

total: bool

Whether this is a total-correctness triple.

Implementations

impl HoareTriple

pub fn partial( pre: Assertion, command: impl Into<String>, post: Assertion, ) -> Self

Create a partial-correctness Hoare triple.

pub fn total( pre: Assertion, command: impl Into<String>, post: Assertion, ) -> Self

Create a total-correctness Hoare triple.

pub fn display(&self) -> String

Return the display string {P} C {Q} or [P] C [Q].

Trait Implementations

impl Clone for HoareTriple

fn clone(&self) -> HoareTriple

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for HoareTriple

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

Formats the value using the given formatter.