Écrire un variant pour la boucle while n!= 1

Le variant : n lui-même.

Entier et positif : n est entier par hypothèse, et la division entière d'un entier strictement positif par $2$ reste positive ou nulle. En fait elle reste $\ge 1$ : si $\text{n}\ge 2$, alors $\text{n}//2\ge 1$.

Strictement décroissant : on entre dans le corps seulement si $\text{n}\ne 1$, donc — n étant $\ge 1$ — si $\text{n}\ge 2$. Et pour $\text{n}\ge 2$, $\lfloor \text{n}/2\rfloor <\text{n}$, l'inégalité étant stricte.

Une suite d'entiers $\ge 1$ strictement décroissante est finie : la boucle s'arrête, et elle s'arrête sur n $=1$, puisque c'est la seule valeur $\ge 1$ qui ne permet pas d'entrer.

Le nombre de tours : $\lfloor {\log }_{2}n\rfloor$. Chaque tour retire un bit à l'écriture binaire de n (chapitre 1) ; on s'arrête quand il n'en reste qu'un. Un entier $n$ s'écrit sur $\lfloor {\log }_{2}n\rfloor +1$ bits, donc il faut $\lfloor {\log }_{2}n\rfloor$ tours.

Vérification : l'égalité a été contrôlée pour tous les $n$ de $1$ à $20000$ — elle tient partout.

Le piège de la précondition. Pour $n=0$, la boucle ne s'arrête jamais : $0//2=0$, et $0\ne 1$. Le variant n'y décroît pas. Pour $n$ négatif, c'est pire : $-3//2=-2$ en Python, la suite décroît sans jamais valoir $1$ — le variant décroît bien, mais il n'est pas positif, et c'est cette hypothèse-là qui manque. Un variant a trois conditions, et les trois servent.