Weakest Liberal Precondition

program-proofing

Definition

Weakest Liberal Precondition

The weakest liberal precondition of a program $\Pi$ and a postcondition $G$ is the weakest formula $\mathrm{wlp}(\Pi ,G)$ such that the Hoare triple $\{\mathrm{wlp}(\Pi ,G)\}\Pi \{G\}$ is partially correct.

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

$$\begin{array}{rl}\{\mathrm{wlp}(\Pi ,G)\}& =\{\sigma \in \mathcal{S}\mid [\Pi ]\sigma \text{ undefined or }[\Pi ]\sigma \in \{G\}\}\\ & =\{\sigma \in \mathcal{S}\mid [\Pi ]\sigma \text{ undefined}\}\cup [\Pi {]}^{-1}(\{G\})\end{array}$$

If a precondition $F$ implies $\mathrm{wlp}(\Pi ,G)$, then $\{F\}\Pi \{G\}$ is partially correct.

Intuition

For an assignment

$$y:=y-1$$

let $\sigma$ be the state before the assignment and ${\sigma }^{\prime }$ the state after it. By the semantics of assignment,

$${\sigma }^{\prime }(y)=\sigma (y)-1$$

and every other variable keeps its old value.

Now suppose the desired postcondition is

$$xy+z=c$$

We want a condition on the old state $\sigma$ that is equivalent to saying that the new state ${\sigma }^{\prime }$ satisfies this formula.

The statement

$${\sigma }^{\prime }\models xy+z=c$$

means

$$x^{{\sigma }^{\prime }}{y}^{{\sigma }^{\prime }}+z^{{\sigma }^{\prime }}=c^{{\sigma }^{\prime }}$$

Using the assignment semantics, this becomes

$$x^{\sigma }(y^{\sigma }-1)+z^{\sigma }=c^{\sigma }$$

which is exactly the old-state condition

$$x(y-1)+z=c$$

Therefore,

$$\mathrm{wlp}(y:=y-1,xy+z=c)=x(y-1)+z=c$$

So the substitution $[y-1/y]$ is not a trick. It is the syntactic way of expressing the semantic fact that the post-state value of $y$ 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:

$$\text{wp}(\Pi ,G)=\text{wlp}(\Pi ,G)\wedge \text{terminates}(\Pi )$$

Verification Method

To verify that a program $\Pi$ satisfies a specification $\{F\}\Pi \{G\}$, one can:

1. Calculate the weakest precondition $F^{\prime }$ from the program $\Pi$ and the postcondition $G$.
2. Show that the actual precondition $F$ implies $F^{\prime }$ (i.e., $F⟹F^{\prime }$).

Axiomatic Semantics

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

Sequencing

$$\text{wlp}(\Pi ;\Omega ,G)=\text{wlp}(\Pi ,\text{wlp}(\Omega ,G))$$

Loop

A loop can be expressed in two equivalent ways.

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

$$\{Inv\wedge e\}\Pi \{Inv\}$$

and conclude after the loop:

$$\{Inv\}\mathbf{while}e\mathbf{do}\Pi \mathbf{od}\{Inv\wedge \neg e\}$$

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

$$\{Inv\wedge e\wedge t=t_0\}\Pi \{Inv\wedge 0<t\le t_0\}$$

and obtain:

$$\{Inv\}\mathbf{while}e\mathbf{do}\Pi \mathbf{od}\{Inv\wedge \neg e\}$$

Examples

Conditional with abort

$$\text{wlp}(\text{if }x\ge 0\text{ then skip else abort fi},x>2)$$ $$=(x\ge 0\wedge \text{wlp}(\text{skip},x>2))\vee (x<0\wedge \text{wlp}(\text{abort},x>2))$$ $$=(x\ge 0\wedge x>2)\vee (x<0\wedge 1)$$ $$=x>2\vee x<0$$

Empty Program

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

$$\text{wlp}(\mathbf{skip},G)=G$$