Hoare calculus

The Hoare calculus (also called Hoare logic ) is a formal system to prove the correctness of programs. It was developed by the British computer scientist C. AR Hoare and later refined by him and other scientists. The Hoare calculus was published in 1969 in an article entitled An axiomatic basis for computer programming .

The purpose of the system is to provide a set of logical rules that allow statements to be made about the correctness of imperative computer programs and to make use of mathematical logic . Hoare builds on earlier contributions by Robert Floyd , who published a similar system for flowcharts. In contrast to the Floyd method, in which execution paths are interpreted, the Hoare calculus works with the source code.

Alternatively, the wp calculus can be used, in which, in contrast to the Hoare calculus, a backward analysis takes place.

Hoare triple

The central element of the Hoare calculus is the Hoare triple, which describes how a program part changes the state of a calculation:

${\displaystyle \{P\}\;S\;\{Q\}.}$

Here, and assurances (English assertions ), is a program segment. is the precondition (English precondition ) and the postcondition (English postcondition ). If the precondition applies, the postcondition applies after the program segment has been executed. Assertions are formulas of predicate logic . ${\displaystyle P}$ ${\displaystyle Q}$ ${\displaystyle S}$ ${\displaystyle P}$ ${\displaystyle Q}$

A triple can be understood in the following way: If applies to the program state before the execution of , then applies afterwards. If not terminated , then there is no after, so any statement can be in this case . In fact, one can choose wrong for the statement to express that it does not terminate. One speaks here of partial correctness . If it is always terminated and then true, one speaks of total correctness . The termination must be proven independently. ${\displaystyle P}$ ${\displaystyle S}$ ${\displaystyle Q}$ ${\displaystyle S}$ ${\displaystyle Q}$ ${\displaystyle Q}$ ${\displaystyle S}$ ${\displaystyle S}$ ${\displaystyle Q}$

If no precondition exists, write:

${\displaystyle \{true\}\;S\;\{Q\}.}$

Partial correctness

The Hoare calculus consists of axioms and rules of derivation for all constructs of a simple imperative programming language:

Axiom of the Empty Instruction

If a program segment does not change any variables, the assertions do not change either, so postcondition is the same as precondition: ${\displaystyle S}$

${\displaystyle {\frac {}{\{P\}S\{P\}}}}$

Assignment axiom

The assignment axiom states that after an assignment, every statement applies to the variable that previously applied to the right-hand side of the assignment:

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

${\displaystyle P[E/x]}$is the statement, which arises in that, in each free occurrence of through replaced. ${\displaystyle P}$ ${\displaystyle x}$ ${\displaystyle E}$

Strictly speaking, the axiom of assignment is not a single axiom, but a scheme for an infinite set of axioms, for , and can take any possible form and can be constructed from it. ${\displaystyle x}$ ${\displaystyle E}$ ${\displaystyle P}$ ${\displaystyle P[E/x]}$

An example of a triple described by the axiom of assignment is:

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

Composition or sequence rule

In order to analyze sequential programs, the individual triples can be linked according to the following rule:

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

This rule can be applied in the following way: If the statements above the line have been proven, the statement below the line can also be regarded as proven.

For example, consider the following two statements that follow from the axiom of assignment

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

and

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

one can deduce the following statement from this:

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

Selection rule (if-then-else rule)

The following rule applies to selection constructs with 2 options:

${\displaystyle {\frac {\{P\wedge B\}\ S\ \{Q\}\ ,\ \{P\wedge \neg B\}\ T\ \{Q\}}{\{P\}\ \mathrm {if} \ B\ \mathrm {then} \ S\ \mathrm {else} \ T\ \{Q\}}}}$

The rule thus proves both the if branch and the else branch. If an if query has no else branch, a slightly modified version of this rule is used:

${\displaystyle {\frac {\{P\wedge B\}\ S\ \{Q\}\ ,\ P\wedge \neg B\Rightarrow Q}{\{P\}\ \mathrm {if} \ B\ \mathrm {then} \ S\ \{Q\}}}}$

Iteration rule (while rule)

${\displaystyle {\frac {\{I\wedge B\}\ S\ \{I\}}{\{I\}\ \mathrm {while} \ B\ \mathrm {do} \ S\ \mathrm {done} \ \{I\wedge \neg B\}}}}$

This is referred to as the loop invariant , which is valid both before, during and after the execution of the loop. An invariant must be determined manually. ${\displaystyle I}$

Rule of Consequence

${\displaystyle {\frac {P\Rightarrow \ P^{\prime },\ \lbrace P^{\prime }\rbrace \ S\ \lbrace Q^{\prime }\rbrace \ ,\ Q^{\prime }\Rightarrow \ Q}{\lbrace P\rbrace \ S\ \lbrace Q\rbrace }}}$

The rule of consequence allows the precondition to be strengthened and the postcondition to be weakened, thus enabling other rules of evidence to be applied. In particular, the precondition or postcondition can also be replaced by an equivalent logical formula. Example:

${\displaystyle \lbrace true\rbrace \ x:=0\ \lbrace x\geq 0\rbrace \ }$ is partially correct because

${\displaystyle {\frac {true\Rightarrow 0=0,\lbrace 0=0\rbrace \ x:=0\ \lbrace x=0\rbrace ,\ x=0\Rightarrow x\geq 0}{\lbrace true\rbrace \ x:=0\ \lbrace x\geq 0\rbrace }}.}$

Total correctness

As explained above, the described calculus is only suitable for the proof of partial correctness. To prove that it is completely correct, the while rule must be extended by a loop variant. It is a function or variable that represents a number with an initial value . It must now be demonstrated that there is a decrease in each loop pass and that the loop terminates at a certain, reduced value. ${\displaystyle t}$ ${\displaystyle z}$ ${\displaystyle t}$

Iteration rule for total correctness

${\displaystyle {\frac {\{I\wedge B~\wedge ~t=z\}\ S\ \{I~\wedge ~t<z\},~I\Rightarrow t\geq 0}{\{I\}\ \mathrm {while} \ B\ \mathrm {do} \ S\ \mathrm {done} \ \{I\wedge \neg B\}}}}$

Here is a term, the loop invariant - that is, what applies in each loop - and a variable in , , and does not occur freely. It is used to compare the value of the term before the loop with that after the loop. The condition ensures that it does not become negative. The idea behind the rule is that if with each iteration of the loop it decreases but never becomes less than zero, the loop has to end at some point. must be from a well-founded set . ${\displaystyle t}$ ${\displaystyle I}$ ${\displaystyle z}$ ${\displaystyle B}$ ${\displaystyle t}$ ${\displaystyle S}$ ${\displaystyle I}$ ${\displaystyle I\Rightarrow t\geq 0}$ ${\displaystyle t}$ ${\displaystyle t}$ ${\displaystyle t}$

rating

With the Hoare calculus and a formal specification, it is possible to check a program or parts of a program for correctness. It provides one of the few procedures that actually prove correctness and not just detect the presence of errors. However, the results of an analysis using the Hoare calculus must be viewed with caution:

• If the specification is incorrect, the results of the analysis may be correct, but compared to an incorrect specification.
• The Hoare calculus does not find any errors that are caused by errors in the specification of the programming language itself or by a faulty compiler.
• The Hoare calculus quickly reaches its limits in large software systems, especially with global variables and recursion.
• For verification, axioms of computer arithmetic must be used, which take into account special features such as the limitation of the whole numbers that can be represented with integer types and the inaccuracy of floating point numbers.

literature

• Hoare: An axiomatic basis for computer programming , Communications of the ACM, Volume 12, 1969, pp. 576-580
• Robert D. Tennent: Specifying Software. A hands-on introduction. Cambridge University Press, Cambridge et al. 2002, ISBN 0-521-00401-2 (an up-to-date textbook with an introduction to Hoare logic), description and "Errors and Corrections".

Web links

• Project Bali has developed rules like the Hoare calculus for a subset of Java for use with the theorem prover Isabelle
• Hoare Tutorial ( Memento from January 31, 2012 in the Internet Archive ) A tutorial that explains how to use the Hoare calculus for program verification (PDF; 493 kB)
• j-Algo-Module Hoare Calculus A visualization of the Hoare calculus within the framework of the algorithm visualization program j-Algo
• KeY-Hoare is a semi-automatic verification system that is based on the KeY Theorem Prover. It performs the Hoare calculus for simple loops.

Individual evidence

1. ↑ ^{a b} Charles Antony Richard Hoare : An Axiomatic Basis for Computer Programming ( Memento of the original from March 4, 2016 in the Internet Archive ) Info: The archive link was inserted automatically and has not yet been checked. Please check the original and archive link according to the instructions and then remove this notice. (PDF; 659 kB). In: Communications of the ACM . Vol. 12, No. 10, 1969, pp. 576-585, doi: 10.1145 / 363235.363259 .  
2. ^ ^{A b} Robert W. Floyd : Assigning meanings to programs . In: Proceedings of the American Mathematical Society Symposia on Applied Mathematics . No. 19 , 1967, p. 19–31 ( virginia.edu [PDF; 684 kB ]).
3. ↑ ^{a b c d e} Peter Liggesmeyer : Software quality . 2nd Edition. Spektrum Akademischer Verlag, Heidelberg 2009, ISBN 978-3-8274-2056-5 , pp. 321-360 .
4. ^ Edmund M. Clarke : Programming Language Constructs for Which it is Impossible to Obtain Good Hoare-like Axiom Systems . In: Journal of the Association for Computing Machinery . tape 26 , no. 1 , 1979, p. 129-147 , doi : 10.1145 / 512950.512952 .