Introduction :

Lorsque l’on écrit un algorithme, on souhaite plusieurs choses :

1. Que cet algorithme se termine (pas de boucle infinie), on parle alors de terminaison de l'algorithme.

2. Qu’il produise le résultat attendu (algorithme correct), on parle alors de correction de l'algorithme.

3. Qu’il soit le plus rapide possible et nécessite le moins de mémoire possible, on parle alors de complexité de l'algorithme (voir autre leçon).

Réaliser la preuve d’un algorithme, c’est :

• Prouver qu’il se termine : c'est donc prouver sa terminaison.

• Prouver qu’il fait bien ce que l’on attend de lui : c'est donc prouver sa correction.

Ces problèmes sont directement liés à l’algorithme et pas à son implémentation dans un langage particulier. En général, on procède en effectuant des tests sur l’algorithme, mais lorsque le cout humain ou financier d’une erreur est trop important, on aimerait pouvoir démontrer que l’algorithme est correct.

I) Terminaison d’un algorithme : variant de boucle

On s’intéresse ici à la terminaison des boucles. Il n’y a pas de problème avec les boucles for dont le nombre d’itération est connu à l’avance. Le problème apparait avec les boucles while pour lesquelles on ne sait pas a priori si la condition de terminaison sera vérifiée.

Exemple :

def f(n):    

    #n un entier

    if not (type(n)==int and n>=0):

        return None

    compteur=2

    produit=1

    while n-compteur>=0:

        produit=produit*compteur

      compteur+=1

  return produit

1. Le programme précédent se termine-t-il toujours, quelle que soit l’entrée ?

Oui, si on n’a pas un entier positif, on retourne none, si l’entier est inférieur à 1 on ne rentre pas dans la boucle while et s’il est plus grand que 2, on considère i = n − compteur, c’est un entier qui décroit strictement à chaque itération.

2. Quel est son but ?

Son but est de calculer n!, c'est à dire factoriel de n : n*(n-1)*(n-2)*...*1, avec n entier positif. Par convention, 0! = 1.

Terminaison de boucle :

Un moyen usuel de démontrer la terminaison d’une boucle est de trouver une quantité, fonction des paramètres de la boucle, qui est un entier positif et qui décroit strictement à chaque itération. Cette quantité est appelée variant de boucle.

Remarques :

— Il existe des moyens plus complexes de démontrer qu’une boucle se termine en faisant intervenir plusieurs expressions, nous ne les verrons pas cette année.

— Il est parfois impossible de démontrer qu’une boucle se termine même si on le vérifie toujours expérimentalement (exemple : suite de syracuse).

II) Correction d’un algorithme : invariant de boucle

Une fois que l’on a démontré qu’un algorithme se termine effectivement, il serait agréable de savoir si celui-ci produit le résultat attendu. Par exemple une fonction qui se termine tout le temps pourrait être

def factorielle(n):

return 1 # retourne n!, mais ne marche que pour 0 et 1

Cette fonction se termine tout le temps mais ... n’est pas très intéressante.

Les instructions simples ne posent pas de problème. Les problèmes arrivent en général lorsque l’on a des boucles. Pour ce paragraphe, on n’écrira que des boucles while (on peut toujours ré-écrire une boucle for en boucle while) avec un seul point d’entrée (pas d’instruction du type « go to » qui n’existe de toutes façons pas en python) et un seul point de sortie (pas de break ou de return au milieu de la boucle).

Exercice :

Montrer par récurrence que le terme général de la suite définie par u₀ = 2 et u_n+1 = (1/3) u_n peut s’écrire u_n = 2 / 3ⁿ.

Si n = 0, on a u₀ = 2, ce qui est bien u_n = 2 / 3⁰ = 2, la propriété est vérifiée au rang 0.

Si n > 0, supposons que u_n = 2 / 3ⁿ et montrons que u_n+1 = 2 / 3ⁿ⁺¹.

On a u_n+1 = (1/3) u_n = u_n / 3 = 2 / (3ⁿ * 3) = 2 / (3ⁿ⁺¹)

La propriété est donc vraie au rang n+1 donc elle est vraie pour tout n.

En informatique, on procède en général d’une façon similaire :

Invariant de boucle :

Pour démontrer qu’un algorithme produit le résultat attendu, on utilise un invariant de boucle, c’est-à-dire une propriété qui :

• est vérifiée avant d’entrer dans la boucle

• si cette propriété est vérifiée avant une itération, elle est vérifiée après celle-ci

• lorsqu’elle est vérifiée en sortie de boucle, elle permet (combinée avec la condition de sortie de boucle) d’en déduire que le programme produit le résultat attendu.

def puissance(k,n): # calcule kⁿ en supposant n > 0

c=n

p=1

# invariant de boucle : P = k^n-c et c >= 0 ; condition d’entrée dans la boucle c > 0

while c>0: # p = k^n-c et c >= 0 et c > 0

p=k*p # p = k^n-c+1 = k^n-(c-1) et c > 0

c=c-1 # p = k^n-c et c >= 0

# (p = k^n-c et c >= 0) et non (c > 0)

return p # (p = k^n-c et c >= 0) et c <= 0 ⇒ p = kⁿ

Remarques :

• Raisonnement analogue aux raisonnements par récurrence :

1. On vérifie que l’invariant de boucle est vrai avant d’entrer dans la boucle (P₀ est vrai).

2. On montre que s’il est vrai au début d’une itération, alors il est vrai à la fin (P_k ⇒ P_k+1).

3. À la fin de la boucle P_kmax est vrai et la condition d’entrée dans la boucle est fausse (sinon on ne serait pas sorti).

• Toute la difficulté est de trouver le bon invariant de boucle.