Struct FormalVerificationOracle 

pub struct FormalVerificationOracle {
    pub max_bound: usize,
    pub timeout_ms: u64,
}

Formal verification oracle (bounded model checking)

Fields

max_bound: usize

Maximum bound for model checking

timeout_ms: u64

Timeout in milliseconds

Implementations

impl FormalVerificationOracle

pub fn new(max_bound: usize, timeout_ms: u64) -> Self

Create a new formal verification oracle

Trait Implementations

impl Debug for FormalVerificationOracle

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

Formats the value using the given formatter.

impl Default for FormalVerificationOracle

fn default() -> FormalVerificationOracle

Returns the “default value” for a type.

impl SemanticOracle for FormalVerificationOracle

fn check_equivalence(&self, source: &str, target: &str) -> SemanticVerdict

Check semantic equivalence between source and target

fn ast_similarity(&self, _source: &str, _target: &str) -> f64

Calculate AST similarity score

fn compare_memory(&self, _source: &str, _target: &str) -> bool

Compare memory layouts

fn compare_performance(&self, _source: &str, _target: &str) -> Option<f64>

Compare performance profiles