Attribute Macro creusot_contracts::macros::invariant

#[invariant]

A loop invariant

The inside of a invariant may look like Rust code, but it is in fact pearlite.

Produced

If the loop is a for loop, you have access to a special variable produced, that holds a sequence of all the (logical representations of) items the iterator yielded so far.

Example

let mut v = Vec::new();
// For annoying reasons, examples cannot use invariants. Please imagine that they are uncommented :)
// #[invariant(v@.len() == produced.len())]
// #[invariant(forall<j: Int> 0 <= j && j < produced.len() ==> v@[j]@ == j)]
for i in 0..10 {
    v.push(i);
}