Mon programme est-il correct ?
Preuve d'un programme : le PGCD
Avec sa méthode de calcul du plus grand commun diviseur (PGCD) de deux nombres entiers, Euclide a inventé, vers l’an 300 avant J. C., l’un des premiers algorithmes connus. La preuve de validité du programme correspondant est un «classique» de l’informatique. Mais prouver des programmes complexes est bien plus difficile…
Le programme ci-dessous réalise l'algorithme du PGCD d'après Euclide. Mais ce programme est-il correct ? Fait-il bien ce qu’on lui demande ?
Dans le programme, la flèche ← signifie : donner à la variable à gauche de la flèche la valeur de l’expression à droite de celle-ci. Vous pouvez essayer le programme en choisissant différentes valeurs de a et de b (après avoir introduit chaque valeur, cliquer dessus) , et observer le déroulement du programme soit en continu, soit pas à pas.
Remarquons que le programme comporte une boucle, ou répétition d’un «pas» : la construction tant que.
La première question est : le programme va-t-il s’arrêter ou va-t-il «tourner» indéfiniment ? Si a et b sont égaux, x et y le sont aussi au départ. La boucle ne s’exécute pas et le PGCD est la valeur commune de x et y (donc de a et b). Si x et y sont différents, un pas de la boucle se décrit ainsi : retrancher le plus petit de ces nombres du plus grand, et donner ce résultat comme valeur à la variable (x ou y) qui contenait le plus grand. L’effet d’un pas de la boucle est donc le suivant : si x et y étaient positifs (ce que nous supposons avant de le démontrer plus loin), ils le restent, et la valeur du plus grand des deux diminue. Les valeurs successives de la plus grande des deux variables x et y au cours de l’exécution forment une suite de nombres entiers positifs qui décroissent. Cette suite va donc nécessairement s’arrêter (au pire des cas à la valeur 1, qui est le plus petit entier positif). Par ailleurs, x et y sont positifs avant le premier pas de la boucle (car ils ont les valeurs de a et b, positifs) ; ils restent donc positifs dans toute la boucle. Quand le programme s’arrête, x et y sont égaux et le résultat délivré est leur valeur commune.
La seconde question est : qu’est-ce qui prouve que ce résultat est bien le PGCD de a et b ? Supposons que x > y avant un pas de la boucle et soit p le PGCD de x et y. Après exécution du pas, la nouvelle valeur de x est x - y, et y n’a pas changé. Alors p, qui divise x et y, divise y et la nouvelle valeur de x. De plus, c’est le plus grand de leurs diviseurs communs ; car s’il y avait un diviseur commun plus grand que p, il diviserait aussi y et l’ancienne valeur de x, donc p ne serait pas leur PGCD. Ainsi la valeur du PGCD de x et y ne change pas au cours de l’exécution de la boucle (on dit que c’est un invariant). Or à la fin de la boucle, x = y et leur PGCD est leur valeur commune. À cause de la propriété d’invariance, ce PGCD est aussi celui de x et y tels qu’ils étaient au début de la boucle. C’est donc bien le PGCD de a et b.
Cette démonstration illustre des techniques utilisées pour la preuve de programmes (trouver une fonction décroissante positive pour montrer l’arrêt d’une boucle, et identifier des invariants). Malheureusement, dès que le programme devient un peu complexe, la difficulté de la preuve augmente très rapidement, ce qui rend vain l’espoir de la réaliser «à la main». Un espoir de progrès réside dans l’usage des assistants de preuve, qui obtiennent des résultats remarquables, mais dont l’usage est encore réservé à des spécialistes.