152 Chapter 3 Describing Syntax and Semantics
To use this in a proof, an inference rule, named the rule of consequence, is
needed. The form of the rule of consequence is{P} S {Q}, P=> P, Q => Q
{P} S {Q}The => symbol means “implies,” and S can be any program statement. The rule
can be stated as follows: If the logical statement {P} S {Q} is true, the assertion
P implies the assertion P, and the assertion Q implies the assertion Q, then it
can be inferred that {P} S {Q}. In other words, the rule of consequence says
that a postcondition can always be weakened and a precondition can always be
strengthened. This is quite useful in program proofs. For example, it allows the
completion of the proof of the last logical statement example above. If we let P
be {x > 3}, Q and Q be {x > 0}, and P be {x > 5}, we have{x>3}x = x–3{x>0},(x>5) => {x>3},(x>0) => (x>0)
{x>5}x=x–3{x>0}The first term of the antecedent ({x > 3} x = x – 3 {x > 0}) was proven
with the assignment axiom. The second and third terms are obvious. There-
fore, by the rule of consequence, the consequent is true.3.5.3.4 Sequences
The weakest precondition for a sequence of statements cannot be described by
an axiom, because the precondition depends on the particular kinds of state-
ments in the sequence. In this case, the precondition can only be described with
an inference rule. Let S1 and S2 be adjacent program statements. If S1 and S2
have the following pre- and postconditions{P1} S1 {P2}
{P2} S2 {P3}the inference rule for such a two-statement sequence is{P1} S1 {P2}, {P2} S2 {P3}
{P1} S1, S2 {P3}
So, for our example, {P1} S1; S2 {P3} describes the axiomatic semantics of
the sequence S1; S2. The inference rule states that to get the sequence pre-
condition, the precondition of the second statement is computed. This new
assertion is then used as the postcondition of the first statement, which can
then be used to compute the precondition of the first statement, which is
also the precondition of the whole sequence. If S1 and S2 are the assignment
statements