Loop invariant

Loop invariant

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 and shown in Figure 8.1.

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)

-- L, start of loop

while

C

-- L, start of iteration

B

-- L, end of iteration

-- L, end of loop

To construct a loop,

1.           Establish the loop invariant at the start of the loop.

2.           The loop body should so update the variables as to progress toward the end, and maintain the loop invariant, at the same time.

3.           When the loop ends, the termination condition and the loop invariant should establish the input-output relation.