Pour vérifier la correction (caractère correct) d’un programme informatique, on se contente souvent de l’essayer sur une batterie de tests, ce qui n’est suffisant que si l’on essaye tous les cas possibles ! Avant de passer à cette étape, on a intérêt à bâtir son programme sur sa preuve. En fait, le problème ne se pose que dans le cas des boucles itératives ou récursives.
Références
La logique. Bibliothèque Tangente 15, 2004.
Mathématiques et informatique. Bibliothèque Tangente 52, 2014.
Les démonstrations. Bibliothèque Tangente 55, 2015.
Suite à 11 (18). Bernard Frize, 2006.
Plus délicat : le cas des fonctions itératives
Il est en général plus difficile de prouver qu’un programme fournit le résultat attendu pour une fonction itérative (c’est-à-dire structurée sur une boucle comme « répéter », « tant que» ou « pour ») que pour une fonction récursive. Les preuves sont fondées sur la notion d’invariant de boucle.
Voyons le cas du calcul du PGCD (plus grand diviseur commun) de deux nombres avec l’algorithme d’Euclide. L’idée lumineuse attribuée à Euclide consiste à remarquer que le PGCD de deux nombres a et b est le même que celui de a et b modulo a, c’est-à-dire du reste d dans la division euclidienne de a par b. On a alors le programme suivant en pseudo-code :
Pgcd(a,b)=
On introduit une variable supplémentaire d
Répéter
d:=a mod b
a:=b
b:=d
jusqu’à ce que d=0
retourner a
L’invariant de boucle est : « Les diviseurs communs de a et b sont les mêmes à chaque étape. » D’autre part, la suite des valeurs de d est strictement décroissante, ce qui assure la sortie de boucle. Cet algorithme peut être mis sous forme récursive :
PgcdRec(a,b)=
Si a=0, retourner b
Sinon retourner PgcdRec(b mod a, a)
Ce programme se prouve alors sans difficulté par récurrence sur l’entier a.
Programmer, c’est prouver : le cas des fonctions récursives
Le corps d’une fonction récursive comporte en général deux parties : le traitement du cas de base et la partie récursive proprement dite, ce qui est à rapprocher du raisonnement par récurrence. L’exemple classique est le calcul de la factorielle d’un nombre entier positif. Voici un exemple en pseudo-code :
Factorielle(n)=
Si n=0, retourner 1
Sinon retourner n*Factorielle(n-1)
La preuve que la fonction Factorielle retourne bien le produit de tous les entiers de 1 à n (noté n!) pour tout entier naturel n s’effectue par récurrence. La démonstration se fait en lisant les lignes du programme précédent. Formalisons le raisonnement en considérant P(n) la propriété « Factorielle(n) retourne n! ».
P(0) est vraie d’après la première ligne du programme. Supposons maintenant que P(n–1) soit vraie pour un entier n ≥ 1 et examinons P(n).
Factorielle(n) fait appel à Factorielle(n-1) qui, d’après l’hypothèse de récurrence, retourne (n–1)! La seconde ligne du programme retourne donc n×(n–1)!, qui vaut n!, donc P(n) est vraie. Ainsi, P(0) est vraie, et si P(n–1) est vraie P(n) l’est également. D’après le principe de récurrence, P(n) est donc vraie pour tout entier naturel n.
En fait, cette preuve suit exactement la programmation de la fonction. On peut résumer cela en affirmant que, dans ce cas, programmer, c’est prouver !