Struct Assertion 

pub struct Assertion {
    pub formula: String,
}

A logical assertion over a program state, represented as a formula string.

Fields

formula: String

The formula as a string (e.g. "x >= 0 /\ y < n").

Implementations

impl Assertion

pub fn new(formula: impl Into<String>) -> Self

Create a new assertion.

pub fn negate(&self) -> Self

Return the negation ¬P.

pub fn and(&self, other: &Self) -> Self

Return the conjunction P ∧ Q.

pub fn or(&self, other: &Self) -> Self

Return the disjunction P ∨ Q.

pub fn subst(&self, var: &str, expr: &str) -> Self

Perform syntactic substitution [e/x] in the formula (string-level).

Trait Implementations

impl Clone for Assertion

fn clone(&self) -> Assertion

Returns a duplicate of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for Assertion

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

Formats the value using the given formatter.

impl Display for Assertion

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

Formats the value using the given formatter.

impl PartialEq for Assertion

fn eq(&self, other: &Assertion) -> bool

Tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

Tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Eq for Assertion

impl StructuralPartialEq for Assertion