Reasoning About Correctness
A loop can have a precondition and a postcondition
It can also have an invariant: a Boolean expression that is true at the beginning of each iteration
Reason: precondition implies invariant, body re-establishes invariant, invariant and termination establish postcondition