Hoare logic

From Wikipedia, the free encyclopedia

Hoare logic (also known as Floyd–Hoare logic) is a formal system developed by the British computer scientist C. A. R. Hoare, and subsequently refined by Hoare and other researchers. It was published in Hoare's 1969 paper "An axiomatic basis for computer programming". The purpose of the system is to provide a set of logical rules in order to reason about the correctness of computer programs with the rigour of mathematical logic.

Hoare acknowledges earlier contributions from Robert Floyd, who had published a similar system for flowcharts.

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 called the precondition and Q the postcondition. Assertions are formulas in predicate logic.

Hoare logic has 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.

1 Partial and total correctness
2 Empty statement axiom
3 Assignment axiom schema
4 Sequencing rule
5 Conditional rule
6 While rule
7 Consequence rule
8 While rule for total correctness
9 See also
10 References

[edit] Partial and total correctness

Standard Hoare logic proves only partial correctness, while termination would have 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.

[edit] Empty statement axiom

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

[edit] 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:

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

Here $P [x / E]$ denotes the expression P in which all free occurrences of the variable x have been replaced with the expression E.

An example of a valid triple is:

$\{x+1=43 \land x=42\} \ y:=x + 1\ \{y=43 \land x=42\} \!$

The assignment axiom proposed by Hoare is incorrect when more than one name can refer to the same stored value. For example, if x and y refer to the same value then

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

is not a true statement, because no precondition can cause y to be 3 after x is set to 2.

[edit] Sequencing rule

$\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 \}$

[edit] Conditional rule

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

[edit] While rule

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

Here P is the loop invariant.

[edit] Consequence rule

$\frac { P^\prime \rightarrow\ P\ ,\ \lbrace P \rbrace\ S\ \lbrace Q \rbrace\ ,\ Q \rightarrow\ Q^\prime } { \lbrace P^\prime\ \rbrace\ S\ \lbrace Q^\prime\rbrace } \!$

[edit] While rule for total correctness

$\frac { \{P \wedge B \wedge t = z \}\ S\ \{P \wedge t < z \} \ ,\ P \rightarrow t \geq 0} { \{P \}\ \textbf{while}\ B\ \textbf{do}\ S\ \textbf{done}\ \{\neg B \wedge P\} } \!$

In this rule, in addition to maintaining the loop invariant, one also proves termination by way of a term whose value decreases during each iteration, here t. Note that t must take values from a well-founded set, so that each step of the loop is counted by decreasing members of a finite chain.

[edit] See also

[edit] References

C. A. R. Hoare. "An axiomatic basis for computer programming". Communications of the ACM, 12(10):576–585, October 1969. DOI:10.1145/363235.363259 | Download PDF
Robert D. Tennent: "Specifying Software" (a recent textbook that includes an introduction to Hoare logic) ISBN 0-521-00401-2 [1]
Project Bali has defined Hoare logic-style rules for a subset of the Java programming language, for use with the Isabelle theorem prover

Retrieved from "http://en.wikipedia.org../../../h/o/a/Hoare_logic.html"

Categories: Logic in computer science | Formal methods