Design and Analysis of Algorithms

138 Design and Analysis of Algorithms

Here the desired expression e is (r), because r ≥ 0 and y > 0 holds throughout the algorithm. The value

of this expression decreases every time the body of the while loop is executed. Thus the termination is

established.

Under what conditions will the

while-do loop not terminate? If not only P but P ∧ B is also an invariant

for the loop, then it will not terminate. This will imply that e > 0 is the invariant of the loop, instead of e ≥ 0.

Similarly, a condition for the non-termination of repeat-until can be derived.

In summary, in order to prove a correctness proposition about a loop, one must:

1. Identify a suitable loop invariant I, if not already given by the software designer.

2. Prove that the initialization ...