Introduction
En informatique, écrire un algorithme correct ne consiste pas seulement à obtenir un résultat qui semble juste sur quelques exemples. Tester un programme permet de déceler des erreurs, mais tester n’est pas prouver : un test montre seulement que l’algorithme fonctionne dans certains cas, pas dans tous. Pour démontrer qu’un algorithme est toujours correct et qu’il finit par s’arrêter, on utilise deux outils fondamentaux : les invariants, qui décrivent une propriété vraie à chaque étape de l’exécution, et les variants, qui assurent la terminaison. Cette démarche s’inscrit dans une logique scientifique : prouver la validité d’une méthode, et non seulement l’observer empiriquement.
Les invariants : une vérité qui reste constante
Un invariant est une propriété logique qui demeure vraie tout au long de l’exécution d’une boucle, depuis son entrée jusqu’à sa sortie. Il sert de témoin de la progression de l’algorithme.
Exemple : dans un algorithme de tri par insertion, à chaque étape, on insère un élément à la bonne place dans une sous-liste déjà triée. L’invariant est donc : après la i-ème étape, les i premiers éléments de la liste sont triés. Cette propriété reste vraie tant que l’algorithme s’exécute, et garantit que lorsque la boucle est terminée, la liste entière est bien triée.
Autre exemple simple : dans une boucle qui calcule la somme des n premiers entiers naturels, l’invariant peut être formulé ainsi : à chaque étape i, la variable somme contient la valeur de 1 + 2 + … + i. Cet énoncé est vérifiable à chaque étape et justifie la correction du calcul.
À retenir
Un invariant est une propriété logique qui reste vraie à chaque étape d’une boucle. Il permet de prouver que l’algorithme construit bien ce qu’il prétend produire.
Les variants : montrer que l’algorithme s’arrête
Un algorithme doit non seulement être correct, mais aussi terminer. Pour cela, on utilise la notion de variant, c’est-à-dire une quantité numérique qui diminue à chaque étape de la boucle et qui ne peut pas descendre indéfiniment.
Exemple : dans une recherche dichotomique d’un élément dans un tableau trié, l’intervalle de recherche est divisé par deux à chaque étape. Le variant est donc la taille de l’intervalle, qui est toujours un entier naturel. Comme il décroît strictement à chaque itération et qu’il est borné inférieurement par 0, il ne peut pas diminuer indéfiniment. On est donc assuré que la boucle s’arrête.
Dans une boucle qui répète « tant que n > 0 », et où à chaque itération on fait n = n − 1, le variant est la valeur de n. Cet entier naturel décroît à chaque étape et atteint forcément 0, moment où la boucle se termine.
À retenir
Un variant est une valeur entière qui décroît strictement à chaque itération et qui est bornée inférieurement. Il garantit que l’algorithme ne s’exécute pas à l’infini.
Exemple concret : la recherche d’un minimum
Prenons l’exemple d’un algorithme simple qui recherche le minimum d’un tableau de nombres.
1. On suppose qu’au départ, le premier élément est le minimum.
2. On parcourt ensuite le tableau en comparant chaque élément avec le minimum courant, que l’on met à jour si nécessaire.
Dans cet algorithme, l’invariant est : après avoir examiné les i premiers éléments, la variable min contient le plus petit de ces i éléments. Cet énoncé est toujours vrai et prouve que, lorsque l’on a parcouru tout le tableau, min contient bien le plus petit élément de tous.
La terminaison est assurée par le fait que la boucle parcourt exactement n éléments, donc elle s’arrête après un nombre fini d’étapes. Ici, le variant est la position de l’indice i, un entier naturel qui croît jusqu’à n.
Cet exemple illustre comment invariants et variants se complètent : l’invariant prouve la correction, et le variant prouve la terminaison.
À retenir
L’invariant décrit la justesse du raisonnement tout au long de l’algorithme, tandis que le variant prouve que la boucle s’arrête. Ensemble, ils démontrent que l’algorithme fonctionne.
Conclusion
Montrer qu’un algorithme fonctionne ne consiste pas seulement à l’exécuter sur quelques exemples, mais à prouver sa validité et sa terminaison. Les invariants permettent de garantir que la propriété recherchée reste vraie à chaque étape, et les variants assurent que le processus ne s’éternise pas. Cette distinction entre tester et démontrer est fondamentale en algorithmique, car elle transforme une simple observation en certitude formelle. Dans la suite du parcours, d’autres méthodes de preuve permettront d’aborder des algorithmes plus complexes, toujours avec l’objectif d’assurer leur correction et leur terminaison.