pub trait Invariant {
// Required method
fn invariant(self) -> bool;
}Expand description
A user-defined type invariant.
Type invariants are additional pre- and postconditions added to each program functions.
Not to be confused with loop invariants or resource invariants.
§Example
struct SumTo10 {
a: i32,
b: i32,
}
// The type invariant constrains the set of valid `SumTo10`s to
// only allow values where the sum of both fields is equal to 10.
impl Invariant for SumTo10 {
#[logic(open)]
fn invariant(self) -> bool {
pearlite! {
self.a@ + self.b@ == 10
}
}
}
// #[requires(inv(x))] // generated by Creusot
// #[ensures(inv(result))] // generated by Creusot
fn invariant_holds(mut x: SumTo10) -> SumTo10 {
assert!(x.a + x.b == 10); // We are given the invariant when entering the function
x.a = 5; // we can break it locally!
x.b = 5; // but it must be restored eventually
x
}§Structural invariants
A type automatically inherits the invariants of its fields.
Examples:
x: (T, U)->inv(x.0) && inv(x.1)x: &T->inv(*x)x: Vec<T>->forall<i> 0 <= i && i < x@.len() ==> inv(x@[i])
This does not prevent the type to additionnaly implement the Invariant trait.
§Mutable borrows
For mutable borrows, the invariant is the conjunction of the invariants of the current
and final values: x: &mut T -> inv(*x) && inv(^x).
§Logical functions
Invariant pre- and postconditions are not added to logical functions:
#[logic]
#[ensures(x.a@ + x.b@ == 10)]
fn not_provable(x: SumTo10) {}Required Methods§
Implementations on Foreign Types§
Source§impl<I: IteratorSpec> Invariant for Enumerate<I>
impl<I: IteratorSpec> Invariant for Enumerate<I>
Source§impl<T: ?Sized, A: Allocator> Invariant for Box<T, A>
Available on crate feature nightly only.
impl<T: ?Sized, A: Allocator> Invariant for Box<T, A>
Available on crate feature
nightly only.