Design and Analysis of Algorithms

748 Design and Analysis of Algorithms

To prove that {m, n are positive integers and x = m and y = n} B {x = gcd(m, n)}, we have to come up

with a suitable loop invariant, meaning some predicate P(m ,n, x, y) that

1. Is true just before the fi rst execution of the body of the

while loop.

2. Remains preserved by each execution of the body of the

while loop.

In terms of Hoare triples, these two requirements can be stated as follows:

1. (m,n are positive integers, x = m, y = n) implies P(m, n, x, y) and

2. {(x does not equal y and P(m, n, x, y))} C {P(m, n, x, y)}. Many predicates P(m, n, x, y) are loop

invariants in the sense of satisfying 1 and 2 (“m, n, x, y are integers” is one such predicate); we want

a loop invariant that ...