====== 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 =====

<code java>
//{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}
</code>

===== 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 [[sav08:Sets and relations#Relation Image]] of a set.

{{sav08:sp.png?400x250|}}



==== 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.

{{sav08:wp.png?400x250|}}

==== 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.

===== Further reading =====

  * {{sav08:backwright98refinementcalculus.pdf|Refinement Calculus Book by Back, Wright}}