Struct SepLogicTriple 

pub struct SepLogicTriple {
    pub precondition: String,
    pub command: String,
    pub postcondition: String,
}

Separation logic Hoare triple.

Fields

precondition: String

command: String

postcondition: String

Implementations

impl SepLogicTriple

pub fn new(pre: &str, cmd: &str, post: &str) -> Self

pub fn frame_rule(&self, frame: &str) -> SepLogicTriple

pub fn display(&self) -> String

Trait Implementations

impl Clone for SepLogicTriple

fn clone(&self) -> SepLogicTriple

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for SepLogicTriple

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

Formats the value using the given formatter.