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
y ≠ 0, or y > 0, ory < 0.
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)