Struct WeakestPrecondition 

pub struct WeakestPrecondition {
    pub stmt: String,
    pub post: String,
}

Weakest precondition transformer.

Fields

stmt: String

post: String

Implementations

impl WeakestPrecondition

pub fn new(stmt: impl Into<String>, post: impl Into<String>) -> Self

pub fn compute_wp(&self) -> String

Compute the weakest precondition WP(stmt, post). Returns a textual description of the WP.

pub fn is_valid_hoare(&self) -> bool

Check whether {WP(stmt,post)} stmt {post} is a valid Hoare triple.