Terminaison et correction de l'algorithme
La terminaison de l'algorithme de recherche dichotomique est cruciale pour garantir qu'il s'arrêtera toujours, quelle que soit l'entrée. Pour prouver la terminaison, on utilise le concept de variant de boucle.
Vocabulaire: Un variant de boucle est une valeur entière positive ou nulle qui décroît strictement à chaque itération de la boucle.
Dans le cas de la recherche dichotomique, le variant de boucle est la différence entre les indices droite
et gauche
. Cette valeur décroît strictement à chaque itération, assurant ainsi la terminaison de l'algorithme.
La correction de l'algorithme est démontrée en utilisant la technique de l'invariant de boucle. Un invariant de boucle est une proposition qui reste vraie à chaque itération.
Définition: Un invariant de boucle pour la recherche dichotomique est : "Si la valeur recherchée est dans le tableau, son indice est compris entre gauche et droite."
La démonstration de la correction montre que cet invariant reste vrai pour chacun des trois cas possibles à chaque itération : la valeur est trouvée, elle est dans la moitié gauche, ou elle est dans la moitié droite.
Highlight: La preuve de terminaison et de correction garantit que l'algorithme de recherche dichotomique fonctionne correctement et s'arrête toujours, ce qui est essentiel pour son utilisation fiable dans des applications pratiques.