Floyd-Hoare Logic

A method of reasoning mathematically about impreative programs.

• Basis of mechanized program verification systems.
• A kind of axiomatic semantics of impreative programs.

Hoare’s Notation (Hoare Triples)

For a program $c$, partitial correctness specification:

$$\{p\}\ c\ \{q\}$$

and total correctness specification:

$$[p]\ c\ [q]$$

where $p$ and $q$ are assertions, $p$ is called precondition, $q$ is called postcondition.

A partitial correctness specification $\{p\}\ c\ \{q\}$ is valid, if and only if

• if $c$ is executed in a state initially satisfying $p$
• and if the execution of $c$ terminates
• then the final state satisfies $q$

It is only required that if the execution terminates, then $q$ holds.

A total correctness specification $[p]\ c\ [q]$ is valid, if and only if

• if $v$ is executed in a state initially satisfying $p$
• then the execution of $c$ terminates
• and the final state satisfies $q$

Informally, total correctness = termination + partitial correctness.

Semantics of Assertions

$\vdash p$: there exists a proof of derivation of $p$ following the inference rules.

$\sigma \vDash p$: $p$ holds (is true) in $\sigma$, or $\sigma$ satisfies $p$.

$$\sigma \vDash \forall x.p \text{ iff } \forall n.\ \sigma\{x \leadsto n\} \vDash p$$

$$\sigma \vDash \exists x.p \text{ iff } \exists n.\ \sigma\{x \leadsto n\} \vDash p$$

(for all/some values of $x$, the assertion $p$ is true)

Validity of Assertions

• $p$ holds in $\sigma$ ($\sigma \vDash p$)
• $p$ is valid: for all $\sigma$, $p$ holds in $\sigma$
• $p$ is unsatisfiable: $\neg p$ is valid

Rules of Hoare Logic

Assignment rule:

$${ \over \{p[e/x]\}\ x:=e\ \{p\}}\ (\texttt{AS})$$

A forward assignment rule (due to Floyd):

$${ \over \{p\}\ x:=e\ \{ \exists v.\ x = e[v/x] \wedge p[v/x] \}}\ (\texttt{AS-FW})$$

where $v$ is a fresh variable.

Strengthening precedent:

$${p \Rightarrow q \ \ \ \ \ \ \{q\}\ c\ \{r\} \over \{p\}\ c\ \{r\}}\ (\texttt{SP})$$

Weakening consequent:

$${\{p\}\ c\ \{q\} \ \ \ \ \ \ q \Rightarrow r \over \{p\}\ c\ \{r\}}\ (\texttt{WC})$$

Sequential composition rule:

$${\{p\}\ c_1\ \{r\} \ \ \ \ \ \ \{r\}\ c_2\ \{q\} \over \{p\}\ c_1; c_2\ \{q\}}\ (\texttt{SC})$$

Skip rule:

$${ \over \{p\}\ \textbf{skip}\ \{p\}}\ (\texttt{SK})$$

Conditional rule:

$${\{p \wedge b\}\ c_1\ \{q\} \ \ \ \ \ \ \{p \wedge \neg b\}\ c_2\ \{q\} \over \{p\}\ \textbf{if } b \textbf{ then } c_1 \textbf{ else } c_2\ \{q\}}\ (\texttt{CD})$$

Conjuction (?) rules:

$${\{p\}\ c\ \{q\} \ \ \ \ \ \ \{p'\}\ c\ \{q'\} \over \{p \wedge p'\}\ c\ \{q \wedge q'\}}\ (\texttt{CA})$$

$${\{p\}\ c\ \{q\} \ \ \ \ \ \ \{p'\}\ c\ \{q'\} \over \{p \vee p'\}\ c\ \{q \vee q'\}}\ (\texttt{DA})$$

While rule:

$${\{i \wedge b\}\ c\ \{i\} \over \{i\}\ \textbf{while } b \textbf{ do } c\ \{i \wedge \neg b\}}\ (\texttt{WHP})$$

$i$ is called loop invariant.

• invariant $i$ must hold initially
• with the negated test $\neg b$ the invariant $i$ must establish the result
• when the test $b$ holds, the body must leave the invariant $i$ unchanged

therefore, the invariant should say that:

• what has been done so far together with what remains to be done
• holds at each iteration of the loop
• and gives the desired result when the loop terminates

The while Rule for Total Correctness

The while commands are the only commands that can cause non-termination in our language (the only kind of command with a non-trival termination rule).

The idea behind the while rule for total correctness is

• to prove $\textbf{while } b \textbf{ do } c$ terminates
• show that some non-negative metric (e.g. a loop counter) decreases on each iteration of $c$
• this decreasing metric is called a variant

$${[i \wedge b \wedge (e = x_0)]\ c\ [i \wedge (e < x_0)] \ \ \ \ \ \ i \wedge b \Rightarrow e \geqslant 0 \over [i]\ \textbf{while } b \textbf{ do } c\ [i \wedge \neg b]}\ (\texttt{WHT})$$

where $x_0 \notin \text{fv}( c ) \cup \text{fv}(e) \cup \text{fv}(i) \cup \text{fv}(b)$ is a logical variable, $e$ is the variant of the loop.

Basic idea:

• the first premise: the metric is decreased by execution of $c$,
• the second premise: when the metric becomes negative, $b$ is false and the loop terminates (invariant $i$ is always satisfied).

Derived Rules

Derived rule for assignment:

$${p \Rightarrow q[e/x] \over \{p\}\ x:=e\ \{q\}}$$

Derived rule for sequenced assignment:

$${\{p\}\ c\ \{q[e/x]\} \over \{p\}\ c;x:=e\ \{q\}}$$

Derived while rule for partial correctness:

$${p \Rightarrow i \ \ \ \ \ \ \{i \wedge b\}\ c\ \{i\}\ \ \ \ \ \ i \wedge \neg b \Rightarrow q \over \{p\}\ \textbf{while } b \textbf{ do } c\ \{q\}}$$

Derived while rule for total correctness:

$$ { \begin{aligned} & p \Rightarrow i \\ & i \wedge b \Rightarrow e \geqslant 0 \\ & i \wedge \neg b \Rightarrow q \\ &[i \wedge b \wedge (e=x_0)]\ c\ [i \wedge (e < x_0)]\end{aligned} \over [p]\ \textbf{while } b \textbf{ do } c\ [q]} $$

Derived rule for multiple sequential composition:

$${\begin{aligned} & p_0 \Rightarrow q_0 \\ & \{q_0\}\ c_0 \{p_1\} & p_1 \Rightarrow q_1 \\ & \dots & \dots \\ & \{q_{n-1}\}\ c_{n-1} \{p_n\} & p_n \Rightarrow q_n \end{aligned} \over \{p_0\}\ c_0;\dots;c_{n-1}\ \{q_n\}}\ (\texttt{MSQ}_n)$$

Soundness and Completeness of Predicate Logic

Notations:

• $\vdash p$: $p$ is provable
• $\vDash p$: $p$ is valid

Definition:

• Soundness: if $\vdash p$ then $\vDash p$
• Completeness: if $\vDash p$ then $\vdash p$

（省略一堆证明）

Hoare Logic is sound and relatively complete (i.e., if $\vDash \{p\}\ c\ \{q\}$, then $\Gamma \vdash \{p\}\ c\ \{q\}$ where $\Gamma = \{p\ |\ (\vDash p)\}$).

Weakest Precondition

Definition: given command $c$ and assertion $q$, the weakest precondition $wp(c,q)$ is an assertion such that

$$\sigma \vDash wp(c,q) \Leftrightarrow (\forall \sigma'.\ (c, \sigma) \longrightarrow^* (\textbf{skip}, \sigma') \Rightarrow \sigma' \vDash q)$$

Corollary: for all $p$, $c$ and $q$,

$$\vDash {p}\ c\ {q} \Leftrightarrow\ \vDash (p \Rightarrow wp(c,q))$$

An assertion language is called expressive if for every $c$ and $q$, the weakest precondition $wp(c,q)$ is an assertion in the language.

Lemma: for every $c$ and $q$, $$\vdash {wp(c,q)}\ c\ {q}.$$