Adéquation à la spécification

Pour vérifier qu'un programme fait bien ce que nous attendons de lui, il faut d'abord possèder une spécification précise et complète de ce qu'il est censé faire. Une telle spécification existe rarement, même pour les programmes simples! Prenons toujours l'exemple initial. Son spécification au moins, est précise et complète.

Spécification S: Calculer dans une variable somme la somme des n premiers entiers naturels 1+2+ ...+ n, où n > 0.

Dans cette partie nous examinons l'adéquation de plusieurs boucles vis-à-vis de cette spécification. Regardons par exemple, si la boucle while_2 étudiée dans la partie 6.2, satisfait la spécification S:

-- Rappel de la boucle while_2
   i, somme : integer := 0; 
begin
   while i < n loop
       i:= i + 1;
       somme := somme + i;
   end loop;
end;

Nous avons déjà montré que while_2 termine toujours (c.a.d., pour toutes les valeurs possibles de n). Maintenant, il nous reste à montrer qu'à l'arrêt, la variable somme contient bien la valeur de 1+2+ ...+n. Pour ce faire, on peut se demander quel est l'état des variables à la sortie de while_2.

Dans un premier temps, on peut répondre à cette question pour quelques valeurs de n. Par exemple, si n=1, alors on constante que while_2 calcule somme = 1; si n = 2, elle calcule somme = 3; si n = 4, alors somme = 10. De cette manière, on a testé while_2 avec les valeurs 1,2,3 pour n. On sait donc dire quelle est la valeur de somme pour ces quelques tests. Il en va autrement de sa valeur pour n'importe quel n positif.

Que sait-on de manière générale à la fin de la boucle? On sait que la condition not(i < n) est vrai. Cependant, ceci ne suffit pas à caractériser l'état final du programme, ce qui est normal parce qu'il faut bien se préoccuper de ce que fait le corps de la boucle. Or, toute la dificulté est de comprendre ce que les itérations ont calculé ici. Pour y arriver nous chercherons à trouver ce que l'on appele l'invariant de la boucle.

L'invariant est une propriété qui est vraie juste avant l'entrée de la boucle et à la fin de chaque étape d'itération. Par conséquent, elle est aussi vraie juste après la fin de la boucle. Pour être utile, l'invariant doit être suffisament général pour compléter notre caractérisation de l'état final du programme, et en particulier, pour nous aider à conclure, si oui ou non, la variable somme contient 1+2+ ...+ n.

Dans notre cas, l'invariant est une formule générale qui décrit le contenu de la variable somme au bout de k étapes. Il aura la forme
${\tt somme}_k = F(k)$
qu'on peut lire: ``au bout de k étapes, la variable somme contient la valeur donnée par F(k)''. Puisque cette formule doit être vraie en particulier avant le début de la boucle (itération 0), k est un nombre entier tel que k >=0.

A quoi servira cette formule? Supposons que nous l'avons trouvé, et que, de plus, nous avons montré qu'elle est effectivement vérifiée lors de chaque itération. Si par la suite, on sait déterminer le nombre m de fois où la boucle est repété, il s'en suit que la valeur finale de somme est ${\tt somme}_m$, et donc, ${\tt somme} = {\tt somme}_m = F(m)$. Si de plus, F(m) = 1+2+ ...+ n, alors nous aurons montré que while_2 calcule bien ce qui est spécifié par S.

Avant de chercher l'invariant nous donnons, en guise de guide pratique, un resumé des pas à suivre pour montrer l'adéquation de notre boucle à la spécification S. Tous les invariants ne sont pas de même nature, cependant, ce guide pourra servir comment modèle pour d'autres boucles à étudier.

1.

On commence par tester la boucle sûr quelques valeurs bien choisies de n. Nous l'avons déjà fait pour n = 1,2,3,4.

2.

On ``déroule'' l'exécution de la boucle à l'aide d'un tableau qui décrit l'état des variables pour chaque itération. Plus particulièrement, on cherche une formulation générale de l'état de somme pour un nombre k arbitraire d'itérations. Cette formule sera notre ``candidate d'invariant''.

3.

On tente de montrer, aussi formellement que possible, que cette formule est bien un invariant pour la boucle (c.a.d., qu'elle est vérifiée à chaque étape).

4.

Pour un n > 0, on détermine le nombre m des fois où la boucle est repétée.

5.

On substitue m dans l'invariant et l'on vérifie si ${\tt somme}_m$ = 1 + 2 + ...+n.

Chercher l'invariant

La meilleure manière de trouver un invariant de boucle est de regarder de près ce qu'elle fait. Nous examinons l'état des variables au bout d'un nombre k arbitraire d'itérations. Nous supposons n > 0 (autrement, le corps de la boucle n'est pas exécuté).

Boucle while_2	0	1	2	...	k	...	n	Arrêt
i < n	-	0 < n	1 < n	...	k-1 < n	...	n-1 < n	not(n < n)
i	0	1	2	...	k	...	n	-
somme	0	0+1	0+1+2	...	1+2+...+ k	...	1+2+ ...+n	-

Ce tableau nous dit qu'à l'étape k, la variable somme contient 0+1+2+ ...+k, ou exprimé autrement

${\tt somme}_k = 0 + 1 + 2 + \ldots + k$.

Cette formule est notre candidate pour être la propriété invariante de la boucle.

Montrer qu'il s'agit d'un invariant

En quoi la formule précédente est-elle ``invariante''pour while_2? Voyons cela:

1.

Elle est vérifiée juste avant le début de la boucle. En effet, k=0 est l'étape juste avant toute itération, et à ce moment là, somme = 0 (par initialisation). Donc, on a bien ${\tt somme}_0 = 0+ \ldots + 0 = 0$.

2.

Elle est vérifiée à la fin de chaque étape. Cet argument est plus délicat. On devrait exhiber une preuve construite par récurrence (sur le nombre d'étapes déjà réalisées). En réalité, en examinant le tableau, il n'est pas difficile de se convaincre qu'à la fin de l'étape k, somme contient bien 0+1+2+ ...+k. Essayons d'énoncer un argument informel:

(a)

A la fin de la première itération k = 1, on a somme = 1. Donc ${\tt somme}_1 = 0 + 1$ est vérifié.

(b)

En fin d'itération k = 2, on a somme = 1 + 2, et donc ${\tt somme}_2 = 1 + 2$ est vérifié.

(c)

Que se passe-t-il lors d'une étape k arbitraire? L'affectation somme := somme + i de l'étape k peut être lue par:
``la valeur de somme à l'étape k est égale à la valeur prise par somme lors de l'étape précédente (k-1) plus la valeur de i''.

On peut donc re-écrire le calcul réalisé par somme := somme + i à l'étape k par:

${\tt somme}_k$ = ${\tt somme}_{(k-1)}$ + i.

Mais, à chaque itération, le compteur d'étapes k et i ont la même valeur (i = k). Notre formule devient:

${\tt somme}_k$ = ${\tt somme}_{(k-1)}$ + k.

Supposons maitenant que la somme calculée jusqu'à l'étape (k-1) est correcte. Cela signifie que, ${\tt somme}_{(k-1)}$ = 0 + 1 + ... + (k-1) est vérifiée. Notre formule devient:

${\tt somme}_k$ = 0 + 1 + ...+ (k-1) + k.

Donc, lors de l'étape k, somme contient bien 0+1+2+ ...+k. Ceci qui montre que lors d'une étape k arbitraire, la formule ${\tt somme}_k = 0 + 1 + 2 + \ldots + k$ est vérifiée.

Montrer l'adéquation

Avec ce raisonnement, nous avons montré que la formule ${\tt somme}_k = 0+1+ \ldots +k$ est un invariant de la boucle while_2. Pour montrer que while_2 calcule effectivement 1+2+ ...+n, il nous reste à trouver le nombre d'étapes éffectué. Il y a deux cas:

1.

Si n <= 0 le corps de la boucle n'est jamais exécuté et la valeur obtenue pour somme est celle de son initialisation (somme = 0). La spécification S nous impose une valeur à calculer seulement dans le cas où n > 0. Ainsi, nous pouvons donner à somme n'importe quelle valeur dans tous les autres cas, pourvu que le programme termine.

2.

Si n > 0, le corps de la boucle est exécuté au moins une fois. On sait que i = n pour chaque étape. Puisque i débute à 0, et qu'il est incrémenté de 1 à chaque étape, il est facile de voir que la dernière étape exécutée est celle où i = k = n. En effet, à l'étape suivante, le test i < n devient faux et la boucle s'arrête. Donc, la boucle est repétée n fois. Il s'ensuit que la valeur finale dans somme est ${\tt somme}_n = 1 + 2 + \ldots +n$.

Conclusion On vient de montrer que la boucle while_2 satisfait la spécification S. Dans la partie précédente nous avons montré que while_2 termine pour n'importe quelle valeur de n. On a donc achevé de montrer que la boucle while_2 est correcte.