Section 1.6 Proof of Correctness
87
assignment rule
Suppose that statement s i is an assignment statement of the form x = e, that is, the
variable x takes on the value of e, where e is some expression. The Hoare triple to
prove correctness of this one statement has the form
{R i } x = e {R i+l }
For this triple to be valid, the assertions R i and R i+1 must be related in a particular way.
eXAMPLe 41
Consider the following assignment statement together with the given precondition
and postcondition:
{x – 1 > 0}
x = x – 1
{x > 0}
For every x, if x – 1 > 0 before the statement is executed (note that this says that
x > 1), then after the value of x is reduced by 1, it will be the case that x > 0.
Therefore,
{x – 1 > 0} x = x – 1 {x > 0}
is valid.
In Example 41, we just reasoned our way through the validity of the wff represented
by the Hoare triple. The point of predicate logic is to allow us to determine validity
in a more mechanical fashion by the application of rules of inference. (After all,
we don’t want to just “reason our way through” the entire program to convince
ourselves of its correctness; the programmer already did that when the program
was written!)
The appropriate rule of inference for assignment statements is the assignment
rule, given in Table 1.18. It says that if the precondition and postcondition are
appropriately related, the Hoare triple can be inserted at any time in a proof sequence
without having to be inferred from something earlier in the proof sequence. This
makes the Hoare triple for an assignment statement akin to a hypothesis in our
previous proofs. And what is the relationship? In the postcondition, locate all
instances of the variable to which an assignment is being made in the assignment
statement right above the postcondition. For each of those instances, substitute the
expression being assigned. The result will be the precondition.
tAbLe 1.18
from
can derive
name of Rule
Restrictions on use
{R i }s i {R i+l }
assignment
1. s i has the form x = e.
2. R i is R i+1 with e substituted
everywhere for x.
87
assignment rule
Suppose that statement s i is an assignment statement of the form x = e, that is, the
variable x takes on the value of e, where e is some expression. The Hoare triple to
prove correctness of this one statement has the form
{R i } x = e {R i+l }
For this triple to be valid, the assertions R i and R i+1 must be related in a particular way.
eXAMPLe 41
Consider the following assignment statement together with the given precondition
and postcondition:
{x – 1 > 0}
x = x – 1
{x > 0}
For every x, if x – 1 > 0 before the statement is executed (note that this says that
x > 1), then after the value of x is reduced by 1, it will be the case that x > 0.
Therefore,
{x – 1 > 0} x = x – 1 {x > 0}
is valid.
In Example 41, we just reasoned our way through the validity of the wff represented
by the Hoare triple. The point of predicate logic is to allow us to determine validity
in a more mechanical fashion by the application of rules of inference. (After all,
we don’t want to just “reason our way through” the entire program to convince
ourselves of its correctness; the programmer already did that when the program
was written!)
The appropriate rule of inference for assignment statements is the assignment
rule, given in Table 1.18. It says that if the precondition and postcondition are
appropriately related, the Hoare triple can be inserted at any time in a proof sequence
without having to be inferred from something earlier in the proof sequence. This
makes the Hoare triple for an assignment statement akin to a hypothesis in our
previous proofs. And what is the relationship? In the postcondition, locate all
instances of the variable to which an assignment is being made in the assignment
statement right above the postcondition. For each of those instances, substitute the
expression being assigned. The result will be the precondition.
tAbLe 1.18
from
can derive
name of Rule
Restrictions on use
{R i }s i {R i+l }
assignment
1. s i has the form x = e.
2. R i is R i+1 with e substituted
everywhere for x.