Hoare logic

Hoare logic (also known as Floyd–Hoare logic or Hoare rules) is a formal system with a set of logical rules for reasoning rigorously about the correctness of computer programs. It was proposed in 1969 by the British computer scientist and logician C. A. R. Hoare, and subsequently refined by Hoare and other researchers. The original ideas were seeded by the work of Robert Floyd, who had published a similar system for flowcharts.

Hoare triple

The central feature of Hoare logic is the Hoare triple. A triple describes how the execution of a piece of code changes the state of the computation. A Hoare triple is of the form

$\{P\}\;C\;\{Q\}$

where P and Q are assertions and C is a command . P is named the precondition and Q the postcondition: when the precondition is met, executing the command establishes the postcondition. Assertions are formulae in predicate logic.

Hoare logic provides axioms and inference rules for all the constructs of a simple imperative programming language. In addition to the rules for the simple language in Hoare's original paper, rules for other language constructs have been developed since then by Hoare and many other researchers. There are rules for concurrency, procedures, jumps, and pointers.

Partial and total correctness

Using standard Hoare logic, only partial correctness can be proven, while termination needs to be proved separately. Thus the intuitive reading of a Hoare triple is: Whenever P holds of the state before the execution of C, then Q will hold afterwards, or C does not terminate. Note that if C does not terminate, then there is no "after", so Q can be any statement at all. Indeed, one can choose Q to be false to express that C does not terminate.

Total correctness can also be proven with an extended version of the While rule.

Rules

Empty statement axiom schema

The empty statement rule asserts that the skip statement does not change the state of the program, thus whatever holds true before skip also holds true afterwards.

$\frac{}{\{P\}\ \textbf{skip}\ \{P\}} \!$

Assignment axiom schema

The assignment axiom states that after the assignment any predicate holds for the variable that was previously true for the right-hand side of the assignment. Formally, let P be an expression in which the variable x is free. Then:

$\frac{}{\{P[E/x]\}\ x:=E \ \{P\} } \!$

where $P[E/x]$ denotes the expression P in which each free occurrence of x has been replaced by expression E.

The assignment axiom scheme means that the truth of $\{P[E/x]\}$ is equivalent to the after-assignment truth of $\{P\}$. Thus were $\{P[E/x]\}$ true prior to the assignment, by the assignment axiom, then $\{P\}$ would be true subsequent to which. Conversely, were $\{P[E/x]\}$ false prior to the assignment statement, $\{P\}$ must then be false afterwards.

Examples of valid triples include:

• $\{x+1 = 43\}\ y:=x + 1\ \{ y = 43 \}\!$
• $\{x + 1 \leq N \}\ x := x + 1\ \{x \leq N\}\ \!$

The assignment axiom scheme is equivalent to saying that to find the precondition, first take the post-condition and replace all occurrences of the left-hand side of the assignment with the right-hand side of the assignment. Be careful not to try to do this backwards by following this incorrect way of thinking: $\{P\} x :=E \{P[E/x]\}$; this rule leads to nonsensical examples like:

• $\{x=5\} x:=3 \{3=5\}$

Another incorrect rule looking tempting at first glance is $\{P\} x:=E \{P \mbox{ and } x=E\}$; it leads to nonsensical examples like:

• $\{x=5\} x:=x+1 \{x=5 \mbox{ and } x=x+1\}$

The assignment axiom proposed by Hoare does not apply when more than one name may refer to the same stored value. For example,

$\{ y=3 \} \ x := 2\ \{y = 3 \}$

is wrong if x and y refer to the same variable, although it is a proper instance of the assignment axiom scheme (with both $\{P\}$ and $\{P[2/x]\}$ being $\{y=3\}$).

Rule of composition

Hoare's rule of composition applies to sequentially executed programs S and T, where S executes prior to T and is written S;T (Q is called the midcondition):

$\frac {\{P\}\ S\ \{Q\}\ , \ \{Q\}\ T\ \{R\} } {\{P\}\ S;T\ \{R\}} \!$

For example, consider the following two instances of the assignment axiom:

$\{ x + 1 = 43\} \ y:=x + 1\ \{y =43 \}$

and

$\{ y = 43\} \ z:=y\ \{z =43 \}$

By the sequencing rule, one concludes:

$\{ x + 1 = 43\} \ y:=x + 1; z:= y\ \{z =43 \}$

Conditional rule

$\frac { \{B \land P\}\;\;\; S\;\;\; \{Q\}\; ,\;\;\;\;\; \{\neg B \land P \}\;\;\; T\;\;\; \{Q\} } { \{P\}\;\;\; \textbf{if}\; B\; \textbf{then}\; S\; \textbf{else}\; T\; \textbf{endif}\;\;\; \{Q\} }$

The conditional rule states that a postcondition $Q$ common to then and else part is also a postcondition of the whole if...endif statement. In the then and the else part, the unnegated and negated condition $B$ can be added to the precondition $P$, respectively. An example is given in the next section.

It was not contained in Hoare's original publication . However, since a statement

$\textbf{if} \; B \; \textbf{then} \; S \; \textbf{else} \; T \; \textbf{endif}$

has the same effect as a one-time loop construct

$\textbf{bool} \; b:= \textbf{true}; \; \textbf{while} \; B \land b \; \textbf{do} \; S; \; b := \textbf{false} \; \textbf{done}; \; b:= \textbf{true}; \; \textbf{while} \; \neg B \land b \; \textbf{do} \; T; \; b := \textbf{false} \; \textbf{done}$

the conditional rule can be derived from the other Hoare rules. In a similar way, rules for other derived program constructs, like for loop, do...until loop, switch, break, continue can be reduced by program transformation to the rules from Hoare's original paper.

Consequence rule

$\frac { P_1 \rightarrow P_2 \; , \;\;\;\;\; \lbrace P_2 \rbrace \;\;\; S \;\;\; \lbrace Q_2 \rbrace \; , \;\;\;\;\; Q_2 \rightarrow Q_1 } { \lbrace P_1 \rbrace \;\;\; S \;\;\; \lbrace Q_1 \rbrace } \!$

This rule allows to strenghten the precondition and/or to weaken the postcondition. It is used e.g. to achieve literally identical postconditions for then then and the else part.

For example, a proof of

needs to apply the conditional rule, which in turn requires to prove

, or simplified

for the then part, and

, or simplified

for the else part.

However, the assignment rule for the then part requires to chose $P$ as

rule application hence yields

, which is logically equivalent to

. The consequence rule is needed to strenghten the precondition

obtained from the assignment rule to 
required for the conditional rule.

Similarly, for the else part, the assignment rule yields

, or equivalently

, hence the consequence rule has to be applied with $P_1$ and $P_2$ being $\{x=15\}$ and $\{true\}$, respectively, to strengthen again the precondition. Informally, the effect of the consequence rule is to "forget" that $x=15$ is known at the entry of the else part, since the assignment rule used for the else part doesn't need that information.

While rule

$\frac { \{P \land B \}\ S\ \{P\} } { \{P \}\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ \{\neg B \land P\} } \!$

Here $P$ is the loop invariant, which is to be preserved by the loop body $S$. After the loop is finished, this invariant $P$ still holds, and moreover $\neg B$ must have caused the loop to end.

For example, a proof of

by the while rule requires to prove

, or simplified

, which is easily obtained by the assignment rule. Finally, the postcondition

can be simplified to $\{x=10\}$.

For another example, the while rule can be used to formally verify the following strange program to compute the exact square root $x$ of an arbitrary number $a$ - even if $x$ is an integer variable and $a$ is not a square number:

After applying the while rule with $P$ being true, it remains to prove

, which follows from the skip rule and the consequence rule.

In fact, the strange program is partially correct: if it happened to terminate, it is certain that $x$ must have contained (by chance) the value of $a$'s square root. However, it is not totally correct, since it obviously will not terminate under allmost all circumstances.

While rule for total correctness

If the above ordinary while rule is replaced by the following one, the Hoare calculus can also be used to prove total correctness, i.e. termination as well as partial correctness. Commonly, square brackets are used here instead of curly braces to indicate the different notion of program correctness.

$\frac { < \textrm{is a well-founded ordering on the set } D, \;\;\;\;\; [P \land B \land t \in D \land t = z ] \;\;\; S \;\;\; [P \land t \in D \land t < z ]} { [P] \;\;\; \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done} \;\;\; [\neg B \land P] } \!$

In this rule, in addition to maintaining the loop invariant, one also proves termination by way of a expression t, called the loop variant, whose value strictly decreases with respect to a well-founded relation $<$ on some domain set $D$ during each iteration. Since $<$ is well-founded, a strictly decreasing chain of members of $D$ can have only finite length, so t cannot keep decreasing forever. (For example, the usual order $<$ is well-founded on the set of positive integer numbers, but neither on the set of all integers nor on the set of positive real numbers; all sets are meant in the mathematical, not in the computing sense, they are all infinite in particular.)

Given the loop invariant P, the condition B must imply that t is not a minimal element of $D$, for otherwise the body $S$ could not decrease $t$ any further, i.e. the premise of the rule would be false. (This is one of various notations for total correctness.)

Resuming the first example of the previous section, for a total-correctness proof of

the while rule for total correctness can be applied with e.g. $D$ being the positive integers with the usual order, and the expression $t$ being $10-x$, which then in turn requires to prove

Informally speaking, we have to prove that the distance $10-x$ decreases in every loop cycle, while it always remains non-negative; this process can go on only for a finite number of cycles.

The previous proof goal can be simplfied to

, which can be proven as follows:

is obtained by the assignment rule, and 

can be strenghtened to $\;\;\; [x<10 \land 10-x=z]\;\;\;$ by the consequence rule.

For the second example of the previous section, of course no expression t can be found that is decreased by the empty loop body, hence termination cannot be proved.

Examples

Example 1
$\{x+1 = 43\}\!$	$\ y:=x + 1\ \!$	$\{ y = 43 \}\!$	(Assignment Axiom)
			$( x + 1 = 43 \Leftrightarrow x = 42 )$
$\{x=42\}\!$	$\ y:=x + 1\ \!$	$\{y=43 \land x=42\}\!$	(Consequence Rule)
Example 2
$\{x + 1 \leq N \}\!$	$\ x := x + 1\ \!$	$\{x \leq N\}\ \!$	(Assignment Axiom)
			($x < N \implies x + 1 \leq N$ for x, N with integer types)
$\{x < N \}\!$	$\ x := x + 1\ \!$	$\{x \leq N\}\ \!$	(Consequence Rule)

See also

• Communicating sequential processes
• Design by contract
• Denotational semantics
• Dynamic logic
• Edsger W. Dijkstra
• Loop invariant
• Assertion (computing)
• Predicate transformer semantics
• Program verification
• Refinement calculus
• Separation logic
• Sequent calculus
• Static code analysis

Further reading

• Robert D. Tennent. Specifying Software (a textbook that includes an introduction to Hoare logic, written in 2002) ISBN 0-521-00401-2

External links

• KeY-Hoare is a semi-automatic verification system built on top of the KeY theorem prover. It features a Hoare calculus for a simple while language.
• j-Algo-modul Hoare calculus — A visualisation of the Hoare calculus in the algorithm visualisation program j-Algo