Hoare-Kalkül

Der Hoare-Kalkül (auch Hoare-Logik) 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 verfeinert. 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.

This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.