Fachkonzept - Korrektheit
Gewünschtes und tatsächliches Verhalten eines Algorithmus
Oft findet man folgende Situation vor: Gesucht ist ein Algorithmus, der ein bestimmtes Verhalten haben soll. Nachdem man einen Algorithmus entwickelt hat, stellt sich die Frage, ob er das gewünschte Verhalten tatsächlich auch zeigt.
Beispielsweise könnte das Problem darin bestehen, einen Algorithmus zur Berechnung des größten gemeinsamen Teilers zweier natürlicher Zahlen zu entwickeln. Das gewünschte Verhalten könnte man so beschreiben:
vorher: x = a; y = b; a, b sind natürliche Zahlen größer als 0 nachher: x = y = ggT(a, b)
Folgender Algorithmus wird zur Lösung des Problems vorgeschlagen:
Es ergibt sich die Frage, ob der Algorithmus tatsächlich das gewünschte Verhalten hat.
Korrektheit bzgl. einer Spezifikation
Zur Beschreibung der oben beschriebenen Situation führen wir Fachbegriffe ein.
Das Verhalten von Algorithmen beschreibt man mit Spezifikationen.
Eine Spezifikation besteht aus einer Vorbedingung, die einen Ausgangszustand beschreibt, sowie einer Nachbedingung, die einen Endzustand beschreibt.
Spezifikationen werden benötigt, um die Korrektheit von Algorithmen zu erfassen.
Ein Algorithmus heißt terminierend bzgl. einer Spezifikation, wenn er bei jedem Ausgangszustand, der die Vorbedingung erfüllt, nach endlich vielen Verarbeitungsschritten zu einem Ende kommt.
Ein Algorithmus heißt (total) korrekt bzgl. einer Spezifikation, wenn er terminierend ist und jeden Ausgangszustand, der die Vorbedingung erfüllt, in einen Endzustand überführt, der die Nachbedingung erfüllt.
Wenn ein Algorithmus entwickelt wird, dann soll er korrekt bzgl. einer vorgegebenen Spezifikation sein. Nur, worauf stützt sich die Aussage, dass ein entwickelter Algorithmus tatsächlich korrekt ist?
Korrektheit testen
Beim Testen eines Algorithmus wird der Algorithmus mit vorgegebenen Testdaten ausgeführt. Dabei wird überprüft, ob er in diesen Fällen das gewünschte Verhalten zeigt.
Zum Wechselwegnahme-Algorithmus könnten z.B. diese Tests durchgeführt werden:
Testfälle: vorher: x = 24; y = 15 nachher: x = 3; y = 3 ok vorher: x = 10; y = 25 nachher: x = 5; y = 5 ok vorher: x = 15; y = 7 nachher: x = 1; y = 1 ok vorher: x = 8; y = 8 nachher: x = 8; y = 8 ok vorher: x = 1; y = 4 nachher: x = 1; y = 1 ok
Folgende Regeln sollten bei der Wahl der Testfälle und der Durchführung von Tests beachtet werden:
Testfälle sollten immer sorgfältig ausgewählt werden. Man sollte sowohl typische als auch untypische Augangsdaten betrachten. Besondere Aufmerksamkeit ist auf Sonderfälle und Grenzwerte zu richten. Unter letzteren versteht man Werte, die gerade noch als Ausgangsdaten zugelassen sind (z. B. größter und kleinster Wert, leerer Text, leere Eingabe usw.). Oft ist es auch günstig, zufällig erzeugte Testfälle zu verwenden.
Da man in der Regel nicht alle denkbaren Fälle durchspielen kann, bleibt oft die Ungewissheit, ob man nicht irgendwelche Sonderfälle übersehen hat.
Mit Testmethoden kann man das Vorhandensein von Fehlern entdecken. Man kann aber mit solchen Methoden meist nicht mit absoluter Gewissheit nachweisen, dass ein Algorithmus korrekt bzgl. der gegebenen Spezifikation ist.
Korrektheit verifizieren
Absolute Gewissheit erhält man, wenn man die Korrektheit eines Algorithmus mit Hilfe eines mathematischen Beweises zeigt. Ist ein solcher Beweis erbracht, dann kann es keine Testfälle geben, die dem spezifizierten Verhalten nicht entsprechen.
Das Beweismuster sieht für den Wechselwegnahme-Algorithmus so aus:
Vor.: x = a; y = b; a, b sind natürliche Zahlen größer als 0
Beh.: Der Algorithmus "Wechselwegnahme" terminiert für x, y
und liefert das Ergebnis x = y = ggT(a, b)
Bew.: ...
Korrektheitsbeweise sind - insbesondere bei komplexen oder umfangreichen - Algorithmen schwer zu führen. Wir werden daher auf solche Korrektheitsnachweise verzichten.
