Strongest Postcondition

program-proofing

Definition

Strongest Postcondition

The strongest postcondition of a program $\Pi$ and a precondition $F$ is the most specific (most restrictive) formula $\mathrm{sp}(F,\Pi )$ such that the Hoare triple $\{F\}\Pi \{\mathrm{sp}(F,\Pi )\}$ is partially correct.

Equivalently, it is the set of states reached by executing $\Pi$ from states satisfying $F$:

$$\{\mathrm{sp}(F,\Pi )\}=\{[\Pi ]\sigma \mid \sigma \in \{F\}\text{ and }[\Pi ]\sigma \text{ is defined}\}$$ $$=[\Pi ](\{F\})$$

If a postcondition $G$ is implied by $\mathrm{sp}(F,\Pi )$, then $\{F\}\Pi \{G\}$ 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.

Sequencing

$$\text{sp}(F,\Pi ;\Omega )=\text{sp}(\text{sp}(F,\Pi ),\Omega )$$

Examples

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

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

Assignment with fresh variable

For an assignment $v:=e$, if $v$ does not occur in the precondition $F$ and $v$ does not occur in the expression $e$, then

$$\mathrm{sp}(F,v:=e)=F\wedge v=e$$

This is the simple case where the new value of the assigned variable can be added directly.

Examples

• $\{x=2\}y:=3\{x=2\wedge y=3\}$
• $\{x=2\}x:=3\{x=2\wedge x=3\}$ is not a valid simplification, because $x$ is overwritten.
• $\{x=2\}y:=y+1\{x=2\wedge y=y+1\}$ is not a valid simplification, because $y$ occurs in $e$.

If the freshness condition does not hold, one has to remember the old value of the assigned variable using a fresh existentially quantified variable.