88
Formal Logic
eXAMPLe 42
For the case of Example 41,
{x − 1 > 0}
x = x − 1
{x > 0}
the triple
{x − 1 > 0} x = x − 1 {x > 0}
is valid by the assignment rule. The postcondition is
x > 0
Substituting x − 1 for x throughout the postcondition results in
x − 1 > 0 or x > 1
which is the precondition. Here we didn’t have to think at all; we just checked that
the assignment rule had been followed.
Certainly Example 41 seems easier than Example 42, and for such a trivial
case you may be tempted to skip use of the assignment inference rule and just
talk your way through the code. Resist this temptation. For one thing, real-world
usage isn’t this trivial. But more to the point, just as in our previous formal logic
systems, you want to rely on the rules of inference instead of on some possibly
flawed thought process.
pRaCtiCe 31 According to the assignment rule, what should be the precondition in the following
program segment?
{precondition}
x = x − 2
{x = y}
Because the assignment rule tells us what a precondition should look like
based on what a postcondition looks like, a proof of correctness often begins with
the final desired postcondition and works its way back up through what the earlier
assertions should look like according to the assignment rule. Once it has been
determined what the topmost assertion must be, a check is done to see that this
assertion is really true.
ReMIndeR
To use the assignment
rule, work from the bottom
to the top.
eXAMPLe 43
Verify the correctness of the following program segment to exchange the values of
x and y:
temp = x
x = y
y = temp