Course notes written by Vašek Chvátal

to supplement Section 3.6 of Kenneth H. Rosen, Discrete Mathematics and its Applications (5th edition)

x=m, y=n;We want to prove thatwhilex does not equal ydoifx < ytheny=y-x;elsex=x-y;endend

m,n are positive integers {S} x=gcd(m,n).

x=m, y=n;and let B denote the program segment

Trivially, we havewhilex does not equal ydoifx < ytheny=y-x;elsex=x-y;endend

m,n are positive integers {A} m,n are positive integers & x=m & y=nand so our job reduces to proving that

m,n are positive integers & x=m & y=n {B} x=gcd(m,n).

as C, so that B can be recorded asifx < ytheny=y-x;elsex=x-y;end

To prove thatwhilex does not equal ydoC;end

m,n are positive integers & x=m & y=n {B} x=gcd(m,n),we have to come up with a suitable

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 thatP(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).

In our example, requirements 1,2, and 3 state that

- P(m,n,m,n) for all choices of positive integers m and n,
- (x < y & P(m,n,x,y)) implies P(m,n,x,y-x) and

(y < x & P(m,n,x,y)) implies P(m,n,x-y,y), - P(m,n,x,x) implies x=gcd(m,n),

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 segmentand our entire program S is the concatenation of A and B. The argument that we have developed involves the following Hoare triples:ifx < ytheny=y-xelsex=x-yendB denotes the program segmentwhilex does not equal ydoCend

(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

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)*/whilex does not equal y /*now x,y are positive integers & gcd(x,y)=gcd(m,n) & x does not equal y*/doifx < ythen/*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;Here is the proof thatwhilex > 0doifx is even;thenx=x/2, y=2y;elsex=x-1, z=z+y;endend

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*/whilex > 0 /*now x is a positive integer & xy+z=mn*/doifx is eventhen/*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;Here is a proof thatwhiley is not zerodor=x mod y; x=y; y=r;end

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)*/whiley is not zero /*now x > 0 & y > 0 & gcd(x,y) = gcd(m,n)*/dor=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];Here is a proof thatwhilek < ndok=k+1;ifa[k] > mthenm=a[k]endend

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]*/whilek < n /*now k < n & m is the largest of all a[1],a[2],...a[k]*/dok=k+1; /*now k is at most n & m is the largest of all a[1],a[2],...a[k-1]*/doifa[k] > mthen/*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]*/

Back to the table of contents of Vašek Chvátal's course notes