Variant non trivial — l'algorithme d'Euclide

Exercice · informatique (tronc commun des prépas scientifiques), chapitre 1 — La discipline de programmation

Énoncé

Prouver la terminaison de la boucle while suivante en exhibant un variant :

def pgcd(a: int, b: int) -> int:
    while b > 0:
        a, b = b, a % b
    return a

Démonstration : Choisissons pour variant la valeur de la variable b.

Positivité : Tant que la boucle s'exécute, la condition b > 0 garantit que notre variant reste strictement positif.
Décroissance : À chaque itération de la boucle, la valeur de b est remplacée par a % b. Par définition mathématique de la division euclidienne, le reste $a mod b$ appartient à l'ensemble ${0, 1, \dots, b - 1}$ . Le nouveau b est donc strictement inférieur à l'ancien. La suite des valeurs successives prises par b est une suite d'entiers naturels strictement décroissante, ce qui prouve la terminaison de la boucle.

Un blocage sur cet exercice ? Le tuteur d'Adloun guide par questions, sans donner la réponse.