Validierung von Programmen

Überblick

Häufig leisten Programme nicht, was von ihnen erwartet wird. Manchmal ist das nur störend; manchmal kostet das irgendjemanden Geld; und manchmal besteht die Möglichkeit, daß zum Beispiel ein computergesteuertes Flugzeug durch einen Programmierfehler abstürzt und Menschen verletzt oder getötet werden. Spätestens in solchen Fällen muß man sich sehr genau Gedanken darüber machen, wie man möglichst sicher sein kann, daß ein Programm keine Fehler enthält.

Es gibt in der Informatik zu diesem Thema ein geflügeltes Wort: „There is always one more bug.“ „Bug“ bedeutet einen Programmierfehler. Die Erfahrung, daß jedes Programm Fehler hat, machen Informatikerinnen schon lange. Es wird auf verschiedenste Weise versucht, die Fehleranfälligkeit in Programmen zu vermindern.

Die meistbenutzte Methode ist der Test von Programmen: Man probiert das Programm oder die einzelnen Teile mit verschiedenen, möglichst systematisch ausgewählten Eingabedatensätzen aus, betrachtet die Ergebnisse und entscheidet dann, ob das Programm einen Fehler gemacht hat oder nicht; wenn ein Fehler vermutet wird, dann wird genauer nachgeforscht, wie das unerwartete Programmverhalten zustande kam.

Von vielen Menschen wird ein anderes Verfahren, der formale Beweis von Programmen, als die sicherste Methode angesehen: Man spezifiziert fmöglichst formal — etwa mit den vorgestellten formalisierten Sprachen — was ein zu untersuchender Programmteil leisten soll und versucht dann Schritt für Schritt nachzuweisen, daß die Anweisungsfolge, aus der das Programm besteht, die Anforderungen erfüllt. Theoretisch kann man auf diese Weise die Korrektheit eines Programms nachweisen, ohne es je laufen zu lassen.

Wir wollen uns in diesem Kapitel um Stärken und Schwächen dieser beiden bekannten Methoden kümmern.