Hoare logic

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

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

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

• 3.1 Iterationsregel for total correctness

Hoare triples

The central element of the Hoare calculus is the Hoare triples, describes how a part of the program changes the state of a computation:

Here, and assurances (English assertions ), is a program segment. is the precondition (English precondition ) and the postcondition (English postcondition ). If the condition is true after the execution of Programmsegements applies the postcondition. Assertions are formulas of predicate logic.

A triple can be understood in the following way: If the program state before execution of holds, then applies thereafter. If not terminated, then there is no after, ie can be any statement in this case. Indeed, one can choose false for the statement to express that not terminated. This is called partial correctness. If ever terminated and thereafter is true, it is called total correctness. The termination must be independently proven.

If no condition exists, one writes:

Partial correctness

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

Axiom of the empty statement

If a program segment does not change any variables, also the assertions do not change, so it is the same postcondition precondition:

Assignment axiom

The assignment axiom states that each statement is true after an assignment for the variable, which was previously on the right side of the assignment:

Is the statement that caused when one replaces in every free occurrence of through.

Strictly speaking, the assignment axiom no single axiom, but a schema for an infinite set of axioms, then, and can assume any form, and can be constructed from it.

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

Composition or sequence rule

In order to analyze sequential programs, each triple can be linked according to the following rule:

This rule can be applied in the following manner: If the statements standing above the line have been demonstrated, which is under the bottom line statement can be regarded as proven.

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

And

We can conclude the following statement from:

Selection rule ( if-then -else rules)

The following rule applies for selection constructs with 2 choices:

Thus, the rule proves both the if - branch and the else branch. Has an if - query no else branch, you use a slightly modified version of this rule:

Iterationsregel ( while- rule)

This is referred to when the loop invariant, both before, during and after execution of the loop is valid. An invariant must be determined manually.

Consequence rule

The consequence rule allows to strengthen the precondition and weaken the postcondition and to enable the application of other rules of evidence. In particular, one can also replace the pre-or postcondition by an equivalent logical formula. example:

Total correctness

As explained above, the calculus described is suitable only for the proof of partial correctness. To prove the total correctness of the while - rule must be extended by a loop variant. It is a feature or a variable which represents a number having an initial value. It must now be shown that is reduced in each loop, and the loop from a specific, reduced value terminated.

Iterationsregel for total correctness

This is a term that loop invariant - that is, what applies in each loop - and a variable that occurs in, and not (Free). It serves to compare the value of the term before the loop after the loop. The condition ensures that it is not negative. The idea behind the rule is that if decreases with each pass through the loop, but never less than zero, the loop has to end sometime. has to be from a well-founded set.

Assessment

With the Hoare calculus and a formal specification, it is possible to examine a program or parts of a program for correctness. It is one of the few methods that can actually prove correctness and not merely the absence of errors. However, the results of an analysis with the Hoare calculus must be treated with caution:

• The specification is incorrect, although the results of the analysis can be accurate, but to a wrong specification.
• With the Hoare calculus no errors are found, arising from errors in the programming language itself or the compiler.
• The Hoare calculus encountered in large software systems, especially with global variables and recursion to its limits.
• In order to verify the axioms of computer arithmetic must be used that take into account the specifics of how the boundedness of the natural numbers and the inaccuracy of large floating point numbers.