Invariants

An invariant is an assertion that is preserved by the loop across iterations.

The loop invariant is valid if it holds...

1. before the first iteration after performing the initialization statement
2. after every iteration
3. when exiting the loop

In Gobra we can specify it with the invariant keyword before a loop.

//@ invariant ASSERTION
for condition {
	// ..
}

Similarly to requires and ensures you can split an invariant on multiple lines.