Strongest Postcondition

program-proofing

Definition

Strongest Postcondition

The strongest postcondition (SP), denoted as $\text{sp}(F,\Pi )$, is the most specific (most restrictive) formula $G^{\prime }$ such that the Hoare triple $\{F\}\Pi \{G^{\prime }\}$ is partially correct.

Formal Semantics

In terms of the set of states $\mathcal{S}$, the SP represents the image of the set of states satisfying $F$ under the execution of $\Pi$:

$$\begin{array}{rl}\{\text{sp}(F,\Pi )\}& =\{[\Pi ]\sigma \mid \sigma \in \{F\}\text{ and }[\Pi ]\sigma \text{ defined}\}\\ & =[\Pi ](\{F\})\end{array}$$

Correctness Relation

A specification $\{F\}\Pi \{G\}$ is partially correct if and only if the strongest postcondition implies the desired postcondition $G$:

$$\{F\}\Pi \{G\}\text{ partially correct}⟺\{\text{sp}(F,\Pi )\}\subseteq \{G\}⟺\text{sp}(F,\Pi )⟹G\text{ is valid}$$

Base Cases

For the empty program, the strongest postcondition is simply the precondition:

• $\text{sp}(F,\mathbf{skip})=F$

Axiomatic Semantics

Similarly to the wlp, the strongest postcondition can be used to define the axiomatic semantics of a programming language for partial correctness.

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 partially correct:

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

Info

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

$$\begin{array}{rl}\mathrm{sp}(F,v:=e)& =\exists v^{\prime }(F[v^{\prime }/v]\wedge v=e[v^{\prime }/v])\\ & \\ \mathrm{sp}(F,\Pi ;\Omega )& =\mathrm{sp}(\mathrm{sp}(F,\Pi ),\Omega )\end{array}$$

$$\begin{array}{rl}\mathrm{sp}(P,t:=x;x:=y;y:=t)& =\mathrm{sp}(\mathrm{sp}(P,t:=x),x:=y;y:=t)\\ & =\mathrm{sp}(\exists t^{\prime }(P[t^{\prime }/t]\wedge t=x[t^{\prime }/t]),x:=y;y:=t)\\ & =\mathrm{sp}(\exists t^{\prime }(P\wedge t=x),x:=y;y:=t)\\ & =\mathrm{sp}(P\wedge t=x,x:=y;y:=t)\\ & \\ & =\mathrm{sp}(\mathrm{sp}(P\wedge t=x,x:=y),y:=t)\\ & =\mathrm{sp}(\exists x^{\prime }((P\wedge t=x)[x^{\prime }/x]\wedge x=y[x^{\prime }/x]),y:=t)\\ & =\mathrm{sp}(\exists x^{\prime }(x^{\prime }=x_0\wedge y=y_0\wedge t=x^{\prime }\wedge x=y),y:=t)\\ & =\mathrm{sp}(\exists x^{\prime }(x^{\prime }=x_0\wedge y=y_0\wedge t=x_0\wedge x=y),y:=t)\\ & =\mathrm{sp}(y=y_0\wedge t=x_0\wedge x=y\wedge \exists x^{\prime }(x^{\prime }=x_0),y:=t)\\ & =\mathrm{sp}(y=y_0\wedge t=x_0\wedge x=y,y:=t)\\ & \\ & =\exists y^{\prime }((y=y_0\wedge t=x_0\wedge x=y)[y^{\prime }/y]\wedge y=t[y^{\prime }/y])\\ & =\exists y^{\prime }(y^{\prime }=y_0\wedge t=x_0\wedge x=y^{\prime }\wedge y=t)\\ & =(t=x_0\wedge x=y_0\wedge y=t\wedge \exists y^{\prime }(y^{\prime }=y_0))\\ & =(t=x_0\wedge x=y_0\wedge y=t)\end{array}$$

Further, we can show that the computed postcondition implies $Q$:

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