Slide 10.4: The weakest precondition wp

Slide 10.3: Applications of Hoare logic (cont.)
Slide 10.5: The weakest precondition wp (cont.)
Home

The Weakest Precondition wp

Again, the axiomatic specification of the semantics of the language construct C is of the form

     {P} C {Q}

where P and Q are assertions. Unfortunately, such a representation of the action of C is not unique and may not completely specify all the actions of C. For example,

The third example
```
   {y ≠ 0} x := 1 / y {x = 1 / y}
```
did not include in the postcondition the fact that y ≠ 0 continues to be true after the execution of the assignment.

↓↓↓
To specify completely the semantics of the assignment to x, we must somehow indicate that x is the only variable that changes under the assignment (unless it has aliases).

Also, y ≠ 0 is not the only condition that will guarantee the correct evaluation of the expression 1/y. y>0 or y<0 will do as well.

↓↓↓
Thus, writing an expected precondition and an expected postcondition will not always precisely determine the semantics of a construct.

What is needed is a way of associating to the construct C a general relation between precondition P and postcondition Q. The way to do this is to use the property that programming is a goal-oriented activity:

An activity that tends to achieve a goal and demonstrate it in subsequent actions.