Lycée > Premiere > NSI > Utiliser les invariants pour corriger un algorithme

Utiliser les invariants pour corriger un algorithme

Fiche de cours
Quiz
Profs en ligne
Videos
Application mobile

Objectifs

Comprendre la nécessité de corriger un algorithme.
Savoir démontrer qu’un algorithme est correct.

Points clés

Coder et tester un algorithme ne prouve pas qu’il est correct.
Trouver, puis utiliser un ou des invariants de boucle d’un algorithme (propositions qui doivent être vraies à chaque itération de l’algorithme) permet de prouver qu’il est correct.

Pour bien comprendre

Utiliser des boucles (for et while).
Utiliser une instruction conditionnelle.
Écrire un algorithme.

1. La méthode

a. Généralités

En informatique, il est d’usage de déterminer une suite finie d’instructions pour résoudre un problème. On détermine ainsi un algorithme de résolution du problème.

En pratique, il est courant de coder cet algorithme dans un langage de programmation et de le tester pour vérifier qu’il fonctionne.

Tester un code qui implémente (traduit) un algorithme ne prouve toutefois pas qu’il est correct, qu’il fait ce que l’on attend de lui. Des exemples, même en grand nombre, ne constituent pas une démonstration.

C’est pourquoi il est nécessaire d’avoir une méthodologie pour démontrer qu’un algorithme est correct.

b. Les invariants de boucle

Pour démontrer qu’un algorithme est correct, on utilise les invariants de boucle.

Un invariant de boucle est une propriété qui, si elle est vraie avant l’exécution d’une itération d’une boucle, le demeure après son exécution.

En pratique, il faut démontrer que les propriétés choisies sont bien des invariants de boucle.

Pour chaque invariant, il y a quatre étapes, qui sont données ci-dessous.

Initialisation : on montre que la propriété est vraie au début de la boucle.
Hypothèse : on suppose que la propriété est vraie à la i-ème itération.
Hérédité : à partir de l’hypothèse, on montre que la propriété est vraie à la (i+1)-ième itération.
Conclusion : on montre qu’en sortie de boucle, le résultat obtenu est celui attendu.

Remarque
Ce type de démonstration ressemble aux démonstrations par récurrence rencontrées en mathématiques.

2. Exemples d'utilisation des invariants de boucle

a. Algorithme de recherche du minimum d'un tableau de nombre

Voici ci-dessous un algorithme de recherche du minimum dans un tableau Tab de nombres de taille n.

mini ← Tab[0]	Tab[0] est affecté à la variable mini.
Pour i allant de 0 à n−1	i = 0, puis i = 1, puis i = 2, puis… i = n−1
Si Tab[i] < mini, alors	Si Tab[i] est inférieur à mini, alors
mini ← Tab[i]	on affecte Tab[i] à la variable mini.
FinSi	Fin de l’instruction « Si ».
FinPour	Fin de l’instruction « Pour ».

Exemple – Rechercher le minimum dans Tab=[2, 3, 1]

mini = Tab[0] = 2
Pour i = 0, Tab[0] = mini (0 = 0). mini ne change pas.
Pour i = 1, Tab[1] > mini (3 > 2). mini ne change pas.
Pour i = 2, Tab[2] < mini (1 < 2). mini = Tab[2] = 1.

Le parcours est fini. Le minimum est donc 1.

Pour démontrer que cet algorithme est correct, on a trouvé l’invariant de boucle suivant :

P(i) : « Après la i-ème itération de la boucle Pour, mini référence le minimum de Tab[0], Tab[1], …, Tab[i]. »

Démonstration de la correction

Initialisation : P(0) est vraie car mini référence Tab[0] avant la boucle.
Hypothèse : Supposons P(i) vraie (pour 0 < i < n−1).
Montrons que P(i+1) est vraie.
Si P(i) est vraie, alors mini référence le minimum de Tab[0], Tab[1], …, Tab[i].
À la (i+1)-ième itération, on compare Tab[i+1] et mini.
- Si Tab[i+1] < mini, alors mini référence Tab[i+1].
  Ainsi mini référence le minimum de Tab[0], Tab[1], …, Tab[i], Tab[i+1]. Donc P(i+1) est vraie.
- Si Tab[i+1] > mini, alors Tab[i+1] est plus grand que le minimum de Tab[0], Tab[1], …, Tab[i]. C’est pourquoi, là encore, mini référence le minimum de Tab[0], Tab[1], …, Tab[i], Tab[i+1]. Donc P(i+1) est vraie.
Finalement, P(i) est vraie pour i entre 0 et n−1. Comme P(n−1) est vraie, alors mini référence le minimum de Tab[0], Tab[1], …, Tab[n−1]. C’est pourquoi mini référence le minimum de Tab.
L’algorithme fait bien ce que l’on veut.

b. Algorithme de détermination du quotient et du reste de la division euclidienne de deux entiers

Effectuer la division euclidienne de a par b (entiers naturels) consiste à déterminer les uniques entiers naturels q et r vérifiant : a = b × q + r avec r < b.

Voici ci-dessous un algorithme de détermination du quotient et du reste de a par b (des entiers naturels vérifiant a > b).

r ← a	a est affecté à la variable r
q ← 0	0 est affecté à la variable q
Tant que r >= b,	Tant que r est supérieur ou égal à b,
q ← q+1	on incrémente q de 1
r ← r−b	et on décrémente r de b.
FinTantque	Fin de la boucle « Tant que ».
Retourner q et r	On retourne q et r.

Exemple – Réaliser le quotient q et le reste r de 25 par 7
a = 25 et b = 7
r = 25 et q = 0

Pour q = 0, r = 25
25 > 7
Pour q = 1, r = 25 − 7 = 18
18 > 7
Pour q = 2, r = 18 − 7 = 11
11 > 7
Pour q = 3, r = 11 − 7 = 4
4 < 7
On stoppe la boucle : q = 3 et r = 4.

On a bien 25 = 3 × 7 + 4.

Pour démontrer que cet algorithme est correct, on a trouvé l’invariant de boucle suivant :

P(i) : « Après la i-ème itération de la boucle Tant que, on a l’égalité a = bq + r. »

Démonstration de la correction

Initialisation : P(0) est vraie car initialement on a q = 0 et r = a ; on a bien bq + r = b × 0 + a = a.
Hypothèse : Supposons P(i) vraie.

Montrons que P(i+1) est vraie.
Si P(i) est vraie, alors, après la i-ème itération de la boucle Tant que, on a l’égalité a = bq + r.
À la (i+1)-ième itération, on compare r et b.

Si r < b (reste < diviseur), alors on sort de la boucle Tant que.
Les variables q et r sont inchangées. On a toujours a = bq + r.

Si r >= b (reste ≥ diviseur), alors on incrémente q de 1 et on décrémente r de b.
Dans ce cas, on a ainsi :

i-ème itération	(i+1)-ième itération
q	q+1
r	r−b
a = b × q + r	b × (q+1) + (r − b) = b × q + b × 1 + r − b = b × q + b + r − b = b × q + r = a

Ainsi l’égalité a = bq + r est vraie après la (i+1)-ième itération.

Donc P(i+1) est vraie dans tous les cas.

Finalement, en sortie de boucle Tant que, on a r < b et a = bq + r. q et r référencent bien le quotient et le reste de la division euclidienne de a par b.