Algorithmus	Einführung Definition Definitionen Flussdiagramme Struktogramme Korrektheit Verifikation Testen Rekursion Literatur Standard-Algorithmen Numerik Links Pfad: Startseite / Fächer / Informatik / Algorithmus / Korrektheit
Autor: mk 06.12.2005 13:52 2681	Algorithmus

Korrektheit eines Algorithmus:

1. Formale Methode (Verifikation):
   Mittels logischer Herleitungen wird die Einhaltung der Bedingungen an die Zwischen- und Endergebnisse des Algorithmus bzw. Programms nachgewiesen.
2. 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).