PROGRAM CORRECTNESS
Course notes written by Vašek Chvátal
to supplement Section 3.6 of Kenneth H. Rosen, Discrete Mathematics and its Applications (5th edition)



Example 1

Let S denote the program
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; 
end
To 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;

in terms of Hoare triples, these two requirements can be stated as

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

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 is useful in the sense that

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

  1. P(m,n,m,n) for all choices of positive integers m and n,
  2. (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),
  3. P(m,n,x,x) implies x=gcd(m,n),
respectively. The input variables m and n are only read at the very beginning and then they are never seen again; their individual values are unimportant and only their gcd (featured in requirement 3) matters; variables x and y may change many times throughout the execution of the while loop. What property P(m,n,x,y) of the static values of m,n and the dynamic values of x,y remains unchanged (=invariant)? On the one hand, the values of x and y do not change in an arbitrary way: in each execution of C, either x is left alone and y replaced by y-x or y is left alone and x replaced by x-y. On the other hand, requirement 3 hints that the invariant property of x and y must be related to gcd(m,n). A missing link that relates the notion of gcd to the kind of changes that x and y are going through is the fact 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) */

Why the program terminates

Because x,y are positive integers and their sum gets smaller with each iteration of the while loop.


Example 2

Let S denote the program
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 */

Why the program terminates

Because x is a nonnegative integer and it gets smaller with each iteration of the while loop.


Example 3

Let S denote the Euclidean Algorithm (ALGORITHM 6 on p.179)
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) */

Why the program terminates

Because y is a nonnegative integer and it gets smaller with each iteration of the while loop.


Example 4

Let S denote the program
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] */

Why the program terminates

Because k is a nonnegative integer and it gets smaller with each iteration of the while loop.


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