Struct FormalVerificationEngine 

pub struct FormalVerificationEngine<T: Float + Debug + Send + Sync + 'static> { /* private fields */ }

Formal verification engine.

Implementations

impl<T: Float + Debug + Send + Sync + 'static> FormalVerificationEngine<T>

pub fn new() -> Self

Create an engine with the default rule set and axioms registered.

pub fn empty() -> Self

Create an engine with nothing registered.

FormalVerificationEngine::verify_all_properties then returns an error, because an engine with no rules has verified nothing.

pub fn rule_count(&self) -> usize

Number of registered rules.

pub fn rule_names(&self) -> Vec<String>

Names of the registered rules.

pub fn add_rule(&mut self, rule: FormalVerificationRule<T>)

Register an additional rule.

pub fn proof_system(&self) -> &ProofSystem<T>

Access the proof system.

pub fn theorem_prover(&self) -> &TheoremProver<T>

Access the theorem prover.

pub fn theorem_prover_mut(&mut self) -> &mut TheoremProver<T>

Mutable access to the theorem prover.

pub fn model_checker_mut(&mut self) -> &mut ModelChecker<T>

Mutable access to the model checker.

pub fn verify_all_properties( &self, data: &Array1<T>, context: &PrivacyContext, ) -> Result<Vec<VerificationResult>>

Run every registered rule.

Returns an error when no rules are registered: an empty result vector must never be readable as “verified”.

pub fn require_all_properties( &self, data: &Array1<T>, context: &PrivacyContext, ) -> Result<Vec<VerificationResult>>

Run every rule and fail if any safety- or correctness-critical rule does not hold.

pub fn check_model_property( &self, property: &SystemProperty, ) -> Result<ModelCheckOutcome>

Check a registered invariant property against the system model.

Trait Implementations

impl<T: Float + Debug + Send + Sync + 'static> Default for FormalVerificationEngine<T>

fn default() -> Self

Returns the “default value” for a type.