Il existe un problème récurrent en informatique : le tri de données. Comme vu précédemment, on travaille souvent sur de grands nombres de valeurs, et il faut bien trier tout ça à un moment pour plusieurs raisons :
# décaler les éléments T[0]..T[i-1] qui sont plus grands que x, en partant de T[i-1]
j ← i
tant que j > 0 et T[j - 1] > x
T[j] ← T[j - 1]
j ← j - 1
# placer x dans le "trou" laissé par le décalage
T[j] ← x
```
Le tri par insertion est *naturel* dans l'esprit : on parcourt le tableau de la gauche vers la droite et pour chaque élément, on le classe dans la partie du tableau situé sur sa gauche.
### Preuve de correction
| Valeur de i | Tableau avant la boucle | Valeur de la clé | Tableau en fin de boucle |
> À la fin de chaque boucle, le tableau est trié de la case n°0 à la case n°i
Une preuve de correction de l'algorithme est la propriété *p(i)* : "le tableau est trié jusqu'à la case n°i" : cette propriété est vraie **avant** et **après** chaque tour de boucle : c'est ce qu'on appelle ***Invariant de boucle***
À l'inverse, le **variant** de boucle est une expression dans la valeur varie à chaque tour de boucle et qui doit justement permettre de mettre fin à la-dite boucle : le variant d'un algorithme de tri sera alors la taille de la liste restante à trier.
Dans le pire des cas (éléments classés par ordre décroissant), la boucle while effectue 2n opérations : chaque tour de boucle for compte pour 2n + 3, répérées n - 1 fois. On a donc (n - 1) (2n + 3).
<arel="license"href="http://creativecommons.org/licenses/by-nc-sa/4.0/"><imgalt="Licence Creative Commons"style="border-width:0"src="https://i.creativecommons.org/l/by-nc-sa/4.0/88x31.png"/></a><br/>Ce cours est mis à disposition selon les termes de la <arel="license"href="http://creativecommons.org/licenses/by-nc-sa/4.0/">Licence Creative Commons Attribution - Pas d’Utilisation Commerciale - Partage dans les Mêmes Conditions 4.0 International</a>