Terminaison du tri par insertion
On cherche à prouver la terminaison du tri par insertion.
Question
Quel variant doit-on considérer pour prouver la terminaison du tri par insertion ?
Solution
Fondamental : Variant du tri par insertion
Comme pour le tri par sélection, dans l'algorithme du tri par insertion, le variant à considérer est la taille de la partie triée.
Question
Quelle est la condition de terminaison ?
Indice
Quelle condition sur la valeur du variant provoque la terminaison de l'algorithme ?
Solution
Fondamental : Condition d'arrêt du tri par insertion
Comme pour le tri par sélection, dans l'algorithme du tri par insertion, la condition de terminaison est le fait que la taille de la partie triée soit égale à la taille de la liste.
Question
Prouver la terminaison du tri par insertion à l'aide du variant.
Indice
La preuve est très similaire à celle pour le tri par sélection.
Solution
Méthode : Terminaison du tri par insertion
On a quelques propriétés de base sur notre variant :
Au début de l'exécution de l'algorithme la taille de la partie triée est nulle ;
A chaque insertion, la taille de la partie triée croit exactement de 1 ;
Lorsque la taille de la partie triée atteint la taille de la liste alors l'algorithme s'arrête.
On sait que l’algorithme s'arrête dès que le variant atteint la taille de la liste.
Il nous suffit donc de prouver que le variant atteint toujours la taille de la liste et on aura la terminaison.
Donc, notre condition d'arrêt est d'atteindre la taille de la liste. Celle-ci est constante et par définition positive.
Notre variant commence à 0 et croit à chaque insertion.
Il atteindra donc toute valeur entière positive.
Donc en particulier la taille de la liste.
Donc notre variant atteindra bien la taille de la liste, quelle que soit la liste en entrée.
Donc notre algorithme termine toujours, quelle que soit la liste en entrée.