Korrektheit als Problem

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 informell so beschreiben:

Übergabe: zwei natürliche Zahlen a und b, die größer als 0 sind
Rückgabe: 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:

vorher:  x = a;  y = b; a und b sind natürliche Zahlen größer als 0
nachher: x+y = ggT(a, b)

In diesem Fall sagen wir, dass der Algorithmus korrekt bzgl. der vorgegebenen Spezifikation ist.

Aufgabe 1

Was meinst du, ist der gezeigte Algorithmus korrekt bzgl. der vorgegebenen Spezifikation? Wie kann man das ggf. überprüfen?