Hoare logic

Template:Short description Template:Use dmy dates 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 Tony Hoare, and subsequently refined by Hoare and other researchers.Template:Sfn The original ideas were seeded by the work of Robert W. Floyd, who had published a similar systemTemplate:Sfn for flowcharts.

Hoare tripleEdit

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

where <math>P</math> and <math>Q</math> are assertions and <math>C</math> is a command.<ref group=note>Hoare originally wrote "<math>P\{C\}Q</math>" rather than "<math>\{P\}C\{Q\}</math>".</ref> <math>P</math> is named the precondition and <math>Q</math> 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 correctnessEdit

Using standard Hoare logic, only partial correctness can be proven. Total correctness additionally requires termination, which can be proven separately or with an extended version of the While rule.Template:Sfn Thus the intuitive reading of a Hoare triple is: Whenever <math>P</math> holds of the state before the execution of <math>C</math>, then <math>Q</math> will hold afterwards, or <math>C</math> does not terminate. In the latter case, there is no "after", so <math>Q</math> can be any statement at all. Indeed, one can choose <math>Q</math> to be false to express that <math>C</math> does not terminate.

"Termination" here and in the rest of this article is meant in the broader sense that computation will eventually be finished, that is it implies the absence of infinite loops; it does not imply the absence of implementation limit violations (e.g. division by zero) stopping the program prematurely. In his 1969 paper, Hoare used a narrower notion of termination which also entailed the absence of implementation limit violations, and expressed his preference for the broader notion of termination as it keeps assertions implementation-independent:

Template:Quote

RulesEdit

Empty statement axiom schemaEdit

The empty statement rule asserts that the Template:Mono statement does not change the state of the program, thus whatever holds true before Template:Mono also holds true afterwards.<ref group=note>This article uses a natural deduction style notation for rules. For example, <math>\dfrac{\alpha,\beta}{\phi}</math> informally means "If both Template:Mvar and Template:Mvar hold, then also Template:Mvar holds"; Template:Mvar and Template:Mvar are called antecedents of the rule, Template:Mvar is called its succedent. A rule without antecedents is called an axiom, and written as <math>\dfrac{}{\quad\phi\quad}</math>.</ref>

<math>\dfrac{}{\{P\}\texttt{skip}\{P\}}</math>

Assignment axiom schemaEdit

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

<math>\dfrac{}{\{P[E/x]\} x := E \{P\}}</math>

where <math>P[E/x]</math> denotes the assertion Template:Mvar in which each free occurrence of Template:Mvar has been replaced by the expression Template:Mvar.

The assignment axiom scheme means that the truth of <math>P[E/x]</math> is equivalent to the after-assignment truth of Template:Mvar. Thus were <math>P[E/x]</math> true prior to the assignment, by the assignment axiom, then Template:Mvar would be true subsequent to which. Conversely, were <math>P[E/x]</math> false (i.e. <math>\neg P[E/x]</math> true) prior to the assignment statement, Template:Mvar must then be false afterwards.

Examples of valid triples include:

<math>\{ x+1 = 43 \} y := x + 1 \{ y = 43 \}</math>
<math>\{ x + 1 \leq N \} x := x + 1 \{ x \leq N \}</math>

All preconditions that are not modified by the expression can be carried over to the postcondition. In the first example, assigning <math>y:=x+1</math> does not change the fact that <math>x+1=43</math>, so both statements may appear in the postcondition. Formally, this result is obtained by applying the axiom schema with Template:Mvar being (<math>y=43</math> and <math>x+1=43</math>), which yields <math>P[(x+1)/y]</math> being (<math>x+1=43</math> and <math>x+1=43</math>), which can in turn be simplified to the given precondition <math>x+1=43</math>.

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: <math>\{P\} x:=E \{P[E/x]\}</math>; this rule leads to nonsensical examples like:

Another incorrect rule looking tempting at first glance is <math>\{P\} x:=E \{P \wedge x=E\}</math>; it leads to nonsensical examples like:

<math>\{ x = 5 \} x := x + 1 \{ x = 5 \wedge x = x + 1 \}</math>

While a given postcondition Template:Mvar uniquely determines the precondition <math>P[E/x]</math>, the converse is not true. For example:

<math>\{ 0 \leq y\cdot y \wedge y\cdot y \leq 9 \} x := y \cdot y \{ 0 \leq x \wedge x \leq 9 \}</math>,
<math>\{ 0 \leq y\cdot y \wedge y\cdot y \leq 9 \} x := y \cdot y \{ 0 \leq x \wedge y\cdot y \leq 9 \}</math>,
<math>\{ 0 \leq y\cdot y \wedge y\cdot y \leq 9 \} x := y \cdot y \{ 0 \leq y\cdot y \wedge x \leq 9 \} </math>, and
<math>\{ 0 \leq y\cdot y \wedge y\cdot y \leq 9 \} x := y \cdot y \{ 0 \leq y\cdot y \wedge y\cdot y \leq 9 \}</math>

are valid instances of the assignment axiom scheme.

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

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

Rule of compositionEdit

Verifying swap-code
without auxiliary variables

The three statements below (line 2, 4, 6) exchange the values of the variables Template:Mvar and Template:Mvar, without needing an auxiliary variable. In the verification proof, the initial value of Template:Mvar and Template:Mvar is denoted by the constant Template:Mvar and Template:Mvar, respectively. The proof is best read backwards, starting from line 7; for example, line 5 is obtained from line 7 by replacing Template:Mvar (target expression in line 6) by <math>a-b</math> (source expression in line 6). Some arithmetical simplifications are used tacitly, viz. <math>a-(a-b) = b</math> (line 5→3), and <math>a+b-b = a</math> (line 3→1).
Nr	Code	Assertions
1:		<math>\{a = A \wedge b = B \}</math>
2:	<math>a := a + b;</math>
3:		<math>\{ a - b = A \wedge b = B \}</math>
4:	<math>b := a - b;</math>
5:		<math>\{b=A\wedge a-b=B\}</math>
6:	<math>a := a - b</math>
7:		<math>\{b= A\wedge a = B \}</math>

Hoare's rule of composition applies to sequentially executed programs Template:Mvar and Template:Mvar, where Template:Mvar executes prior to Template:Mvar and is written <math>S;T</math> (Template:Mvar is called the midcondition):Template:Sfn

<math>\dfrac{\{P\} S \{Q\}\quad,\quad \{Q\} T \{R\}}{\{P\} S;T \{R\}}</math>

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

and

By the sequencing rule, one concludes:

Another example is shown in the right box.

Conditional ruleEdit

<math>\dfrac{\{B \wedge P\} S \{Q\}\quad,\quad \{\neg B \wedge P \} T \{Q\}}{\{P\} \texttt{if}\ B\ \texttt{then}\ S\ \texttt{else}\ T\ \texttt{endif} \{Q\}}</math>

The conditional rule states that a postcondition Template:Mvar common to Template:Mono and Template:Mono part is also a postcondition of the whole Template:Mono statement.Template:Sfn In the Template:Mono and the Template:Mono part, the unnegated and negated condition Template:Mvar can be added to the precondition Template:Mvar, respectively. The condition, Template:Mvar, must not have side effects. An example is given in the next section.

This rule was not contained in Hoare's original publication.Template:Sfn However, since a statement

<math>\texttt{if}\ B\ \texttt{then}\ S\ \texttt{else}\ T\ \texttt{endif}</math>

has the same effect as a one-time loop construct

<math>\texttt{bool}\ b:=\texttt{true}; \texttt{while}\ B\wedge b\ \texttt{do}\ S; b:=\texttt{false}\ \texttt{done}; b:=\texttt{true}; \texttt{while}\ \neg B\wedge b\ \texttt{do}\ T; b:=\texttt{false}\ \texttt{done}</math>

the conditional rule can be derived from the other Hoare rules. In a similar way, rules for other derived program constructs, like Template:Mono loop, Template:Mono loop, Template:Mono, Template:Mono, Template:Mono can be reduced by program transformation to the rules from Hoare's original paper.

Consequence ruleEdit

<math>\dfrac{P_1 \rightarrow P_2\quad ,\quad \{P_2\} S \{Q_2\}\quad ,\quad Q_2 \rightarrow Q_1}{\{P_1\} S \{Q_1\}}</math>

This rule allows to strengthen the precondition <math>P_2</math> and/or to weaken the postcondition <math>Q_2</math>. It is used e.g. to achieve literally identical postconditions for the Template:Mono and the Template:Mono part.

For example, a proof of

<math>\{0 \leq x \leq 15 \}\texttt{if}\ x<15\ \texttt{then}\ x:=x+1\ \texttt{else}\ x:=0\ \texttt{endif} \{0 \leq x \leq 15 \}</math>

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

<math>\{0 \leq x \leq 15 \wedge x < 15 \} x:=x+1 \{ 0 \leq x \leq 15 \}</math>, or simplified

for the Template:Mono part, and

<math>\{0 \leq x \leq 15 \wedge x \geq 15\} x:=0 \{0 \leq x \leq 15\}</math>, or simplified

for the Template:Mono part.

However, the assignment rule for the Template:Mono part requires to choose Template:Mvar as <math>0\leq x \leq 15</math>; rule application hence yields

<math>\{0 \leq x+1 \leq 15\} x:=x+1 \{0 \leq x \leq 15\}</math>, which is logically equivalent to

<math>\{-1 \leq x < 15\} x:=x+1 \{0 \leq x \leq 15\}</math>.

The consequence rule is needed to strengthen the precondition <math>\{-1 \leq x < 15\}</math> obtained from the assignment rule to <math>\{0 \leq x < 15\}</math> required for the conditional rule.

Similarly, for the Template:Mono part, the assignment rule yields

<math>\{0 \leq 0 \leq 15\} x:=0 \{0 \leq x \leq 15\}</math>, or equivalently

<math>\{\texttt{true}\} x:=0 \{0 \leq x \leq 15\}</math>,

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

While ruleEdit

<math>\dfrac{\{P \wedge B\} S \{P\}}{\{P\} \texttt{while}\ B\ \texttt{do}\ S\ \texttt{done} \{\neg B \wedge P\}}</math>

Here Template:Mvar is the loop invariant, which is to be preserved by the loop body Template:Mvar. After the loop is finished, this invariant Template:Mvar still holds, and moreover <math>\neg B</math> must have caused the loop to end. As in the conditional rule, Template:Mvar must not have side effects.

For example, a proof of

<math>\{x \leq 10\} \texttt{while}\ x<10\ \texttt{do}\ x:=x+1\ \texttt{done} \{\neg x < 10 \wedge x \leq 10\}</math>

by the while rule requires to prove

<math>\{x \leq 10 \wedge x < 10\} x := x + 1 \{x \leq 10 \}</math>, or simplified

<math>\{x < 10\} x := x + 1 \{x \leq 10 \}</math>,

which is easily obtained by the assignment rule. Finally, the postcondition <math>\{\neg x <10 \wedge x\leq 10\}</math> can be simplified to <math>\{x=10\}</math>.

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

<math>\{\texttt{true}\} \texttt{while}\ x\cdot x \neq a\ \texttt{do}\ \texttt{skip}\ \texttt{done} \{x \cdot x = a \wedge \texttt{true}\}</math>

After applying the while rule with Template:Mvar being Template:Mono, it remains to prove

<math>\{\texttt{true} \wedge x\cdot x \neq a\} \texttt{skip} \{\texttt{true}\}</math>,

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 Template:Mvar must have contained (by chance) the value of Template:Mvar's square root. In all other cases, it will not terminate; therefore it is not totally correct.

While rule for total correctnessEdit

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.

<math>\dfrac{<\ \text{is a well-founded ordering on the set}\ D\quad,\quad [P \wedge B \wedge t \in D \wedge t = z] S [P \wedge t \in D \wedge t < z ]}{[P \wedge t \in D] \texttt{while}\ B\ \texttt{do}\ S\ \texttt{done} [\neg B \wedge P \wedge t \in D]}</math>

In this rule, in addition to maintaining the loop invariant, one also proves termination by way of an expression Template:Mvar, called the loop variant, whose value strictly decreases with respect to a well-founded relation Template:Mvar on some domain set Template:Mvar during each iteration. Since Template:Mvar is well-founded, a strictly decreasing chain of members of Template:Mvar can have only finite length, so Template:Mvar cannot keep decreasing forever. (For example, the usual order Template:Mvar is well-founded on positive integers <math>\mathbb{N}</math>, but neither on the integers <math>\mathbb{Z}</math> nor on positive real numbers <math>\mathbb{R}^+</math>; all these sets are meant in the mathematical, not in the computing sense, they are all infinite in particular.)

Given the loop invariant Template:Mvar, the condition Template:Mvar must imply that Template:Mvar is not a minimal element of Template:Mvar, for otherwise the body Template:Mvar could not decrease Template:Mvar any further, i.e. the premise of the rule would be false. (This is one of various notations for total correctness.) <ref group="note"> Hoare's 1969 paper didn't provide a total correctness rule; cf. his discussion on p.579 (top left). For example Reynolds' textbookTemplate:Sfn gives the following version of a total correctness rule: <math>\dfrac{P \wedge B \rightarrow 0\leq t\quad ,\quad [P \wedge B \wedge t=z] S [P \wedge t<z]}{[P] \texttt{while}\ B\ \texttt{do}\ S\ \texttt{done} [P \wedge \neg B]}</math> when Template:Mvar is an integer variable that doesn't occur free in Template:Mvar, Template:Mvar, Template:Mvar, or Template:Mvar, and Template:Mvar is an integer expression (Reynolds' variables renamed to fit with this article's settings). </ref>

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

<math>[x \leq 10]\texttt{while}\ x < 10\ \texttt{do}\ x:=x+1\ \texttt{done} [\neg x < 10 \wedge x \leq 10]</math>

the while rule for total correctness can be applied with e.g. Template:Mvar being the non-negative integers with the usual order, and the expression Template:Mvar being <math>10 - x</math>, which then in turn requires to prove

<math>[x \leq 10 \wedge x < 10 \wedge 10-x \geq 0 \wedge 10-x = z] x:= x+1 [x \leq 10 \wedge 10-x \geq 0 \wedge 10-x < z]</math>

Informally speaking, we have to prove that the distance <math>10-x</math> 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 simplified to

<math>[x < 10 \wedge 10-x = z] x:=x+1 [x \leq 10 \wedge 10-x < z]</math>,

which can be proven as follows:

<math>[x+1 \leq 10 \wedge 10-x-1 < z] x:=x+1 [x \leq 10 \wedge 10-x < z]</math> is obtained by the assignment rule, and

<math>[x+1 \leq 10 \wedge 10-x-1 < z]</math> can be strengthened to <math> [x < 10 \wedge 10-x = z]</math> by the consequence rule.

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

NotesEdit

Template:Reflist

ReferencesEdit