Théorème : une suite strictement décroissante d'entiers relatifs prend nécessairement des valeurs négatives.
Pour montrer qu'une boucle se termine, on peut montrer l’existence d’un variant de boucle.
Un variant de boucle est une quantité, associée à une boucle et permettant de prouver sa terminaison.
C'est souvent un entier positif tout au long de l’algorithme et qui décroît strictement après chaque itération .
n=6
p=1
while n>0:
p=p*n
n=n-1
print(n,p)
0 720
$n$ est un variant de boucle.
En notant $n_k$ et $p_k$ les valeurs de $n$ et $p$ après la $k$ème itération de la boucle, on a $\forall k\in\mathbb{N}$, $n_{k+1}=n_k-1$.
$(n_k)_{k\in\mathbb{N}}$ est donc une suite strictement décroissante d'entiers et donc la boucle se termine bien.
u=6
while u!=1:
print(u)
if u%2==0:
u=u//2
else:
u=3*u+1
6 3 10 5 16 8 4 2
Cette suite est appelée la suite de Syracuse.
On ne sait pas démontrer si la boucle se termine pour toute valeur de $u_0$ ou pas
Une boucle for bien écrite se termine toujours.
p=10
r=1
for i in range(1,p+1):
r=r*i
print(r)
3628800
La boucle se termine
p=10
r=1
for i in range(1,p+1):
r=r*i
i=i-2
print(r)
3628800
Mal écrite mais elle se termine quand même
Exemple d'une boucle for qui ne se termine pas :
L=[1,2,3]
for i in L:
L.append(i)
# a est un réel et n un entier naturel non nul
a,n = 3,6
r = 1
while n > 0:
if n%2 == 1:
r = r*a
a = a**2
n = n//2
print(r)
729
$n$ est un variant de boucle.
On note $n_k$ la valeur de $n$ après $k$ itérations de la boucle, si pour tout $k$, $n_k>0$, la suite $(n_k)$ est une suite strictement décroissante d'entiers : $n_{k+1}\leqslant \frac12 n_k<n_k$ ce qui n'est pas possible.
Il existe donc un entier $k$ tel que $n_k=0$ et la boucle se termine.
# a et b sont des entiers naturels non nuls
a,b = 60,16
while b > 0:
c = a % b
a = b
b = c
print(a,b,c)
4 0 0
$b$ est un variant de boucle. La boucle se termine.