Hoare-Kalkül

Hoare-Kalkül

Der Hoare-Kalkül (auch Hoare-Logik) ist ein Formales System, entwickelt von dem britischen Informatiker C. A. R. Hoare und später verfeinert von Hoare und anderen Wissenschaftlern. Er 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. Alternativ kann auch der wp-Kalkül benutzt werden, bei dem im Gegensatz zum Hoare-Kalkül eine Rückwärtsanalyse stattfindet.

Das zentrale Element des Hoare-Kalküls ist das Hoare-Tripel, das beschreibt, wie ein Programmteil den Zustand einer Berechnung verändert:

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

Dabei nennt man P und Q Zusicherungen (englisch assertions). S ist ein Programmsegment. P heißt die Vorbedingung (englisch precondition), Q heißt die Nachbedingung (englisch postcondition). Zusicherungen sind Formeln der Prädikatenlogik.

Ein Tripel kann auf folgende Weise verstanden werden: Falls P für den Programmzustand vor der Ausführung von S gilt, dann gilt Q danach. Falls S nicht terminiert, dann gibt es kein danach, also kann in diesem Fall Q jede beliebige Aussage sein. Tatsächlich kann man für Q die Aussage false wählen, um auszudrücken, dass S nicht terminiert. Man spricht hier von partieller Korrektheit. Falls S immer terminiert und danach Q wahr ist, spricht man von totaler Korrektheit. Die Terminierung muss unabhängig bewiesen werden.

Inhaltsverzeichnis

Partielle Korrektheit

Der Hoare-Kalkül besteht aus Axiomen und Ableitungsregeln für alle Konstrukte einer einfachen imperativen Programmiersprache:

Zuweisungsaxiom

Das Zuweisungsaxiom besagt, dass nach einer Zuweisung jede Aussage für die Variable gilt, welche vorher für die rechte Seite der Zuweisung galt:

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

P[E / x] ist die Aussage, die dadurch entsteht, dass man in P jedes freie Vorkommen von x durch E ersetzt.

Genau genommen ist das Zuweisungsaxiom kein einzelnes Axiom, sondern ein Schema für eine unendliche Menge von Axiomen, denn x, E und P können jede mögliche Form annehmen, und P[E / x] kann daraus konstruiert werden.

Ein Beispiel für ein durch das Zuweisungsaxiom beschriebenes Tripel ist:

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

Kompositions- oder Sequenzregel

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

Diese Regel kann auf folgende Weise angewendet werden: Wenn die über dem Strich stehenden Aussagen bewiesen worden sind, kann die unter dem Strich stehende Aussage auch als bewiesen angesehen werden.

Betrachtet man zum Beispiel die folgenden beiden Aussagen, die aus dem Zuweisungsaxiom folgen

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

und

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

kann man die folgende Aussage daraus folgern:

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

Auswahlregel (if-then-else-Regel)

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

Die Regel beweist also sowohl den if-Zweig, als auch den else-Zweig.

Iterationsregel (while-Regel)

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

Hierbei wird I als die Schleifeninvariante bezeichnet.

Konsequenzregel

\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 }

Die Konsequenzregel erlaubt es, die Vorbedingung zu verstärken und die Nachbedingung abzuschwächen und so die Anwendung anderer Beweisregeln zu ermöglichen. Insbesondere kann man auch die Vor- oder Nachbedingung durch eine äquivalente logische Formel ersetzen. Beispiel:

\lbrace true \rbrace\ x = 0 \ \lbrace x \geq 0\rbrace\ ist partiell korrekt, denn
\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 }.

Totale Korrektheit

Wie oben erläutert eignet sich das beschriebene Kalkül nur für den Beweis der partiellen Korrektheit. Zum Beweis der totalen Korrektheit kann es durch Erweiterung der while-Regel verwendet werden:

Iterationsregel für totale Korrektheit

\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 \} }

Hierbei ist t ein Term, I die Schleifeninvariante – also das, was in jedem Schleifendurchlauf gilt – und z eine Variable, die in B, t, S und I nicht (frei) vorkommt. Sie dient dazu, den Wert des Terms vor der Schleife mit dem nach der Schleife zu vergleichen. Die Bedingung I \Rightarrow t \geq 0 stellt sicher, dass t nicht negativ wird. Die Idee hinter der Regel ist, dass, wenn t mit jedem Schleifendurchlauf abnimmt, aber nie kleiner als Null wird, die Schleife irgendwann enden muss. t muss dabei aus einer fundierten Menge sein.

Literatur

Weblinks

  • Das Project Bali hat Regeln nach Art des Hoare-Kalküls für ein Subset von Java aufgestellt, zur Benutzung mit dem Theorembeweiser Isabelle
  • Hoare Tutorial Ein Tutorial, das den Umgang mit dem Hoare-Kalkül zur Programmverifikation erklärt (PDF-Datei; 493 kB)
  • j-Algo-Modul Hoare Kalkül Ein Visualisierung des Hoare-Kalküls im Rahmen des Algorithmenvisualisierungsprogramms j-Algo

Wikimedia Foundation.

Schlagen Sie auch in anderen Wörterbüchern nach:

  • Hoare — ist der Name folgender Personen: Mike Hoare (* 1920), britischer Offizier und Söldner Samuel Hoare, 1. Viscount Templewood (1880–1959), britischer Politiker Sean Hoare (1963/64−2011), britischer Journalist Tony Hoare (* 1934), britischer… …   Deutsch Wikipedia

  • Hoare-Logik — Der Hoare Kalkül (auch Hoare Logik) ist ein Formales System, entwickelt von dem britischen Informatiker C. A. R. Hoare und später verfeinert von Hoare und anderen Wissenschaftlern. Er wurde 1969 in einem Artikel mit dem Titel An axiomatic basis… …   Deutsch Wikipedia

  • Hoare-Tripel — Der Hoare Kalkül (auch Hoare Logik) ist ein Formales System, entwickelt von dem britischen Informatiker C. A. R. Hoare und später verfeinert von Hoare und anderen Wissenschaftlern. Er wurde 1969 in einem Artikel mit dem Titel An axiomatic basis… …   Deutsch Wikipedia

  • Kalkül — Als Kalkül (der, das, fr. calcul „Rechnung“; von lat. calculus „Rechenstein, Spielstein“) versteht man in den formalen Wissenschaften wie Logik und Mathematik ein System von Regeln, mit denen sich aus gegebenen Aussagen (Axiomen) weitere Aussagen …   Deutsch Wikipedia

  • Wp-Kalkül — Der wp Kalkül ist ein Kalkül in der Informatik zur Verifikation eines imperativen Programmcodes. Die Abkürzung wp steht für weakest precondition, auf deutsch schwächste Vorbedingung. Die Überprüfung der Korrektheit geschieht durch… …   Deutsch Wikipedia

  • C.A.R. Hoare — Tony Hoare, 2005 Sir Charles Antony Richard Hoare (* 11. Januar 1934 in Colombo, Sri Lanka), besser bekannt als Tony Hoare oder C.A.R. Hoare, ist ein britischer Informatiker. Hoare erlangte hohes Ansehen durch die Entwicklung des Quicksort… …   Deutsch Wikipedia

  • C. A. R. Hoare — Tony Hoare, 2005 Sir Charles Antony Richard Hoare (* 11. Januar 1934 in Colombo, Sri Lanka), besser bekannt als Tony Hoare oder C.A.R. Hoare, ist ein britischer Informatiker. Hoare erlangte hohes Ansehen durch die Entwicklung des Quicksort… …   Deutsch Wikipedia

  • Charles Antony Richard Hoare — Tony Hoare, 2005 Sir Charles Antony Richard Hoare (* 11. Januar 1934 in Colombo, Sri Lanka), besser bekannt als Tony Hoare oder C.A.R. Hoare, ist ein britischer Informatiker. Hoare erlangte hohes Ansehen durch die Entwicklung des Quicksort… …   Deutsch Wikipedia

  • wp-Kalkül — Der wp Kalkül ist ein Kalkül in der Informatik zur Verifikation eines imperativen Programmcodes. Die Abkürzung wp steht für weakest precondition, auf deutsch schwächste Vorbedingung. Bei der Verifikation geht es nicht darum, die Funktion mit… …   Deutsch Wikipedia

  • Hoarekalkül — Der Hoare Kalkül (auch Hoare Logik) ist ein Formales System, entwickelt von dem britischen Informatiker C. A. R. Hoare und später verfeinert von Hoare und anderen Wissenschaftlern. Er wurde 1969 in einem Artikel mit dem Titel An axiomatic basis… …   Deutsch Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”