Macro cvlr_spec 

macro_rules! cvlr_spec {
    (requires: $r:expr, ensures: $e:expr $(,)?) => { ... };
    (ensures: $e:expr $(,)?) => { ... };
}

Creates a specification from preconditions (requires) and postconditions (ensures).

This macro is a convenience wrapper around cvlr_spec that provides a more readable syntax for creating specifications.

Syntax

cvlr_spec! {
    requires: requires_expression,
    ensures: ensures_expression,
}

// Or omit `requires` to use [`cvlr_true`](crate::cvlr_true) as the precondition:
cvlr_spec! {
    ensures: ensures_expression,
}

Parameters

• requires (optional) - A boolean expression over the context type representing the precondition. If omitted, cvlr_true is used for the same context as ensures.
• ensures - A boolean expression over the context type that uses eval_with_states to evaluate over both pre-state and post-state

Returns

Returns a value implementing CvlrSpec with the same context type as the ensures expression.

Examples

use cvlr_spec::{cvlr_spec, cvlr_predicate, cvlr_def_states_predicate};

struct Counter {
    value: i32,
}

// Define a predicate for the ensures clause that compares pre and post states
cvlr_def_states_predicate! {
    pred CounterIncreases ( [ c, o ] : Counter ) {
        c.value > o.value;
    }
}

// Create a spec using the macro
let spec = cvlr_spec! {
    requires: cvlr_predicate! { | c : Counter | -> { c.value >= 0 } },
    ensures: CounterIncreases,
};

// Use the spec
let pre = Counter { value: 5 };
let post = Counter { value: 10 };
spec.assume_requires(&pre);
spec.check_ensures(&post, &pre);