The Weakest Precondition wp (Cont.)

Finally, we define the axiomatic semantics of the language construct C as the function wp(C, _) from assertions to assertions. This function is a predicate transformer in that it takes a predicate as argument and returns a predicate result. A predicate is explained as follows:
For instance, {x | x is a positive integer less than 4} is the set {1, 2, 3}. Thus, an element of {x | S(x)} is an object t for which the statement S(t) is true. Such a sentence S(x) is called a predicate.
It also appears to work backward, in that it computes the weakest precondition from any postcondition. Three examples of finding the weakest precondition wp are as follows:
  1. Our running example of the assignment can now be restated as follows: 
         wp( x := 1/y,  x = 1/y ) = ( y ≠ 0 )
  2. As another example, consider the assignment x := x + 1 and the postcondition x > 0: 
         wp( x := x + 1,  x > 0 ) = ( x > -1 )
    In other words, for x to be greater than 0 after the execution of x := x + 1, x must be great than -1 just prior to execution.

  3. On the other hand, if we have no condition on x but simply want to state its value, we have 
         wp( x := x + 1,  x = A ) = ( x = A – 1 )
Again, this may seem backward, but a little reflection should convince you of its correctness.