Terminaison et Correction

Contenus

Lorsque l’on crée un algorithme, il faut tenir compte des trois critères suivant : la terminaison, la correction et la complexité.

La terminaison garantit que l’algorithme se termine au bout d’un certain nombre d’opérations élémentaires. La correction garantit que l’algorithme donne le résultat attendu lorsqu’il se termine.

Exemple

Un être humain et un chien ne vieillissent pas de la même manière. Pour déterminer l’équivalent humain de l’âge d’un chien de moins de 15kg, on utilise le tableau ci-dessous, où x représente l’âge réel de l’animal (en années), et y l’équivalent humain en terme de vieillissement.

Soit l’algorithme suivant :

Vérifions la terminaison. Il s’agit d’une suite de conditionnement avec des calculs élémentaires à l’intérieur. Une fois toutes les conditions vérifiées dans l’ordre, l’algorithme se termine.

Pour ce qui est de la correction, l’algorithme effectue bien les opérations décrites dans le tableau.

Exemple difficile

En général, la terminaison est difficile à vérifier car on ne connaît pas toujours, a priori, le nombre d’instructions effectuées. La correction est compliquée lorsqu’on est en présence d’aide à la décision ou de recherche opérationnelle. Il faut alors utiliser des principes mathématiques pour prouver que l’algorithme est correct.

Prenons l’exemple du calcul du pgcd en itératif.

L’algorithme se termine si la condition d’arrêt de la boucle se réalise, c’est à dire si y s’annule. Dans la boucle, y est remplacé par un reste modulo y. Donc à chaque passage, y décroit strictement tout en restant positif ou nul. Par conséquent, y finit par atteindre 0, on sort alors de la boucle. L’algorithme se termine bien après un certain nombre d’itération.

Au départ, x=a et y=b. Dans la boucle, on remplace (x,y) par (y, x mod y). On sait que pgcd(x,y)=pgcd(y, x mod y). Donc à chaque itération, pgcd(x,y)=pgcd(a,b). En sortie de boucle, on a y=0, or pgcd(x,0)=x. Par récurrence on en déduit qu’on renvoie pgcd(a,b). L’algorithme calcule bien le pgcd souhaité.

Outil pour la terminaison et la correction

On appelle convergent une quantité qui prend ses valeurs dans un ensemble bien fondé et qui diminue strictement à chaque passage dans une boucle. Un ensemble bien fondé est un ensemble totalement ordonné dans lequel il n’existe pas de suite infinie strictement décroissante. L’existence d’un convergent pour une boucle garantit que l’algorithme finit par en sortir. Par exemple, dans le cas de l’algorithme d’Euclide, y est un convergent.

On appelle invariant de boucle une propriété qui, si elle est vraie à l’entrée dans une boucle, reste vraie après chaque passage dans cette boucle. Elle est donc vraie à la sortie de cette boucle. L’invariant de boucle est analogue au principe de récurrence. La mise en évidence d’un invariant de boucle adapté permet de prouver la correction d’un algorithme. Par exemple, pgcd(a,b)=pgcd(x,y) est un invariant de boucle.

Nous prendrons en exemple un algorithme avec aléatoire afin de tester les notions de terminaison et de correction.

En informatique, l’aléatoire attribut une valeur dans un intervalle de valeur. Le pseudo-aléatoire est soit limité par la taille du conteneur (int, double, etc) soit par l’algorithme utilisé (génération d’un nombre modulo un très grand nombre). Dans l’algorithme, nous supposons que n et p sont des nombres entiers strictement positif. Si ces derniers ont une opération le rendant négatif, alors la valeur de 0 sera automatiquement attribué.

Dans la deuxième partie de la condition, x décroit tandis que y possède une valeur aléatoire (strictement bornée). x tend donc vers la valeur 0. Dans la première partie de la condition, y décroit vers 0 à partir de sa valeur aléatoire. Nous en concluons donc que l’algorithme fait décroître y à 0, puis décrémente x avant de redonner une valeur à y.

Par récurrence nous en concluons que x tendra vers 0 après un certain nombre d’itération, donc que la deuxième partie ne sera plus visité. Et y tend aussi vers 0, donc nous sortons de la boucle. Nous avons donc prouver que l’algorithme se termine. Il n’est pas utile de parler de correction dans ce cas puisque nous n’avions pas de cahier des charges à vérifier.

Il est a noté que certain algorithme ne possède pas de preuve de terminaison que la célèbre fonction de Syracuse.