Section 1.6 Proof of Correctness
91
or
{n = 5 and n ≥ 10} y = 100 {y = 6}
holds. Remember that this stands for an implication, which will be true because its
antecedent, n = 5 and n ≥ 10, is false. We must also show that
{Q ` B′} P 2 {R}
or
{n = 5 and n < 10} y = n + 1 {y = 6}
holds. Working back from the postcondition, using the assignment rule, we get
{n + 1 = 6 or n = 5}
y = n + 1
{y = 6}
Thus
{n = 5} y = n + 1 {y = 6}
is true by the assignment rule and therefore
{n = 5 and n < 10} y = n + 1 {y = 6}
is also true because the condition n < 10 adds nothing new to the assertion. The
conditional rule allows us to conclude that the program segment is correct.
pRaCtiCe 33 Verify the correctness of the following program segment with the precondition and
postcondition shown.
{x = 4}
if x < 5 then
y = x − 1
else
y = 7
end if
{y = 3}
eXAMPLe 46
Verify the correctness of the following program segment to compute max(x, y), the
maximum of two distinct values x and y.
{x ∙ y}
if x >= y then
max = x
else
max = y
end if