Struct HoareLogic 

pub struct HoareLogic {
    pub axiom_names: Vec<String>,
}

Hoare logic system with proof-theoretic API.

Fields

axiom_names: Vec<String>

Implementations

impl HoareLogic

pub fn new() -> Self

pub fn axioms(&self) -> Vec<(&str, &str)>

Return all Hoare logic axioms as (name, description) pairs.

pub fn soundness_proof(&self) -> String

Return a description of the soundness proof for Hoare logic.

pub fn completeness_proof(&self) -> String

Return a description of the completeness proof (Cook’s theorem).

Trait Implementations

impl Default for HoareLogic

fn default() -> Self

Returns the “default value” for a type.