The loop invariant is true in four crucial points in a loop. Using the loop invariant, we can construct the loop and reason about the properties of the variables at these points.
Example:
Design an iterative algorithm to compute an. Let us name the algorithm power(a, n).
For example,
power(10, 4) = 10000
power (5, 3) = 125
power (2, 5) = 32
Algorithm power(a, n) computes a by multiplying an cumulatively n times,
The specification and the loop invariant are shown as comments. power (a, n)
– – inputs: n is a positive integer
– – outputs: p = an
p, i : = 1, 0
while i ≠ n
– – loop invariant: p = ai
p, i : = p x a, i + 1
The step by step execution of power (2, 5) is shown in Table. Each row shows the values of the two variables p and i at the end of an iteration, and how they are calculated. We see that p = a is true at the start of the loop, and remains true in each row. Therefore, it is a loop invariant.
When the loop ends, p = ai is still true, but i = 5. Therefore, p = a5 . In general, when the loop ends,
p = an . Thus, we have verified that power(a, n) satisfies its specification.
