Correction du tri par insertion

On cherche à prouver la correction du tri par insertion.

On supputera que l'insertion est correcte. Pour les élèves les plus rapides, on pourra prouver cette correction

Question

Quels invariant(s) devez-vous considérer ?

Indice

Contrairement au tri par sélection, on a besoin ici, d'un seul invariant.

Solution

FondamentalInvariant du tri par insertion

L'invariant pour le tri par insertion est : la partie dite triée est triée.

Question

Prouvez la validité de l'invariant au début de l'algorithme.

Indice

On va faire un preuve par le vide

Solution

MéthodeAvant la première insertion

Avant la première insertion, la partie dite triée est vide.

Donc elle est forcément triée.

Question

Prouvez la constance de l'invariant à chaque tour de boucle.

Indice

On utilisera l’hypothése que l'insertion, insert le nouvel élément au bon endroit, si et seulement si la partie dite triée est triée.

Solution

Invariant par insertion

Nous supposons donc qu'avant l'insertion, la partie dite triée est triée.

Or on suppose que l'insertion, insert au bon endroit si la partie dite triée est triée.

Donc la nouvelle partie dite triée est triée.

Question

Déduisez la validité de l'invariant.

Solution

Récurrence

Entre deux insertions, on ne fait rien, donc la partie dite triée reste triée, si elle l'était déjà.

Donc en utilisant un raisonnement par récurrence, la partie dite triée est toujours triée.

Question

Prouvez la correction du tri par insertion.

Solution

Correction du tri par insertion

Les invariants sont toujours vrais, avant et après une insertion.

Avec la preuve de terminaison, après la dernière insertion, 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 insertion est correct.

Correction de l'insertion (pour les plus rapides)

On cherche maintenant à prouver la correction de l'insertion.

Question

Quels invariant(s) devez-vous considérer ?

Question

Prouvez la validité du/des invariants au début de l'algorithme.

Question

Prouvez la constance du/des invariants à chaque tour de boucle.

Question

Déduisez la validité du/des invariants.

Question

Prouvez la correction de l'insertion.