Attribute Macro 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();
#[invariant(v@.len() == produced.len())]
#[invariant(forall<j> 0 <= j && j < produced.len() ==> v@[j]@ == j)]
for i in 0..10 {
    v.push(i);
}