Page 396 - Discrete Mathematics and Its Applications

5.5 Program Correctness 375

Example 3 illustrates how this rule of inference is used.
EXAMPLE 3 Verify that the program segment

if x< 0 then
abs := −x
else
abs := x

is correct with respect to the initial assertion T and the final assertion abs =|x|.

Solution: Two things must be demonstrated. First, it must be shown that if the initial assertion is
true and x< 0, then abs =|x|. This is correct, because when x< 0 the assignment statement
abs := −x sets abs =−x, which is |x| by definition when x< 0. Second, it must be shown
that if the initial assertion is true and x< 0 is false, so that x ≥ 0, then abs =|x|. This is also
correct, because in this case the program uses the assignment statement abs := x, and x is |x|
by definition when x ≥ 0, so abs := x. Hence, using the rule of inference for program segments
of this type, this segment is correct with respect to the given initial and final assertions. ▲

Loop Invariants

Next, proofs of correctness of while loops will be described. To develop a rule of inference for
program segments of the type

while condition
S

note that S is repeatedly executed until condition becomes false. An assertion that remains true
each time S is executed must be chosen. Such an assertion is called a loop invariant. In other
words, p is a loop invariant if (p ∧ condition){S}p is true.
Suppose that p is a loop invariant. It follows that if p is true before the program segment is
executed, p and ¬condition are true after termination, if it occurs. This rule of inference is

(p ∧ condition){S}p
∴ p{while condition S}(¬ condition ∧ p).

The use of a loop invariant is illustrated in Example 4.
EXAMPLE 4 A loop invariant is needed to verify that the program segment

i := 1
factorial := 1
while i< n
i := i + 1
factorial := factorial · i

terminates with factorial = n! when n is a positive integer.