Section 1.6 Proof of Correctness
89
At the beginning of this program segment, x and y have certain values. Thus
we may express the actual precondition as x = a and y = b. The desired postcondition is then x = b and y = a. Using the assignment rule, we can work backward
from the postcondition to find the earlier assertions (read the following from the
bottom to the top).
{y = b, x = a}
temp = x
{y = b, temp = a}
x = y
{x = b, temp = a}
y = temp
{x = b, y = a}
The first assertion agrees with the precondition; the assignment rule, applied
repeatedly, assures us that the program segment is correct.
pRaCtiCe 32 Verify the correctness of the following program segment with the precondition and postcondition shown:
hx = 3}
y = 4
z = x + y
hz = 7j
Sometimes the necessary precondition is trivially true, as shown in the next
example.
eXAMPLe 44
Verify the correctness of the following program segment to compute y = x − 4.
y = x
y = y − 4
Here the desired postcondition is y = x − 4. Using the assignment rule to work
backward from the postcondition, we get (again, read bottom to top)
{x − 4 = x − 4}
y = x
{y − 4 = x − 4}
y = y − 4
{y = x − 4}
The precondition is always true; therefore, by the assignment rule, each successive
assertion, including the postcondition, is true.