Weakest Precondition

program-proofing

Definition

Weakest Precondition

The weakest precondition of a program $\Pi$ and a postcondition $G$ is the most general (least restrictive) formula $\mathrm{wp}(\Pi ,G)$ such that the Hoare triple $\{\mathrm{wp}(\Pi ,G)\}\Pi \{G\}$ is totally correct.

Equivalently, $\mathrm{wp}(\Pi ,G)$ characterises exactly the states from which $\Pi$ terminates in a state satisfying $G$.

$$\{\mathrm{wp}(\Pi ,G)\}=\{\sigma \in \mathcal{S}\mid [\Pi ]\sigma \text{ is defined and }[G]([\Pi ]\sigma )=\text{true}\}$$

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

Relation to WLP

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 }$).

Informative Power

If $F⟹F^{\prime }$, then $F$ is stronger than $F^{\prime }$. By proving this implication, we ensure that $F$ provides enough information/constraints to guarantee that the program ends in a state satisfying $G$.

Sequencing

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

Abort

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

$$\text{wp}(\mathbf{abort},G)=0$$

If a specification $\{F\}\mathbf{abort}\{G\}$ is totally correct, then $F$ must be false. Otherwise, the program would have to terminate and satisfy $G$, which it cannot do.

Examples

Conditional with abort

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

Swapping values

Let $P,Q$ be two conditions with:

$$\begin{array}{rl}P:& x=x_0\wedge y=y_0\\ Q:& x=y_0\wedge y=x_0\end{array}$$

Show that following Hoare triple is totally correct:

$$\{P\}t:=x;x:=y;y:=t\{Q\}$$

$\{F\}\Pi \{G\}$ is totally correct if $F\Rightarrow \mathrm{wp}(\Pi ,G)$.

$$\begin{array}{rl}\mathrm{wp}(v:=e,G)& =G[e/v]\\ \mathrm{wp}(\Pi ;\Omega ,G)& =\mathrm{wp}(\Pi ,\mathrm{wp}(\Omega ,G))\end{array}$$

$$\begin{array}{rl}\mathrm{wp}(t:=x;x:=y;y:=t,Q)& =\mathrm{wp}(t:=x;x:=y,\mathrm{wp}(y:=t,Q))\\ & =\mathrm{wp}(t:=x;x:=y,Q[t/y])\\ & =\mathrm{wp}(t:=x,wp(x:=y,Q[t/y]))\\ & =\mathrm{wp}(t:=x,Q[t/y][y/x])\\ & =Q[t/y][y/x][x/t]\end{array}$$

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

$$\begin{array}{rlrl}P& \Rightarrow Q[t/y][y/x][x/t]& & \\ (x=x_0\wedge y=y_0)& \Rightarrow (x=y_0\wedge y=x_0)[t/y][y/x][x/t]& & \\ (x=x_0\wedge y=y_0)& \Rightarrow (x=y_0\wedge t=x_0)[y/x][x/t]& & \\ (x=x_0\wedge y=y_0)& \Rightarrow (y=y_0\wedge t=x_0)[x/t]& & \\ (x=x_0\wedge y=y_0)& \Rightarrow (y=y_0\wedge x=x_0)& & \square \end{array}$$