Der Umgang mit dem Hoare-Kalkül zur Programmverifikation

Michael Gellner

Einführung in die Verifikation

Der Umgang mit dem Hoare-Kalkül zur Programmverifikation

1 Allgemeines

1.1 Ursprung

Schon in den frühen eiten der Programmierung trat das Bedürfnis auf, die entstandenen Artefakte auf deren Korrektheit hin analysieren zu können und sich nicht nur auf die Suche nach Fehlern beschränken zu müssen: Alan Turing hat sich dieser Fragestellung bereits 1949 gewidmet [Tur 49], fortgesetzt wurde dieser Gedanke dann im Wesentlichen von Floyd, dessen Artikel aus dem Jahr 1967 als eine Wurzel der Verifikation angesehen werden kann [Flo 67]. Hierauf aufbauend hat Hoare das 1969 vorgestellte System der axiomatischen Semantik entwickelt [Hoa 69]. Tatsächlich ist diese häufig auch als Hoare-Kalkül bezeichnete Methode der Verifikation also nicht ausschließlich das Werk von C.A.R Hoare. Die Regel zum Beweis der totalen Korrektheit von Schleifen geht nicht auf Hoare sondern auf eine lange eit nach Hoares Artikel veröffentlichte Arbeit von Dijkstra zurück [Dij82], die Regel für bedingte Anweisungen stammt von Lauer [Lau71]. Ein weiterer falscher Eindruck der leicht entstehen kann ist der, dass die Begriffe Hoare-Kalkül und Verifikation synonym zueinander verwendet werden können. war wird in vielen Lehrveranstaltungen des Grundstudiums unter dem Begriff Verifikation lediglich die Hoaresche Logik behandelt, tatsächlich ist Verifikation mittlerweile ein recht umfangreiches Themengebiet, in dem der Hoare-Kalkül lediglich eine Methode unter vielen darstellt. ahlreiche Spezialisierungen, die im Laufe der Jahre entwickelt wurden, z.B. für parallele, verteilte, nichtdeterministische oder auch disjunkte parallele Programme, dienen dem weck der Verifikation, werden aber über andere Formalismen, Axiome und Regelsysteme als ausschließlich der Hoarschen Logik realisiert. Ein Beispiel ist das Model Checking, eine Verifikationsmethode für reaktive Systeme, hierbei handelt es sich um Systeme, die mit ihrer Umgebung in Aktions/Reaktionsbeziehungen treten, ein anderes die Programmanalyse, die sich im Gegensatz zum Hoare-Kalkül automatisieren lässt. Die axiomatische Semantik im Hoarschen Sinne lehnt sich stark an Ideen an, wie sie am ehesten in der imperativen Sprache Pascal umgesetzt sind. Tatsächlich für Pascal entwickelt (auch der Eindruck entsteht aufgrund der inhaltlichen Nähe des Hoare-Kalküls zu den Konstrukten der Sprache Pascal gelegentlich unzutreffender Weise) ist der Hoare-Kalkül hingegen nicht. Hoares ursprüngliche Veröffentlichung ‚An axiomatic basis for computer programming’ stammt aus dem Jahr 1969. Der Entwickler der Sprache Pascal, Niklaus

Wirth, publiziert diese Sprache erstmals 1971 [Wir71]. Hoare hat seine Systematik 1973 mit Wirth zusammen unter einem ähnlich Titel (An Axiomatic Definition of the Programming Language Pascal) um einem Focus auf Pascal erweitert [HM 73]. Die Nähe der Hoarschen Logik zur Sprache Pascal resultiert aus der gemeinsamen Arbeit von Hoare und Wirth ab Mitte der 60er Jahre; einige Ideen von Wirth haben Hoare sicherlich bei der Entwicklung seiner Axiome inspiriert, der ebenfalls an Belangen der Semantik und Korrektheit interessierte Wirth hat aber im Gegenzug die Sprache Pascal auch entlang der Ideen von Hoare entworfen, offensichtlich so, dass sich zumindest die damals bekannte partielle Korrektheit damit zeigen ließ. Neben zahlreicher Kritik an der axiomatischen Semantik ‚von außen’ also an deren Anwendung schlechthin, an deren Kompliziertheit etc. – dies wird weiter hinten ausführlicher diskutiert – ist seit einer einschlägigen Publikation von Clarke 1979 auch ein schwererwiegender inhaltlicher Mangel bekannt: Sobald das Prozedurkonzept reichhaltig genutzt wird, ist es prinzipiell unmöglich, ein vollständiges Hoarsches Beweissystem zu finden [Cla 79]. Dies auch dann, wenn man sich auf logische Strukturen mit einem endlichen Datenbereich einschränkt. Damit kommt die Hoare’sche Logik in der Praxis relativ schnell an ihre Grenzen, denn kaum ein Softwaresystem, das heute realen Anforderungen genügen muss, kann aus Gründen der Komplexität in monolithischer Form erstellt werden.

1.2 Was ist der weck des Hoare-Kalküls?

Grundsätzlich besteht der Wunsch nach Software die fehlerfrei ist, die Erfahrung zeigt hingegen, dass bereits fehlerarme Software die Ausnahme darstellt und garantiert fehlerfreie sich bislang als nicht realisierbar erweist. Nach Faustregeln zur Häufigkeit von Fehlern ist beispielsweise bei einem Projekt wie Windows NT 5.0 mit einem Umfang von bis zu 27 Millionen eilen Code zunächst von rund 6 Millionen enthaltenen Fehlern auszugehen. Diese lassen sich durch Testen finden. Hierzu gibt es verschiedene Techniken wie Black Boxoder White-Box Tests, Anweisungs-, Bedingungs- und Pfadüberdeckungen und viele andere mehr. Je Testlauf – so besagt eine andere Faustregel – kann man damit rechnen, ca. 30 % der Fehler zu finden. Rund 20 Durchläufe jedes Systemteils führen dann langsam zu einer akzeptablen Fehlerquote, zu einem ustand, in dem ein System dann zumindest vermarktet werden kann. Auch dies ein Unterfangen, das für unter 200 Millionen US-Dollar nicht realisierbar ist [Lov 98]. Man sieht an diesem Beispiel auch deutlich, dass wirkliche Fehlerfreiheit nicht im Entferntesten zu erwarten ist. Ein Alternative zum Testen ist das Vermeiden von Fehlern bzw. das direkte Finden von Abweichungen zwischen Spezifikation und Implementation. Mit Testen lässt sich also immer nur ermitteln, wenn etwas nicht korrekt läuft, die bereits vorliegende Korrektheit läßt sich damit jedoch nicht zeigen. Wird beim Testen kein Fehler mehr gefunden, heißt dies auch keineswegs zwingend, daß ein Programm fehlerfrei ist, sondern nur, daß die gewählte Teststrategie keine Fehler mehr zutage fördert. Die Verifikation beansprucht für sich, direkt zu beweisen, daß ein Programm fehlerfrei ist.

Testen vs. Verifikation: n Testen bedeutet das Suchen von Fehlern n Verifikation will die Korrektheit eines Programms zeigen

---

Michael Gellner

Einführung in die Verifikation

Michael Gellner A = „Der Eiffelturm steht in München.“ B = „Berlin ist pleite.“ C = „Im Himmel ist Jahrmarkt.“

Einführung in die Verifikation

Überprüfung von Software – Begriffe Verifikation: Eine Methodik zum Durchführen eines formalen Beweises, der zeigen soll, dass ein Programm P eine Spezifikation S erfüllt. Testen: Das Überprüfen eines Programms P mittels einer Testmenge T, ob P für T die Spezifikation S erfüllt. Validierung: Überprüfung der Spezifikation S, ob diese die Anforderungen A tatsächlich erfüllt.

2 Voraussetzungen

Die Verifikation bedient sich häufig der Logik, genauer der Teilgebiete Aussagenlogik, und Prädikatenlogik, daher gilt es sich damit vertraut zu machen, soweit dies nicht der Fall ist.

Die Aussagenlogik liefert nun Syntax und Semantik, um mit solchen Aussagenvariablen hantieren zu können. Hierfür gibt es logische Operatoren wie etwa Negation, Konjunktion und Disjunktion. Um zu sehen wie dies auf die Wahrheitswerte wirkt, berücksichtigt man alle Werte, die eine Aussagevariable annehmen kann und notiert das Ergebnis des Operators nach Anwendung auf die Aussagevariable. Negation Eine Verneinung bzw. Negation wendet den Sinn einer Aussage. Dies entspricht der Benutzung des Wortes nicht. Die Negation ist unär, d.h. sie hat nur einen Operanden. A wahr falsch ØA falsch wahr

2.1 Aussagenlogik und Prädikate

Aussagenlogik beschäftigt sich mit Aussagen, Aussageformen und deren Verknüpfungen. Einige Aspekte der Aussagen- und Prädikatenlogik, die bei der Verifikation von Bedeutung sind, werden hier wiederholt. Die entsprechende einschlägige Literatur (z.B. Schöning, Logik für Informatiker [Sch 95]) kann und will dieser Abschnitt nicht ersetzen. Aussagen Eine Aussage nichts anderes als ein Satz, der (sinnvoll) mit wahr oder falsch bewertet werden kann. Beispiele: „Der Eiffelturm steht in München.“ „Berlin ist pleite.“ „Im Himmel ist Jahrmarkt.“ „Die ahl 7 ist prim“ Wichtig ist lediglich, dass sich eine Aussage formal als wahr oder falsch beantworten lässt, auch wenn, wie bei der dritten Aussage eine Bestätigung oder Verneinung von niemanden wirklich gegeben werden kann. Die beiden möglichen Beurteilungen einer Aussage wahr oder falsch werden als Wahrheitswerte bezeichnet. Im Gegensatz zu den obigen Beispielen sind folgende Sätze hingegen keine Aussagen: „Wie spät ist es jetzt?“ „Komm her.“ „Hey, Du da drüben.“ „Hilfe!“ Keine Aussagen sind Fragen, Befehle, einzelne Worte sowie sinnlose eichenfolgen. Um mit den Aussagen einfacher arbeiten zu können, werden sie mit Variablen gleichgesetzt, die in der Logik meist Grossbuchstaben sind. Also:

Eine Verneinung bzw. Negation wendet den Sinn einer Aussage. Dies entspricht der Benutzung des Wortes nicht. Die Negation ist unär, d.h. sie hat nur einen Operanden. Konjunktion Die Verundung bzw. Konjunktion verknüpft zwei Aussagen und liefert ein Ergebnis für beide Aussagen. Für die verknüpfte oder Gesamtaussage gilt hierbei, dass sie nur wahr sein, wenn beide Teile bereits wahr sind, in allen anderen Fällen resultiert für die Gesamtaussage ebenfalls der Wahrheitswert falsch. Die Konjunktion ist binär. A wahr falsch wahr falsch Beispiel: Die Aussagen A = „Wenn man über 18 ist, kann man einen Führerschein machen.“ B = „Wenn man einen Sehtest besteht, kann man einen Führerschein machen.“ lassen sich entsprechend der Konjunktion zu A Ù B verknüpfen: A Ù B = „Wenn man über 18 ist und eine Sehtest besteht, kann man einen Führerschein machen.“ Implikation Die Folgerung bzw. Implikation verknüpft wiederum zwei Aussagen zu einer. In diesem Fall so, dass die Gesamtaussage auch dann bereits als wahr 4 B wahr wahr falsch falsch AÙB wahr falsch falsch falsch

---

Michael Gellner

Einführung in die Verifikation

Michael Gellner junktion als auch für die Exklusion verwendet. A wahr falsch wahr falsch Beispiel: Die Aussagen B wahr wahr falsch falsch

Einführung in die Verifikation

gilt, wenn eine der beiden Aussagen A oder B bereits wahr ist. Die Implikation steht für die Beziehung, „wenn … dann …“ A wahr falsch wahr falsch B wahr wahr falsch falsch A®B wahr wahr falsch wahr

AÅB falsch wahr wahr falsch

u beachten sind die Festlegungen der eilen 2 und 4. Kann aus etwas Falschem etwas Wahres folgen? Aus logischer Sicht ja, aus falschen Daten kann zunächst immer alles folgen (das ist häufig das Verhängnisvolle). Wenn man falsch misst, rechnet oder eine Fehlerquelle in einem Versuchsaufbau hat, kann man zufällig immer auf ein (tatsächlich) richtiges Ergebnis oder ein falsches Ergebnis kommen. Die Wahl von wahr ist im Fall falscher Vorderglieder von Implikationen per Definition gefunden worden. Beispiel: Die Aussagen A = „BILD schreibt immer die Wahrheit .“ B = „BILD ist gut.“ lassen sich entsprechend der Implikation zu A ® B verknüpfen: A ® B = „Wenn Bild immer die Wahrheit schreibt, dann folgt, dass Bild gut ist.“ Äquivalenz Der Vergleich bzw. die Äquivalenz gleicht die Wahrheitswerte zweier Aussagen ab. Wenn beide Aussagen gleiche Wahrheitswerte haben (also auch wenn beide falsch sind) ist die Äquivalenz wahr. A wahr falsch wahr falsch Beispiel: Die Aussagen A = „BILD schreibt die Wahrheit.“ B = „BILD lügt nicht.“ lassen sich entsprechend der Äquivalenz zu A « B verknüpfen: A « B = „Bild schreibt genau dann die Wahrheit, wenn sie nicht lügt.“ Exklusion (Antivalenz) Die ausschließende Veroderung bzw. Exklusion stellt eine Veroderung dar, bei nur eine Teilaussage wahr sein darf, damit die Gesamtaussage wahr liefert (entweder nur A oder nur B, nicht beides und auch nicht keines von beiden). In unserer Alltagssprache wird das Wort „oder“ sowohl für die Dis5 B wahr wahr falsch falsch A«B wahr falsch falsch wahr

A = „Man kann reinkommen.“ B = „Man kann rauskommen.“ lassen sich entsprechend der Äquivalenz zu A Å B verknüpfen: A Å B = „Man kann rein- oder rauskommen.“ Neben diesen gebräuchlichen Kombinationen der Belegung zweier Variablen mit Wahrheitswerten gibt es weitere, wie die Identität (unär), NAND oder NOR (binär), die hier nicht weiter betrachtet werden. Häufiger von Bedeutung können noch die Formeln von de Morgan sein, die wichtige Beziehungen zwischen Aussagetermen wiedergeben: (i) (ii) Ø(A Ù B) Û Ø(A) Ú Ø(B) Ø(A Ú B) Û Ø(A) Ù Ø(B)

Um aussagenlogische Ausdrücke formulieren und auswerten zu können, muss eine Syntax vorliegen, die die Reihenfolge festlegt, in der zusammengesetzte Terme zu verarbeiten sind und Klammern aufgelöst werden müssen. Mit der Aussagenlogik können also lediglich Aussagen gebildet und dann der Wahrheitswert bestimmt werden. Die Prädikatenlogik erweitert die Ausdrucksmöglichkeiten der Aussagenlogik, dies wird ergänzt um Prädikate bzw. Prädikatsymbole und um Quantoren. Prädikate (Aussageformen) Prädikate sind Sätze, die Variablen enthalten und die beim Ersetzen dieser Variablen mit Elementen einer gegebenen Menge eine Aussage bilden (also auf die Menge {wahr, falsch} abbilden). Beispiele: „Der Eiffelturm ist x Meter hoch“ (das heißt implizit: x Î Ñ) „Die ahl n ist prim.“ (implizit n Î Í) Prädikate können von beliebiger Stelligkeit sein: „Der ggT von i und j ist n.“ (implizit: i, j, n Î Í) „Der x-te Kaiser von China heißt y.“ (implizit: x Î Í und y Î String)

6