Invariant
Precondition
Weaseling
Loop invariant
Loop variant
Loop invariant
Loop variant
Check instruction
Postcondition
Invariant
Execution completed