Slide 10.4: The weakest precondition wp
Slide 10.6: The weakest precondition wp (cont.)
Home

The Weakest Precondition wp (Cont.)

We usually know what we want to be true after the execution of a statement or program, and the question is whether the known conditions before the execution will guarantee that this becomes true. Thus, postcondition Q is assumed to be given, and a specification of the semantics of C becomes a statement of which preconditions P of C have the property that 
     {P} C {Q}
In general, given an assertion Q, there are many assertions P with the property that {P} C {Q}. One example has been given: For 1/y to be evaluated, we may require that There is one precondition P, however, that is the most general or weakest assertion with the property that {P} C {Q}. This is called the weakest precondition of postcondition Q and construct C and is written wp(C, Q). In our example, y ≠ 0 is clearly the weakest precondition such that 1/y can be evaluated. Both y > 0 and y < 0 are stronger than y ≠ 0 since they both imply y ≠ 0. Indeed,
P is by definition weaker than R if R implies P (written in logical form as R → P).
That is a statement R → P means that whenever R is true, P is true also. For example, if R is the statement, “x is in Illinois,” and P is the statement “x is in the United States,” then R → P is the statement, “If x is in Illinois, then x is in the United States.” Using these definitions we have the following restatement of the property {P} C {Q}: 
     {P} C {Q} if and only if P → wp(C, Q)