Hoare-Kalkül

Der Hoare-Kalkül (auch Hoare-Logik oder Floyd-Hoare-Kalkül) ist ein formales System, um die Korrektheit von Programmen nachzuweisen. Er wurde von dem britischen Informatiker C. A. R. Hoare entwickelt und später von ihm und anderen Wissenschaftlern verbessert. Der Hoare-Kalkül wurde 1969 in einem Artikel mit dem Titel An axiomatic basis for computer programming veröffentlicht.

Der Zweck des Systems ist es, eine Menge von logischen Regeln zu liefern, die es erlauben, Aussagen über die Korrektheit von imperativen Computer-Programmen zu treffen und sich dabei der mathematischen Logik zu bedienen. Hoare knüpft an frühere Beiträge von Robert Floyd an, der ein ähnliches System für Flussdiagramme veröffentlichte. Im Gegensatz zum floydschen Verfahren, bei dem Ausführungspfade interpretiert werden, arbeitet der Hoare-Kalkül mit dem Quellcode.

Alternativ kann auch der wp-Kalkül benutzt werden, bei dem im Gegensatz zum Hoare-Kalkül eine Rückwärtsanalyse stattfindet.

↑ Charles Antony Richard Hoare: An Axiomatic Basis for Computer Programming (Memento vom 4. März 2016 im Internet Archive) (PDF; 659 kB). In: Communications of the ACM. Bd. 12, Nr. 10, 1969, S. 576–585, doi:10.1145/363235.363259.
↑ Robert W. Floyd: Assigning meanings to programs. In: Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Nr. 19, 1967, S. 19–31 (virginia.edu [PDF; 684 kB]).
↑ Peter Liggesmeyer: Software-Qualität. 2. Auflage. Spektrum Akademischer Verlag, Heidelberg 2009, ISBN 978-3-8274-2056-5, S. 321–360, doi:10.1007/978-3-8274-2203-3.

[Primärquelle-1] Charles Antony Richard Hoare: An Axiomatic Basis for Computer Programming (Memento vom 4. März 2016 im Internet Archive) (PDF; 659 kB). In: Communications of the ACM. Bd. 12, Nr. 10, 1969, S. 576–585, doi:10.1145/363235.363259.

[Floyd-2] Robert W. Floyd: Assigning meanings to programs. In: Proceedings of the American Mathematical Society Symposia on Applied Mathematics. Nr. 19, 1967, S. 19–31 (virginia.edu [PDF; 684 kB]).

[Software-Qualität-3] Peter Liggesmeyer: Software-Qualität. 2. Auflage. Spektrum Akademischer Verlag, Heidelberg 2009, ISBN 978-3-8274-2056-5, S. 321–360, doi:10.1007/978-3-8274-2203-3.