In each code fragment, assume the program executes the statement,
and that makes the boolean expression in the following comment true.
Write a boolean expression that must be true before the program
executes the statement in order for this to be so.
a.
// true
x = 4
// x == 4
| b.
// x > 2
x = x + 3
// x > 5
c.
// x > 3
x = x + i
// x > i + 3
| |
In each case, I show the weakest (most general) boolean expression
that must be true to ensure that the following statement causes the
final expression to be true. (By weakest, I mean the one that
allows the largest range of values for x
.) There are
many other correct answers where the expressions are stronger. In a.,
any initial boolean expression at all is correct, since the final expression
does not depend on the initial expression. In b., x == 3
(or
any number larger than 2) is correct.
The expression before the statement is called the
precondition and the expression after is called the
postcondition. My solutions show the weakest
precondition. These examples are simple enough to see the
weakest precondition by intuition (or trial and error), but it is
always possible to calculate the weakest precondition for an
assignment statement by substituting the expression on the right side
of the assignment for the same variable in the postcondition. For
example in c., substituting x + i
for x
in
x > i + 3
yields (x + i) > i + 3
, which is
equivalent to x > 3
. This same procedure can be used to
confirm the correctness of the solutions to problems 3. and 4.
Calculating the weakest precondition
of a statement (or block of statements) is used extensively in proving
code correct, or deriving code from a specification.