Hoare Logic Basics

Hoare logic is a way of inserting annotations into code to make proofs about program behavior simpler. We first explain them using sets and relations.

Example Proof

//{0 <= y}
i = y;
//{0 <= y & i = y}
r = 0;
//{0 <= y & i = y & r = 0}
while //{r = (y-i)*x & 0 <= i}
 (i > 0) (
  //{r = (y-i)*x & 0 < i}
  r = r + x;
  //{r = (y-i+1)*x & 0 < i}
  i = i - 1
  //{r = (y-i)*x & 0 <= i}
)
//{r = x * y}

Hoare Triple for Sets and Relations

When $P, Q \subseteq S$ (sets of states) and $r \subseteq S\times S$ (relation on states, command semantics) then Hoare triple

$\begin{equation*} \{P \}\ r\ \{ Q \} \end{equation*}$

means

$\begin{equation*} \forall s,s' \in S. \left( s \in P \land (s,s') \in r \rightarrow s' \in Q \right) \end{equation*}$

We call $P$ precondition and $Q$ postcondition.

Note: weakest conditions (predicates) correspond to largest sets; strongest conditions (predicates) correspond to smallest sets that satisfy a given property (Graphically, a stronger condition $x > 0 \land y > 0$ denotes one quadrant in plane, whereas a weaker condition $x > 0$ denotes the entire half-plane.)

Strongest Postcondition - sp

Definition: for $P \subseteq S$ , $r \subseteq S\times S$ ,

$\begin{equation*} sp(P,r) = \{ s' \mid \exists s. s \in P \land (s,s') \in r \} \end{equation*}$

This is simply Relation Image of a set.

Lemma: Characterization of sp

$sp(P,r)$ is the the smallest set $Q$ such that $\{P\}r\{Q\}$ , that is:

$\{P\} r \{ sp(P,r) \}$
$\forall Q \subseteq S.\ \{P\} r \{Q\} \rightarrow sp(P,r) \subseteq Q$

Backward Propagation of Errors

If we have a relation $r$ and a set of errors $E$ , we can check if program meets specification by checking:

$\begin{equation*} sp(P,r) \cap E = \emptyset \end{equation*}$

$\begin{equation*} \forall y. \lnot (y \in sp(P,r) \land y \in E) \end{equation*}$

$\begin{equation*} \forall y.\ \lnot ((\exists x. P(x) \land (x,y) \in r) \land y \in E) \end{equation*}$

$\begin{equation*} \forall y.\ \lnot \exists x. (P(x) \land (x,y) \in r \land y \in E) \end{equation*}$

$\begin{equation*} \forall x,y.\ \lnot (x \in P \land (x,y) \in r \land y \in E) \end{equation*}$

$\begin{equation*} \forall x,y.\ \lnot (x \in P \land (y,x) \in r^{-1} \land y \in E) \end{equation*}$

$\begin{equation*} \forall x,y.\ \lnot (y \in E \land (y,x) \in r^{-1} \land x \in P) \end{equation*}$

$\begin{equation*} sp(E, r^{-1}) \cap P = \emptyset \end{equation*}$

$\begin{equation*} P \subseteq sp(E, r^{-1})^c \end{equation*}$

In other words, we obtain an upper bound on the set of states $P$ from which we do not reach error. We next introduce the notion of weakest precondition, which allows us to express $sp(E,r^{-1})$ from $Q$ given as complement of error states $E$ .

Weakest Precondition - wp

Definition: for $Q \subseteq S$ , $r \subseteq S \times S$ ,

$\begin{equation*} wp(r,Q) = \{ s \mid \forall s'. (s,s') \in r \rightarrow s' \in Q \} \end{equation*}$

Note that this is in general not the same as $sp(Q,r^{-1})$ when then relation is non-deterministic or partial.

Lemma: Characterization of wp

$wp(r,Q)$ is the largest set $P$ such that $\{P\}r\{Q\}$ , that is:

$\{wp(r,Q)\} r \{Q \}$
$\forall P \subseteq S.\ \{P\} r \{Q\} \rightarrow P \subseteq wp(r,Q)$

Some More Laws on Preconditions and Postconditions

We next list several more lemmas on properties of wp, sp, and Hoare triples.

Postcondition of inverse versus wp

If instead of good states we look at the completement set of “error states”, then $wp$ corresponds to doing $sp$ backwards. In other words, we have the following:

$\begin{equation*} S \setminus wp(r,Q) = sp(S \setminus Q,r^{-1}) \end{equation*}$

Disjunctivity of sp

$\begin{equation*} sp(P_1 \cup P_2,r) = sp(P_1,r) \cup sp(P_2,r) \end{equation*}$

$\begin{equation*} sp(P,r_1 \cup r_2) = sp(P,r_1) \cup sp(P,r_2) \end{equation*}$

Conjunctivity of wp

$\begin{equation*} wp(r,Q_1 \cap Q_2) = wp(r,Q_1) \cap wp(r,Q_2) \end{equation*}$

$\begin{equation*} wp(r_1 \cup r_2,Q) = wp(r_1,Q) \cap wp(r_2,Q) \end{equation*}$

Pointwise wp

$\begin{equation*} wp(r,Q) = \{ s \mid s \in S \land sp(\{s\},r) \subseteq Q \} \end{equation*}$

Pointwise sp

$\begin{equation*} sp(P,r) = \bigcup_{s \in P} sp(\{s\},r) \end{equation*}$

Three Forms of Hoare Triple

The following three conditions are equivalent:

$\{P\} r \{Q\}$

$P \subseteq wp(r,Q)$

$sp(P,r) \subseteq Q$

Expanding Paths

The condition

$\begin{equation*} \{ P \}\ \big(\ \bigcup_{i \in J} r_i \big)\ \{ Q \} \end{equation*}$

is equivalent to

$\begin{equation*} \forall i. i \in J \rightarrow \{ P \} r_i \{ Q \} \end{equation*}$

Transitivity

If $\{P\} s_1 \{ Q \}$ and $\{Q\} s_2 \{R\}$ then also $\{P\} s_1 \circ s_2 \{ R \}$ .

We write this as the following inference rule:

$\begin{equation*} \frac{\{P\} s_1 \{ Q \}, \ \ \{Q\} s_2 \{R\}} {\{P\} s_1 \circ s_2 \{ R \}} \end{equation*}$

Hoare Logic for Loops

The following inference rule holds:

$\begin{equation*} \frac{\{P\} s \{ P \}, \ \ n \geq 0} {\{P\} s^n \{ P \}} \end{equation*}$

Proof is by transitivity.

By Expanding Paths condition above, we then have:

$\begin{equation*} \frac{\{P\} s \{ P \}} {\{P\} \bigcup_{n \ge 0} s^n \{ P \}} \end{equation*}$

In fact, $\bigcup_{n \ge 0} s^n = s^*$ , so we have

$\begin{equation*} \frac{\{P\} s \{ P \}} {\{P\} s^* \{ P \}} \end{equation*}$

This is the rule for non-deterministic loops.

LARA