Voici le calcul du PGCD par soustractions successives

while a != b:
    if a > b:
        a = a - b
    else:
        b = b - a

La trace.

Quatre tours, et $\mathrm{PGCD}(48,18)=6$.

La précondition. $a\ge 1$ et $b\ge 1$. Avec $a=0$ et $b=5$, la boucle ferait $b\leftarrow 5-0=5$ indéfiniment : elle ne s'arrêterait jamais.

L'invariant. À chaque tour, $\mathrm{PGCD}(a,b)$ est inchangé — c'est la propriété $\mathrm{PGCD}(a,b)=\mathrm{PGCD}(a-b,b)$ pour $a>b$. Comme à la sortie $a=b$ et que $\mathrm{PGCD}(a,a)=a$, la valeur commune est le PGCD des données de départ.

Le variant. La quantité $a+b$ est un entier strictement positif qui décroît strictement à chaque tour, puisqu'on retranche à l'un des deux une valeur $\ge 1$. Une suite d'entiers positifs strictement décroissante est finie : la boucle s'arrête.

La vérification.

import math

def pgcd_soustractions(a, b):
    """PGCD de a et b par soustractions. Rend le couple (pgcd, nb de tours).

    Precondition : a >= 1 et b >= 1.
    """
    assert a >= 1 and b >= 1
    tours = 0
    while a != b:
        if a > b:
            a = a - b
        else:
            b = b - a
        tours = tours + 1
    return a, tours

for a in range(1, 120):
    for b in range(1, 120):
        assert pgcd_soustractions(a, b)[0] == math.gcd(a, b)

Les $14161$ cas passent, et pgcd_soustractions(48, 18) rend (6, 4) : les quatre tours de la trace.

Le défaut de la méthode : pgcd_soustractions(1, 1000) fait 999 tours pour un résultat évident. C'est le variant qui le dit : $a+b$ ne décroît que de $1$ à chaque tour. L'algorithme d'Euclide par restes corrige cela — banque supplémentaire.