Frage: Euklid-Korrektheit. ggT(a; b) = ggT(a' - b'; b') = ggT(a'; b') ?
Ich habe Probleme beim Nachvollziehen dieser Lösung:
Beweis.
A und B seien die ursprünglichen Werte bei Aufruf von Euklid(a,b,ggt).
a' und b' seien die Werte von a und b vor Ausführen des Schleifenrumpfs.
Terminierung: Bei jedem Durchlauf der Schleife wird entweder a oder b um den Wert der anderen Variablen reduziert. Da sie natürliche Zahlen sind, müssen sie nach endlich vielen Schritte gleich werden.
Korrektheit: Behauptung ggT(A;B) = ggT(a; b) ist eine Schleifeinvariante:
Bei Eintritt gilt A = a und B = b. O. B. d. A. sei a > b.
Nach Ausführen des Rumpfs gilt a = a' - b' und b = b'
Und damit ggT(a; b) = ggT(a' - b'; b') = ggT(a'; b') (Satz).
(Hier meine Frage: Ich verstehe ggT(a;b) = ggT(a' - b'; b'), da man hier einfach nur das neue a; b bekommt, indem man die Werte vor dem Ausführen jeweils abzieht. Aber wieso schließt man daraus nun auf ggT(a'; b') ?
Ist das weil man mit ggT(a' - b'; b') man ab diesem Punkt sich nach dem Schleifendurchgang befindet und ggT(a',b') schon den die Werte vor dem neuen Schleifendurchgang beschreibt?
Weil nehmen wir an a = 5 und b = 2, dann wäre vor Schleifeneintritt ggT(A,B) = ggT(a;b) und ggT(a',b') = ggT(a;b), weil ja am Anfang a' = a und b' = b gilt. (a' und b' = Werte vor Ausführung der Schleife)
ggT(a; b) = ggT(a' - b'; b') = ggT(a'; b')
ggT(5;2) = ggT (5 - 2; 2) =/= ggT(5;2)
Das a' und b' ändert sich ja nicht während der Schleife.
Da bei Schleifeneintritt ggT(a0; b0) = ggT(A;B) war, folgt ggT(A;B) = ggT(a; b) nach Ausfuhrung des Schleifenrumpfs.
Die Korrektheit folgt dann direkt aus der Schleifeninvariante.