In a loop, if L is an invariant of the loop body B, then L is known as a loop invariant, while C
– – L
B
– – L
The loop invariant is true before the loop body and after the loop body, each time. Since L is true at the start of the first iteration, L is true at the start of the loop also (just before the loop). Since L is true at the end of the last iteration, L is true when the loop ends also (just after the loop). Thus, if L is a loop variant, then it is true at four important points in the algorithm, as annotated in the algorithm.
1. At the start of the loop (just before the loop)
2. at the start of each iteration (before loop body)
3. at the end of each iteration (after loop body)
4. at the end of the loop (just after the loop)