Loop Annotations
A loop invariant is a property that must hold before each iteration of a loop. The verifier checks that it holds initially and that the loop body preserves it.
Inductive Reasoning
Loop verification uses the same technique as mathematical induction: prove a base case, prove the inductive step, and conclude the property holds for all iterations.
Finding Loop Invariants
A systematic approach to discovering the invariants your loop needs.