Programmverifikation

Halteproblem

 aufwärts

Mit den Methoden der Programm­verifikation 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 Programm­stück formal zu beweisen, deckt erbarmungs­los Fehler, implizite Annahmen und sonstige Ungenauig­keiten auf.

Bei größeren Programmen stoßen diese Techniken an Grenzen. Letztlich ist es sogar grund­sätzlich unmöglich, die Korrektheit von beliebigen Programmen zu beweisen. Dies hängt mit der Nicht-Entscheid­bar­keit des Halteproblem zusammen.

 

Halteproblem
Gegeben:Programm P
Gefragt:Terminiert P?

 

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:

boolean halts(String p)
{
    if (p interpretiert als Programm terminiert)
        return true;
    else
        return false;
}

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 Schleifen­körper. Die Schleifen­bedingung ist ein Aufruf der Funktion halts, diese erhält als Parameter einen Aufruf des Programms test selbst:

void test()
{
    while (halts("test();"));
}

 

Wir betrachten nun, was die Funktion halts tut, wenn sie mit dem Programm test als Parameter aufgerufen wird. Es lassen sich zwei Fälle unter­scheiden, je nach dem, ob das Programm test terminiert oder nicht:

 

  1. test terminiert  folgt  halts liefert true  folgt  While-Schleife in test läuft endlos  folgt  test terminiert nicht
  2. test terminiert nicht  folgt  halts liefert false  folgt  While-Schleife in test wird sofort verlassen  folgt  test terminiert

 

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

 

homeH.W. Lang   Hochschule Flensburg   lang@hs-flensburg.de   Impressum   ©  
Valid HTML 4.01 Transitional

Hochschule Flensburg
Campus Flensburg

Informatik in Flensburg studieren...

 

Neu gestaltetes Studienangebot:

Bachelor-Studiengang
Angewandte Informatik

mit Schwerpunkten auf den Themen Software, Web, Mobile, Security und Usability.

Ihr Abschluss
nach 7 Semestern:
Bachelor of Science

 

Ebenfalls ganz neu:

Master-Studiengang
Angewandte Informatik

Ein projektorientiertes Studium auf höchstem Niveau mit den Schwerpunkten Internet-Sicherheit, Mobile Computing und Human-Computer Interaction.

Ihr Abschluss
nach 3 Semestern:
Master of Science

 

Weitere Informatik-Studienangebote an der Hochschule Flensburg:

Medieninformatik

Wirtschaftsinformatik