Korrektheit verifizieren

Ein Beweis (für Mathematiker)

Ziel ist es zu beweisen, dass der ggT-Algorithmus korrekt bzgl. der angegebenen Spezifikation ist.

Voraussetzung: Wir gehen davon aus, die Vorbedingung erfüllt ist, d.h., dass x = a; y = b gilt und dass a und b natürliche Zahlen ungleich 0 sind.

Behauptung: Der Algorithmus liefert das Ergebnis x + y = ggT(a,b).

Beweis:

Wir zeigen zunächst, dass Algorithmus nach endlich vielen Schritten zu einem Ende kommt und ein Ergebnis liefert.

Der Algorithmus startet mit zwei natürlichen Zahlen x = a und y = b, die nach Voraussetzung beide größer als 0 sind. In jedem Schleifendurchlauf wird eine der beiden Zahlen verkleinert. Es ist leicht einzusehen, dass man nicht unendlich oft eine der beiden Zahlen verkleinern kann, so dass beide weiterhin größer als Null bleiben. Bei der Ausführung des Algorithmus kann man also nicht in eine Endlosschleife geraten.

Für die weitere Argumentation benötigen wir die folgende Eigenschaft des größten gemeinsamen Teilers:

Für beliebige natürliche Zahlen m und n mit m >= n gilt: 
ggT(m, n) = ggT(m-n, n).

Dabei legen wir fest, dass ggT(z, 0) = z bzw. ggT(0, z) = z gelten soll, wenn z eine beliebige natürliche Zahl ist. Es soll also z.B. ggT(4, 0) = 4 gelten.

Diese Eigenschaft wird weiter unten separat nachgewiesen.

Wir zeigen als nächstes, dass die folgende Bedingung vor dem ersten und nach jedem Schleifendurchlauf erfüllt ist:

{ggT(x, y) = ggT(a, b)}

Vor dem ersten Schleifendurchlauf gilt selbstverständlich diese Bedingung, da hier x = a und y = b gilt.

Als nächstes zeigen wir, dass die genannte Bedingung nach einem Schleifendurchlauf noch gilt, sofern sie vorher bereits erfüllt war. Wir nehmen also an, dass die Bedingung ggT(x, y) = ggT(a, b) vor einem Schleifendurchlauf gilt. Die Werte der Variablen x und y nach der Ausführung der Schleifenanweisungen bezeichnen wir mit x' und y'. Es gilt x' = x - y und y' = y oder x' = x und y' = y - x. Jetzt nutzen wir die oben angegebene allgemeine Eigenschaft des ggT aus. Aus ihr folgt, dass in jedem Fall ggT(x', y') = ggT(x, y) gelten muss. Da ggT(x, y) = ggT(a, b) vorausgesetzt war, folgt, dass ggT(x', y') = ggT(a, b) nach dem Schleifendurchlauf gilt.

Insgesamt ergibt sich jetzt, dass nach Abarbeitung aller Schleifendurchläufe die Bedingung ggT(x, y) = ggT(a, b) immer noch erfüllt ist.

Kommt es zum Verlassen der Schleife, so gilt entweder x = 0 oder y = 0.

Im Fall x = 0 erhält man: ggT(x, y) = ggT(0, y) = y = x+y.

Im Fall y = 0 erhält man analog: ggT(x, y) = ggT(x, 0) = x = x+y.

Kombiniert man jetzt die Ergebnisse, so erhält man: x+y = ggT(x, y) = ggT(a, b).

Damit ist der Beweis erbracht, dass Algorithmus tatsächlich das spezifizierte Verhalten hat.

Entscheidend für den Beweis war die zusätzlich ins Spiel gebrachte Bedingung ggT(x, y) = ggT(a, b). Sie stellt die sogenannte Schleifeninvariante dar. Das ist eine Bedingung, die während der Schleifenausführungen stets erfüllt bleibt.

Aufgabe 1

Begründe, dass der ggT die folgende Eigenschaft hat:

Für beliebige natürliche Zahlen m und n mit m >= n gilt: 
ggT(m, n) = ggT(m-n, n).

Gehe dabei wie folgt vor:

Zeige: Wenn t ein Teiler von m und n (mit m >= n) ist, dann ist t auch ein Teiler von m-n.

Zeige: Wenn t ein Teiler von m-n und n (mit m >= n) ist, dann ist t auch ein Teiler von m.

Benutze diese Ergebnisse, um die Eigenschaft zu begründen.