Concepts of Programming Languages

3.5 Describing the Meanings of Programs: Dynamic Semantics 153

x1=E1

and

x2=E2

then we have

{P3x2SE2} x2=E2 {P3}
{(P3x2SE2)x1SE1} x1=E1 {P3x2SE2}

Therefore, the weakest precondition for the sequence x1 = E1; x2 = E2 with
postcondition P3 is {(P3x2SE2)x1SE1}.
For example, consider the following sequence and postcondition:

y = 3 * x + 1;
x = y + 3;
{x < 10}

The precondition for the second assignment statement is

y < 7

which is used as the postcondition for the first statement. The precondition for
the first assignment statement can now be computed:

3 * x + 1 < 7
x < 2

So, {x < 2} is the precondition of both the first statement and the two-
statement sequence.

3.5.3.5 Selection

We next consider the inference rule for selection statements, the general form
of which is

if B then S1 else S2

We consider only selections that include else clauses. The inference rule is

{B and P} S1 {Q}, {(not B) and P} S2{Q}

{P} if B then S1 else S2 {Q}

This rule indicates that selection statements must be proven both when the
Boolean control expression is true and when it is false. The first logical state-
ment above the line represents the then clause; the second represents the else