Korrektheit eines Algorithmus:
aus R.Baumann, Informatik SII, Band 1, Klett 1992, S.185:
Ein Algorithmus heißt
korrekt, wenn er seiner Spezifikation genügt, d. h. wenn er zu allen
Eingabedaten, die der Vorbedingung genügen, die Ausgabedaten erzeugt, welche die Nachbedingung
erfüllen. Die Überprüfung eines Algorithmus bzw. Programms hinsichtlich Korrektheit kann auf
zwei grundsätzlich verschiedene Weisen erfolgen:
- Formale Methode (Verifikation):
Mittels logischer Herleitungen wird die Einhaltung der Bedingungen an die Zwischen- und
Endergebnisse des Algorithmus bzw. Programms nachgewiesen.
- Empirische Methode (Testen):
Mit bestimmten ausgesuchten Daten, für die das Ergebnis bekannt ist, wird der Algorithmus
bzw. das Programm erprobt. Dabei kann lediglich das Vorhandensein von Fehlern entdeckt,
nicht jedoch die Fehlerfreiheit nachgewiesen werden.
- Entscheidend bei der Verifikation ist neben dem Nachweis des Abbrechens (der Termination)
das Auffinden einer Schleifeninvariante, d. h. einer Aussageform, die nach jedem
Schleifendurchlauf wahr ist, wenn sie es vorher war. Die Wahrheit der Schleifeninvarianten
und das Zutreffen der Abbruchbedingung erlaubt den Schluß, daß die erstrebte Nachbedingung
erreicht ist, der Algorithmus also tut, was in der Spezifikation verlangt wird.
- Nicht erst zur nachträglichen Analyse eines Algorithmus ist die Aufstellung einer
Schleifeninvarianten hilfreich; man sollte dies vielmehr schon beim Entwurf tun. Die Idee
der Schleifeninvarianten ist häufig gleich der Entwurfsidee, in die mathematisches Wissen
über den betrachteten Gegenstand eingeht.
- Der Methode der Programmverifikation stellen sich in der Praxis große Hindernisse entgegen.
Bei umfangreichen Programmen ist ein formaler Korrektheitsbeweis der geschilderten Art i. d.
R. nicht möglich. Unsere Beispiele betrafen vergleichsweise wenig umfangreiche mathematische
Algorithmen, deren Spezifikation seit Jahrhunderten bekannt ist. In der Praxis besteht das
eigentliche Problem jedoch im Entwickeln eines geeigneten Modells (...), und es ist zu
prüfen, ob das Modell "auf die Wirklichkeit paßt". Erst wenn dies gesichert ist, kann die
Verifikation beginnen. In der Praxis ändern sich Spezifikationen laufend, das Modell wird
abgewandelt. Daher ist man dort auf die - zugegebenermaßen unvollkommene - Methode des
empirischen Testens angewiesen.
- Regeln zur Wahl von Testdaten: Man wähle sowohl typische als auch untypische Eingabewerte.
Besondere Aufmerksamkeit ist auf Sonderfälle und Grenzwerte zu richten. Unter letzteren
versteht man Werte, die gerade noch als Eingabewerte zugelassen sind (z. B. größter und
kleinster Wert, leerer Text, leere Eingabe usw.). Man sollte auch zufällige Testdaten
verwenden, selbst wenn diese nicht sinnvoll erscheinen mögen, denn mit ihnen lassen sich
Testlücken aufgrund scheinbarer Selbstverständlichkeiten vermeiden.
- Regeln zur Testdurchführung: Man notiere vor der Durchführung des Testlaufs, welche Ausgabe
das Programm laut Spezifikation liefern soll. Man prüfe nicht nur, ob das Programm tut,
was es soll, sondern auch, ob es etwas tut, was es nicht soll (z. B.: hat eine Prozedur
unerwünschte Nebenwirkungen?)
- Regeln zur Testvereinfachung: Man entwerfe Algorithmen bzw. Programme testfreundlich, d. h.,
man befolge die Grundsätze des strukturierten Programmentwurfs und baue ggf. geeignete
Testhilfen (z. B. Meßpunkte) ein.
- Maßnahme zur Fehlerlokalisierung: An markanten Stellen des Programms werden
Ausgabeanweisungen eingefügt (sogenannte Kontrollausgaben), um den aktuellen Programmzustand
zu erfassen.
- Häufige Fehlerquellen:
- Schleifen, die entweder einmal zu oft oder einmal zu wenig durchlaufen werden,
- Nicht initialisierte Variablen,
- Bereichsüberschreitung von Variablen (z. B. Indexüberschreitung bei Reihungen),
- Unerwartete Nebenwirkungen von Prozeduren und Funktionen, insbesondere bei Verwendung
globaler Variablen,
- Numerische Überraschungen (z. B. Rundungsfehler, Auslöschung führender Ziffern bei
Subtraktion benachbarter Zahlen).
