Weakest Liberal Precondition

program-proofing

Definition

Weakest Liberal Precondition

The weakest liberal precondition of a program and a postcondition is the weakest formula such that the Hoare triple is partially correct.

Equivalently, it is the set of states from which either does not terminate or terminates in a state satisfying :

If a precondition implies , then is partially correct.

Intuition

For an assignment

let be the state before the assignment and the state after it. By the semantics of assignment,

and every other variable keeps its old value.

Now suppose the desired postcondition is

We want a condition on the old state that is equivalent to saying that the new state satisfies this formula.

The statement

means

Using the assignment semantics, this becomes

which is exactly the old-state condition

Therefore,

So the substitution is not a trick. It is the syntactic way of expressing the semantic fact that the post-state value of is computed from the pre-state by the assignment.

Relation to WP

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., ).

Axiomatic Semantics

The wlp can be used to define the axiomatic semantics of a programming language (like SIMPLE) for partial correctness.

Sequencing

Loop

A loop can be expressed in two equivalent ways.

If is a loop invariant and is the loop guard, then one may annotate the body with the guard:

and conclude after the loop:

Equivalently, one can combine the invariant with the post-loop condition directly:

and obtain:

Examples

Conditional with abort

Empty Program

For the empty program, the wlp is simply the postcondition: