Weakest Precondition

program-proofing

Definition

Weakest Precondition

The weakest precondition of a program and a postcondition is the most general (least restrictive) formula such that the Hoare triple is totally correct.

Equivalently, characterises exactly the states from which terminates in a state satisfying .

If a precondition implies , then is totally correct.

Relation to WLP

The weakest precondition is more restrictive than the weakest liberal precondition because it must also guarantee termination:

Verification Method

To verify that a program satisfies a specification , one can:

1. Calculate the weakest precondition from the program and the postcondition .
2. Show that the actual precondition implies (i.e., ).

Informative Power

If , then is stronger than . By proving this implication, we ensure that provides enough information/constraints to guarantee that the program ends in a state satisfying .

Sequencing

Abort

For the abort command, there is no terminating execution. Therefore, the weakest precondition is false:

If a specification is totally correct, then must be false. Otherwise, the program would have to terminate and satisfy , which it cannot do.

Examples

Conditional with abort

Swapping values

Let be two conditions with:

Show that following Hoare triple is totally correct:

Observation

is totally correct if .

Further, we can show that the computed precondition is implied by :