Correction du tri par sélection
On cherche ici à prouver que notre algorithme de tri par sélection trie bien la liste en entrée.
Fondamental : Invariants du tri par sélection
Pour le tri par sélection, il y a 2 invariants :
La partie dite triée est en effet triée
Tous les éléments de la partie triée sont inférieurs ou égaux à ceux de la partie non triée
Les points clefs où l'on vérifie ces invariants sont avant et après chaque sélection.
Remarque :
On remarque ici que nos deux invariants ne sont pas des conditions de boucle mais bien des conditions que nous avons placées en sus.
Preuve de la correction du tri par sélection
Méthode : Avant la première sélection
On va commencer par vérifier qu'avant la première sélection, les invariants sont vrais.
Avant la première sélection, la partie dite triée est vide.
Donc :
Elle est triée, l'ensemble vide est toujours trié ;
Tous ses éléments (il n'y en a aucun) sont inférieurs ou égaux à ceux de la partie non triée.
Méthode : Invariant par sélection
Montrons que si les invariants sont vrais avant une sélection, alors ils le sont toujours après.
Nous supposons donc qu'avant la sélection nous avons :
La partie dite triée est triée ;
Tous les éléments de la partie triée sont inférieurs ou égaux à ceux de la partie non triée.
Lors de la sélection, on choisi le plus petit élément de la partie non triée et on l'ajoute à la fin de la partie triée.
Cet élément faisait parti de la partie non-triée, donc il est supérieur ou égal à tous les éléments de la partie triée.
Donc l'ajouter à la fin de la partie triée garde le fait que cette nouvelle partie triée, de un plus grande, est toujours triée.
Cet élément est le plus petit des éléments de la partie non triée, donc est inférieur ou égal à tout les éléments restants de la partie non triée.
Or les éléments de la partie triée étaient déjà inférieurs ou égaux à ceux de la nouvelle partie non triée.
Donc les éléments de la nouvelle partie triée sont toujours inférieurs ou égaux à ceux de la partie non triée.
Donc si les invariants étaient vrais avant la sélection, ils le sont toujours après.
Méthode : Invariant d'une sélection à l'autre
Prouvons que si les invariants sont vrais à la fin d'une sélection, ils sont toujours vrai avant la suivante (si suivante il y a).
Entre 2 sélection, on ne fait rien, donc les invariants ne risquent pas de changer.
Donc ils sont toujours valide.
Méthode : Invariance des invariants
Au début du programme, les invariants sont vrais
Ils restent vrai par sélection
Donc les invariants sont toujours vrais.
Remarque : Raisonnement par récurrence
On appelle raisonnement par récurrence, ce type de raisonnement. Où :
on vérifie au début qu'une propriété est vraie,
puis qu'elle le reste à chaque étape.
Vous les verrez plus en détails en terminale en NSI, mais aussi en mathématiques.
Méthode : Correction du tri par sélection
Les invariants sont toujours vrais, avant et après une sélection.
Avec la preuve de terminaison, après la dernière sélection, la partie triée est de la même taille que la liste.
Or la partie triée est triée.
Donc la liste est triée.
Donc l'algorithme du tri par sélection est correct.