Page 394 - Discrete Mathematics and Its Applications

5.5 Program Correctness 373

EXAMPLE 1 Show that the program segment

y := 2
z := x + y
is correct with respect to the initial assertion p: x = 1 and the final assertion q: z = 3.

Solution: Suppose that p is true, so that x = 1 as the program begins. Then y is assigned the
value 2, and z is assigned the sum of the values of x and y, which is 3. Hence, S is correct with
respect to the initial assertion p and the final assertion q. Thus, p{S}q is true. ▲

Rules of Inference

A useful rule of inference proves that a program is correct by splitting the program into a
sequence of subprograms and then showing that each subprogram is correct.
Suppose that the program S is split into subprograms S 1 and S 2 .Write S = S 1 ; S 2 to indicate
that S is made up of S 1 followed by S 2 . Suppose that the correctness of S 1 with respect to the
initial assertion p and final assertion q, and the correctness of S 2 with respect to the initial
assertion q and the final assertion r, have been established. It follows that if p is true and S 1 is
executed and terminates, then q is true; and if q is true, and S 2 executes and terminates, then r
is true. Thus, if p is true and S = S 1 ; S 2 is executed and terminates, then r is true. This rule of
inference, called the composition rule, can be stated as

p{S 1 }q
q{S 2 }r
∴ p{S 1 ; S 2 }r.

This rule of inference will be used later in this section.
Next, some rules of inference for program segments involving conditional statements and
loops will be given. Because programs can be split into segments for proofs of correctness, this
will let us verify many different programs.

Conditional Statements

First, rules of inference for conditional statements will be given. Suppose that a program
segment has the form

if condition then
S

where S is a block of statements. Then S is executed if condition is true, and it is not executed
when condition is false.To verify that this segment is correct with respect to the initial assertion p
and final assertion q, two things must be done. First, it must be shown that when p is true and
condition is also true, then q is true after S terminates. Second, it must be shown that when p
is true and condition is false, then q is true (because in this case S does not execute).
This leads to the following rule of inference:

(p ∧ condition){S}q
(p ∧¬condition) → q
∴ p{if condition then S}q.