Mit den Methoden der Programmverifikation ist es möglich, die Korrektheit von sehr einfachen Programmen zu beweisen. In vielen Fällen enthalten Programme Teilstücke, die einfach genug sind, dass sie formal verifiziert werden können. Der Versuch, ein solches Programmstück formal zu beweisen, deckt erbarmungslos Fehler, implizite Annahmen und sonstige Ungenauigkeiten auf.
Bei größeren Programmen stoßen diese Techniken an Grenzen. Letztlich ist es sogar grundsätzlich unmöglich, die Korrektheit von beliebigen Programmen zu beweisen. Dies hängt mit der Nicht-Entscheidbarkeit des Halteproblem zusammen.
Satz: Es ist nicht entscheidbar, ob ein beliebiges gegebenes Programm bei jeder Eingabe terminiert oder nicht.
Der Beweis dieser Tatsache ist sogar sehr einfach [GSchn 94]. Angenommen, die folgende Funktion existiert:
Die Funktion erhält als Parameter einen Programmtext p und gibt true zurück, falls das Programm p terminiert und false sonst.
Ferner sei folgendes Programm test gegeben. Es besteht aus einer While-Schleife mit leerem Schleifenkörper. Die Schleifenbedingung ist ein Aufruf der Funktion halts, diese erhält als Parameter einen Aufruf des Programms test selbst:
Wir betrachten nun, was die Funktion halts tut, wenn sie mit dem Programm test als Parameter aufgerufen wird. Es lassen sich zwei Fälle unterscheiden, je nach dem, ob das Programm test terminiert oder nicht:
In beiden Fällen ergibt sich also ein Widerspruch – daher muss die Annahme falsch sein, dass die Funktion halts existiert.
[GSchn 94] D. Gries, F.B. Schneider: A Logical Approach to Discrete Math. Springer (1994)
Weiter mit: [Aufgaben] [Literatur] oder [up]