Struct HoareVerifier 

pub struct HoareVerifier { /* private fields */ }

A simple Hoare-logic verifier for IO programs.

Records pre/postcondition pairs for IO operations and checks consistency.

Implementations

impl HoareVerifier

pub fn new() -> Self

Create an empty verifier.

pub fn add_triple( &mut self, op: impl Into<String>, pre: impl Into<String>, post: impl Into<String>, )

Add a Hoare triple.

pub fn triple_count(&self) -> usize

Count registered triples.

pub fn postcondition_of(&self, op: &str) -> Option<&str>

Look up the postcondition for a given operation.

pub fn has_triple(&self, op: &str) -> bool

Check if an operation has been registered.

pub fn operations(&self) -> Vec<&str>

Get all registered operation names.

Trait Implementations

impl Default for HoareVerifier

fn default() -> Self

Returns the “default value” for a type.