Terminaison du tri par sélection
On cherche ici à prouver que notre algorithme de tri par séléction termine quelque soit la liste en entrée.
Fondamental : Variant du tri par sélection
Le variant qui nous intéresse dans le cas du tri par sélection est la taille de la partie triée.
Remarque : Un variant mais pas une variable
On remarque ici que le variant n'est pas une variable mais plutôt la taille d'une valeur abstraite.
On pourrait la rendre concrète en ayant une variable qui représente cette taille.
Méthode : Preuve de la terminaison du tri par sélection
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 sélection, 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 sélection.
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.