Algorithmus von Euklid

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 ∈$\mathbb {N}$ 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.