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

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

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, the command establishes the postcondition. Assertions are formulas 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

Standard Hoare logic proves only partial correctness, while termination needs 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 be also 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.

:$\backslash frac\{\}\{\backslash \{P\backslash \}\backslash \; \backslash textbf\{skip\}\backslash \; \backslash \{P\backslash \}\}\; \backslash !$

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:

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

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

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

Examples of valid triples include:

:*$\backslash \{x+1\; =\; 43\backslash \}\backslash \; y:=x\; +\; 1\backslash \; \backslash \{\; y\; =\; 43\; \backslash \}\backslash !$ :*$\backslash \{x\; +\; 1\; \backslash leq\; N\; \backslash \}\backslash \; x\; :=\; x\; +\; 1\backslash \; \backslash \{x\; \backslash leq\; N\backslash \}\backslash \; \backslash !$

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

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

is not a true statement if x and y refer to the same variable, because no precondition can cause y to be 3 after x is set to 2.

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.

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

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

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

and

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

By the sequencing rule, one concludes:

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

Conditional rule

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

Consequence rule

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

While rule

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

Here P is the loop invariant.

While rule for total correctness

::

In this rule, in addition to maintaining the loop invariant, one also proves termination by way of a term, called the loop variant, here t, whose value strictly decreases with respect to a well-founded relation during each iteration. Note that, given the invariant P, the condition B must imply that t is not a minimal element of its range, for otherwise the premise of this rule would be false. Because the relation "<" is well-founded, each step of the loop is counted by decreasing members of a finite chain. Also note that square brackets are used here instead of curly braces to denote total correctness, i.e. termination as well as partial correctness. (This is one of various notations for total correctness.)

Examples

:{|style="text-align:left" |bgcolor="#C0C0C0" colspan=4|Example 1 |- |$\backslash \{x+1\; =\; 43\backslash \}\backslash !$ |$\backslash \; y:=x\; +\; 1\backslash \; \backslash !$ |$\backslash \{\; y\; =\; 43\; \backslash \}\backslash !$ |(Assignment Axiom) |- | | | |$(\; x\; +\; 1\; =\; 43\; \backslash Leftrightarrow\; x\; =\; 42\; )$ |- |$\backslash \{x=42\backslash \}\backslash !$ |$\backslash \; y:=x\; +\; 1\backslash \; \backslash !$ |$\backslash \{y=43\; \backslash land\; x=42\backslash \}\backslash !$ |(Consequence Rule) |- |bgcolor="#C0C0C0" colspan=4|Example 2 |- |$\backslash \{x\; +\; 1\; \backslash leq\; N\; \backslash \}\backslash !$ |$\backslash \; x\; :=\; x\; +\; 1\backslash \; \backslash !$ |$\backslash \{x\; \backslash leq\; N\backslash \}\backslash \; \backslash !$ |(Assignment Axiom) |- | | | |( for x, N with integer types) |- | |$\backslash \; x\; :=\; x\; +\; 1\backslash \; \backslash !$ |$\backslash \{x\; \backslash leq\; N\backslash \}\backslash \; \backslash !$ |(Consequence Rule) |}

See also

Communicating sequential processes

Design by contract

Denotational semantics

Dynamic logic

Edsger W. Dijkstra

Loop invariant

Predicate transformer semantics

Program verification

Refinement calculus

Separation logic

Sequent calculus

Static code analysis

References

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

Project Bali has defined Hoare logic-style rules for a subset of the Java programming language, for use with the Isabelle theorem prover

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

Category:Logic in computer science Category:Formal methods