92
Formal Logic
The desired postcondition reflects the definition of the maximum, (x > y and
max = x) or (x < y and max = y). The two implications to prove are
{x ∙ y and x ≥ y} max = x {(x > y and max = x) or (x < y and max = y)}
and
{x ∙ y and x < y} max = y {(x > y and max = x) or (x < y and max = y)}
Using the assignment rule on the first case (substituting x for max in the postcondition) would give the precondition
(x > y ` x = x) ~ (x < y ` x = y)
Since the second disjunct is always false, this is equivalent to
(x > y ` x = x)
which in turn is equivalent to
x > y
or
x ∙ y and x ≥ y
The second implication is proved similarly.
In Chapter 2, we will see how to verify correctness for a loop statement,
where a section of code can be repeated many times.
As we have seen, proof of correctness involves a lot of detailed work. It is a
difficult tool to apply to large programs that already exist. It is generally easier
to prove correctness while the program is being developed. Indeed, the list of
assertions from beginning to end specifies the intended behavior of the program
and can be used early in its design. In addition, the assertions serve as valuable
documentation after the program is complete.
S e c t I o n 1 . 6 Review
tecHnIQueS
• Verify the correctness of a program segment that
includes assignment statements.
• Verify the correctness of a program segment that
includes conditional statements.
MAIn IdeA
• A formal system of rules of inference can be used
to prove the correctness of program segments.
W
W
eXeRcISeS 1.6
In the following exercises, * denotes multiplication.
1. According to the assignment rule, what is the precondition in the following program segment?
{precondition}
x = x + 1
{x = y − l}