Weakest Precondition

program-proofing

Definition

Weakest Precondition

The weakest precondition (WP) is the most general (least restrictive) formula $F^{\prime }$ such that the Hoare triple $\{F^{\prime }\}\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$.

Examples

Example: 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\}$$

Info

$\{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}$$