x=m, y=n;
while x does not equal y
do if x < y
then y=y-x;
else x=x-y;
end
end
We want to prove that
m,n are positive integers {S} x=gcd(m,n).
Breaking the program into smaller pieces.
First, let us break S into two parts: let A denote the program segment
x=m, y=n;and let B denote the program segment
while x does not equal y
do if x < y
then y=y-x;
else x=x-y;
end
end
Trivially, we have
m,n are positive integers {A} m,n are positive integers & x=m & y=n
and so our job reduces to proving that
m,n are positive integers & x=m & y=n {B} x=gcd(m,n).
Loop invariants. Program segment B is a while loop. Let us
denote its body
if x < y
then y=y-x;
else x=x-y;
end
as C, so that B can be recorded as
while x does not equal y do C; endTo prove that
m,n are positive integers & x=m & 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 first execution of the body of the while loop, and
2. remains preserved by each execution of the body of the while loop;
1. (m,n are positive integers, x=m, y=n) implies P(m,n,x,y) and
2. (x does not equal y & P(m,n,x,y)) {C} P(m,n,x,y).
3.(P(m,n,x,y) & x=y) implies x=gcd(m,n).
If we manage to find a predicate P(m,n,x,y) along with a proof that this predicate has the three properties required of a useful loop invariant, then we are done: from 2. we can infer that
P(m,n,x,y) {B} (P(m,n,x,y) & x=y);
from this triple and 1. and 3. we can infer (by the "consequence rule")
the desired conclusion,
m,n are positive integers & x=m & y=n {B} x=gcd(m,n).
Guessing a useful loop invariant. There is no prescription for
coming up with useful loop invariants that could be first learned by
rote and then applied mechanically. Understanding why the program does
what it does and a bit of inspiration are two of the keys to success.
In our example, requirements 1,2, and 3 state that
gcd(x,y)=gcd(x,y-x)=gcd(x-y,y).What does not change while the values of x and y keep changing is the value of gcd(x,y); at the very beginning, we have x=m,y=n, and so gcd(x,y)=gcd(m,n); since gcd(x,y) remains invariant; these observations may suggest using
gcd(x,y)=gcd(m,n)as the desired P(m,n,x,y). This P satisfies requirements 1 and 2, but it misses requirement 3 by a hair: if x is an integer, then
gcd(x,x)= x if x is positive, gcd(x,x) is undefined if x=0, gcd(x,x)=-x if x is negative,and so gcd(x,x)=gcd(m,n) does not imply x=gcd(m,n). Fortunately, as x and y are changing, the larger of the two values gets decremented by the smaller, and so both of these values remain positive. To say it differently, "x,y are positive integers" is also a loop invariant. The predicate
x,y are positive integers & gcd(x,y)=gcd(m,n)has all three properties 1,2,3 required of the desired P(m,n,x,y).
A review of the argument. In the notation we have been using,
A denotes the program segment
x=m, y=n;
C denotes the program segment
if x < y then y=y-x else x=x-y end
B denotes the program segment
while x does not equal y do C end
and our entire program S is the concatenation of A and B. The argument
that we have developed involves the following Hoare triples:
(1) m,n are positive integers
{x=m, y=n}
x,y are positive integers & gcd(x,y)=gcd(m,n)
(2) x,y are positive integers & gcd(x,y)=gcd(m,n) & x < y
{y=y-x}
x,y are positive integers & gcd(x,y)=gcd(m,n)
(3) x,y are positive integers & gcd(x,y)=gcd(m,n) & x > y
{x=x-y}
x,y are positive integers & gcd(x,y)=gcd(m,n)
(4) x,y are positive integers & gcd(x,y)=gcd(m,n) & x does not equal y
{C}
x,y are positive integers & gcd(x,y)=gcd(m,n)
(5) x,y are positive integers & gcd(x,y)=gcd(m,n)
{B}
x,y are positive integers & gcd(x,y)=gcd(m,n) & x = y
(6) x,y are positive integers & gcd(x,y)=gcd(m,n)
{B}
x=gcd(m,n)
(7) m,n are positive integers
{S}
x=gcd(m,n)
Validity of Hoare triples (1),(2),(3) may be verified from scratch;
Hoare triple (4) may be inferred from Hoare triples (2) and (3); Hoare
triple (5) may be inferred from Hoare triple (4); Hoare triple (6) may
be inferred from Hoare triple (5); Hoare triple (7) may be inferred
from Hoare triples (1) and (6). Formally, (4) follows from (2) and (3)
by the rule of inference for the if-then-else
constructs (page 287); (5) follows from (4) by the rule of inference
for while loops (page 288); (7) follows from (1) and (6) by the
"composition rule" (page 286). To derive formally (6) from (5), one
may use the following rule of inference, half if which is mentioned in
the book as Exercise 11 on p. 200, and which helps to alleviate some
of the pedantry of formal proofs.
Consequence Rule:
From
p implies p'
p'{S}q'
q'implies q
we may infer
p{S}q
Another way of presenting the argument is to annotate the program by predicates in the variables m,n,x,y that hold at various checkpoints:
/* m,n are positive integers */
x=m, y=n;
/* now x,y are positive integers & gcd(x,y)=gcd(m,n) */
while x does not equal y
/* now x,y are positive integers & gcd(x,y)=gcd(m,n) & x does not equal y*/
do if x < y
then /* now x,y are positive integers & gcd(x,y)=gcd(m,n) & x < y */
y=y-x
/* now x,y are positive integers & gcd(x,y)=gcd(m,n) */
else /* now x,y are positive integers & gcd(x,y)=gcd(m,n) & x > y */
x=x-y
/* now x,y are positive integers & gcd(x,y)=gcd(m,n) */
end
/* now x,y are positive integers & gcd(x,y)=gcd(m,n) */
end
/* now x,y are positive integers & gcd(x,y)=gcd(m,n) & x = y; this implies
x=gcd(m,n) */
x=m, y=n, z=0;
while x > 0
do if x is even;
then x=x/2, y=2y;
else x=x-1, z=z+y;
end
end
Here is the proof that
m is a nonnegative integer & n is an integer {S} z=mn:
/* m is a nonnegative integer & n is an integer */
x=m, y=n, z=0;
/* now x is a nonnegative integer & xy+z=mn */
while x > 0
/* now x is a positive integer & xy+z=mn */
do if x is even
then /* now x is an even positive integer & xy+z=mn */
x=x/2, y=2y;
/* now x is a positive integer & xy+z=mn */
else /* now x is a positive integer & xy+z=mn */
x=x-1, z=z+y;
/* now x is a nonnegative integer & xy+z=mn */
end
/* now x is a nonnegative integer & xy+z=mn */
end
/* now x is a nonnegative integer & xy+z=mn & x is at most 0; this implies
z=mn */
x=m, y=n;
while y is not zero
do r=x mod y;
x=y;
y=r;
end
Here is a proof that
m,n are positive integers {S} x=gcd(m,n):
/* m > 0 & n is nonnegative */
x=m, y=n;
/* now x > 0 & y is nonnegative & gcd(x,y) = gcd(m,n) */
while y is not zero
/* now x > 0 & y > 0 & gcd(x,y) = gcd(m,n) */
do r=x mod y;
/* now r is nonnegative & y > 0 & gcd(r,y) = gcd(m,n) */
x=y;
/* now r is nonnegative & x > 0 & gcd(r,x) = gcd(m,n) */
y=r;
/* now y is nonnegative & x > 0 & gcd(y,x) = gcd(m,n) */
end
/* now x > 0 & y = 0 & gcd(x,y) = gcd(m,n),
which implies x = gcd(m,n) */
k=1,m=a[1];
while k < n
do k=k+1;
if a[k] > m then m=a[k] end
end
Here is a proof that
n is a positive integer {S} m is the largest of all a[1],a[2],...a[n]:
/* n is a positive integer */
k=1,m=a[1];
/* now k is at most n & m is the largest of all a[1],a[2],...a[k] */
while k < n
/* now k < n & m is the largest of all a[1],a[2],...a[k] */
do k=k+1;
/* now k is at most n & m is the largest of all a[1],a[2],...a[k-1] */
do if a[k] > m
then /* now k is at most n & m is the largest of all a[1],a[2],...a[k-1] & a[k] > m */
m=a[k];
/* now k is at most n & m is the largest of all a[1],a[2],...a[k] */
end
/* now k is at most n & m is the largest of all a[1],a[2],...a[k] */
end
/* now k is at least n & now k is at most n & m is the largest of all a[1],a[2],...a[k],
which implies that m is the largest of all a[1],a[2],...a[n] */