Slide 10.6: The weakest precondition wp (cont.)

Slide 10.5: The weakest precondition wp (cont.)
Slide 10.7: General properties of wp
Home

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:

Our running example of the assignment can now be restated as follows:
```
     wp( x := 1/y,  x = 1/y ) = ( y ≠ 0 )
```
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.

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.