Invariant de boucle : démontrer la correction d'une boucle

Pour montrer qu'une boucle se termine, on peut montrer l'existence d'un variant de boucle

Pour montrer la correction d'une boucle, on peut montrer l’existence d’un invariant de boucle.

Un invariant de boucle est une propriété qui est vraie avant la boucle et qui reste vraie à chaque passage de la boucle. (lié au principe de récurrence)

Exemples

n=6
p=1
while n>0:
    p=p*n
    n=n-1
print(n,p)

Calcul de $n!$

On note $n_k$ et $p_k$ les valeurs de $n$ et $p$ après $k$ itérations de la boucle.

Un invariant de boucle : $p_k\times n_k!=a!$

Un variant de boucle : $n$

# n entier naturel
n=5
r=1
i=0
while  i < n:
    r = r*2
    i = i+1
print(r)

Calcul de $2^n$

On note $r_k$ et $i_k$ les valeurs de $r$ et $i$ après $k$ itérations de la boucle.

invariant de boucle : $r_k=2^k$

variant de boucle : $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)

Exponentiation rapide : calcul de $a^n$

invariant de boucle : $a^n = {a_k}^{n_k}\times r_k$

variant de boucle : $n$

Version récursive :

def puiss(a,n):
    if n == 0:
        return 1
    if n%2 == 1:
        return a*puiss(a**2,n//2)
    return puiss(a**2,n//2)

puiss(2,10)

On montre par récurrence forte sur $n$ que la fonction retourne $a^n$

# 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)

calcule le pgcd de $a$ et $b$

invariant de boucle : pgcd$(a,b) = $pgcd$(a_k,b_k)$

variant de boucle : $b$