input: a >= 1, b >= 1; // a = A, b = B
while (a /= b) {
// Invariante: gcd(a,b) = gcd(A,B)
// Variante: max (a,b)
if a > b then a := a - b else b := b - a
}
output: a // a = gcd(A,B)
Beweis:
- Termination: die Variante ist
∈
und
streng fallend.
- Korrektheit: die Invarianz folgt aus
gcd(a, a) = a
,
gcd(a - b, b) = gcd(a, b)
.
- Beweise dafür: mit gcd-Definition.
Johannes Waldmann
2015-12-11