Page 397 - Discrete Mathematics and Its Applications

376 5 / Induction and Recursion

Let p be the assertion “factorial = i! and i ≤ n.” We first prove that p is a loop invariant.
Suppose that, at the beginning of one execution of the while loop, p is true and the condition of
the while loop holds; in other words, assume that factorial = i! and that i< n. The new values
i new and factorial new of i and factorial are i new = i + 1 and factorial new = factorial · (i + 1) =
(i + 1)!= i new !. Because i< n, we also have i new = i + 1 ≤ n. Thus, p is true at the end of
the execution of the loop. This shows that p is a loop invariant.
Now we consider the program segment. Just before entering the loop, i = 1 ≤ n and
factorial = 1 = 1!= i! both hold, so p is true. Because p is a loop invariant, the rule of infer-
ence just introduced implied that if the while loop terminates, it terminates with p true and with
i< n false. In this case, at the end, factorial = i! and i ≤ n are true, but i< n is false; in other
words, i = n and factorial = i!= n!, as desired.
Finally, we need to check that the while loop actually terminates. At the beginning of the
program i is assigned the value 1, so after n − 1 traversals of the loop, the new value of i will
be n, and the loop terminates at that point. ▲

A final example will be given to show how the various rules of inference can be used to
verify the correctness of a longer program.
EXAMPLE 5 We will outline how to verify the correctness of the program S for computing the product of
two integers.

procedure multiply(m, n: integers)

if n< 0 then a := −n
S 1
else a := n

k := 0
S 2
x := 0
⎧
⎨while k< a
S 3 x := x + m
k := k + 1
⎩

if n< 0 then product := −x
S 4
else product := x
return product
{product equals mn}

The goal is to prove that after S is executed, product has the value mn. The proof of correctness
can be carried out by splitting S into four segments, with S = S 1 ; S 2 ; S 3 ; S 4 , as shown in the
listing of S. The rule of composition can be used to build the correctness proof. Here is how the
argument proceeds. The details will be left as an exercise for the reader.
Let p be the initial assertion “m and n are integers.”Then, it can be shown that p{S 1 }q is true,
when q is the proposition p ∧ (a =|n|). Next, let r be the proposition q ∧ (k = 0) ∧ (x = 0).It
is easily verified that q{S 2 }r is true. It can be shown that “x = mk and k ≤ a” is an invariant for
the loop in S 3 . Furthermore, it is easy to see that the loop terminates after a iterations, with k = a,
so x = ma at this point. Because r implies that x = m · 0 and 0 ≤ a, the loop invariant is true
before the loop is entered. Because the loop terminates with k = a, it follows that r{S 3 }s is true
where s is the proposition “x = ma and a =|n|.” Finally, it can be shown that S 4 is correct with
respect to the initial assertion s and final assertion t, where t is the proposition “product = mn.”
Putting all this together, because p{S 1 }q, q{S 2 }r, r{S 3 }s, and s{S 4 }t are all true, it fol-
lows from the rule of composition that p{S}t is true. Furthermore, because all four segments
terminate, S does terminate. This verifies the correctness of the program. ▲