logo
Terminaison d'un algorithme
Invariant de boucle

A priori, les algorithmes de tri par insertion et de tri par sélection "fonctionnent" correctement : ils trient bien le tableau donné en entrée, on dit que ces algorithmes sont corrects. On parle aussi de la "correction d'un algorithme" pour dire qu'un algorithme produit bien le résultat attendu.

Multiplier les exemples qui "fonctionnent" ne veut pas dire que l'algorithme donnera le "bon résultat" dans toutes les circonstances. C'est un peu comme en mathématiques, vérifier qu'une propriété est vraie sur un exemple n'a pas valeur de démonstration. Il se pourrait très bien que dans une situation donnée notre algorithme de donne pas le résultat attendu.

Il existe un moyen de démonter (au sens mathématique du terme) la correction d'un algorithme. Si nous arrivons à démontrer la correction de l'algorithme de tri par insertion, nous pourrons alors affirmer que, quel que soit le tableau donné en entrée, nous obtiendrons bien en sortie ce même tableau, mais trié. Pour démontrer la correction de l'algorithme de tri par insertion, nous allons utiliser un "invariant de boucle"

Qu'est-ce qu'un invariant de boucle ?

On appelle invariant de boucle une propriété qui est vraie avant et après chaque itération.

Prenons tout de suite un exemple avec le tri par insertion :

Afin de travailler sans avoir à faire des aller-retour entre les pages, voici, pour mémoire, l'algorithme de tri par insertion :

VARIABLE
t : tableau d'entiers
i : nombre entier
j : nombre entier
k : nombre entier
DEBUT
j←2
tant que j<=longueur(t):   //boucle 1
  i←j-1
  k←t[j]
  tant que i>0 et que t[i]>k:   //boucle 2
    t[i+1]←t[i]
    i←i-1
  fin tant que
  t[i+1]←k
  j←j+1
fin tant que
FIN

Divisons le tableau t en 2 parties :

Nous allons travailler sur cet exemple : t = [27, 10, 12, 8, 11]

Au départ nous avons j=2, donc t[1..j-1] = t[1..1] = [27] (le tableau t[1..j-1] contient un unique élément)

À début de la deuxième itération de la "boucle 1", nous avons t = [10, 27, 12, 8, 11] et j=3, d'où t[1..j-1] = t[1..2] = [10, 27]

À début de la troisième itération de la "boucle 1", nous avons t = [10, 12, 27, 8, 11] et j=4, d'où t[1..j-1] = t[1..3] = [10, 12, 27]

À début de la quatrième itération de la "boucle 1", nous avons t = [8, 10, 12, 27, 11] et j=5, d'où t[1..j-1] = t[1..4] = [8, 10, 12, 27]

Que peut-on dire du tableau t[1..j-1] au début de chaque itération ?

Réponse : t[1..j-1] est un tableau trié !

Notre invariant de boucle pourrait donc être : "Le tableau t[1..j-1] est trié"

Trouver ce qui pourrait être un invariant de boucle est une chose, encore faut-il ensuite démontrer qu'il est correct (une fois de plus l'étude d'un cas particulier ne vaut pas démonstration). La démonstration doit se faire en 3 étapes :

Revenons au tri par insertion et à notre invariant de boucle "Le tableau t[1..j-1] est trié" :

Cette démonstration nous permet d'affirmer que l'algorithme de tri par insertion est correct.

À faire vous-même 1

Trouvez un invariant de boucle pour l'algorithme de tri par sélection. Procédez ensuite à la démonstration en 3 étapes afin de démontrer la correction de l'algorithme de tri par sélection.

Remarques diverses :

Dans un algorithme non récursif, le seul cas possible de non terminaison provient de while ou repeat. Dans le cas d’une boucle Pour i de a à b, un variant simple est b − i. Toute boucle for se finit.



Ressources :

  1. terminaison-de-boucle.
  2. terminaison.
  3. terminaison.