Struct ValidatedInterval 

pub struct ValidatedInterval { /* private fields */ }

A validated interval: a FloatInterval together with a proof obligation tag.

In a real verified system this would carry a kernel proof; here we store a human-readable certificate string.

Implementations

impl ValidatedInterval

pub fn verified(interval: FloatInterval, certificate: impl Into<String>) -> Self

Create a verified validated interval.

pub fn unverified(interval: FloatInterval) -> Self

Create an unverified validated interval (e.g., computed, not proved).

pub fn interval(&self) -> FloatInterval

Return the underlying interval.

pub fn is_verified(&self) -> bool

Return whether this interval has been formally verified.

pub fn certificate(&self) -> &str

The certificate string.

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

Compute the addition of two validated intervals. Result is verified only if both inputs are.

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

Compute the multiplication of two validated intervals.

Trait Implementations

impl Clone for ValidatedInterval

fn clone(&self) -> ValidatedInterval

Returns a duplicate of the value.

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

Performs copy-assignment from source.

impl Debug for ValidatedInterval

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

Formats the value using the given formatter.