Terminaison

Nous examinons ici le problème posé par la question ``notre boucle termine-t-elle pour n'importe quelle valeur des entrées considérées''? Nous traitons toujours l'exemple du calcul de la somme 1 + 2 + ...+ n, pour un entier n positif. Selon la forme de la boucle employée, la preuve de la terminaison sera différente.

Cas simple: boucle for

Si le calcul est fait par une boucle for, la terminaison est immédiate. En effet, une boucle for est exécutée un nombre de fois qui ne change pas dynamiquement une fois la boucle commencée. Par exemple, étudions la terminaison de la boucle for_1 (partie 6.3) qui calcule la somme de notre exemple avec une boucle for.

-- Rappel de la boucle for_1
for i in 1..n loop
   somme := somme + i;
end loop;

Si n est positif, cette boucle exécute l'action somme := somme + i exactement n fois. Puisque n est forcément un nombre fini, il est évident que la boucle termine. Si n est négatif ou zéro, le corps de la boucle n'est jamais exécuté, donc, dans ce cas là, elle termine aussi.

Conclusion: for_1 termine pour n'importe quelle valeur de n.

Terminaison d'une boucle loop:

Pour qu'une boucle loop termine, elle doit possèder au moins une instruction exit avec une condition de sortie qui devient vraie après un nombre fini d'itérations. Examinons la terminaison de la boucle:

-- Boucle loop_2
  i, somme : integer := 0;
begin
  loop
     i := i + 1;
     somme := somme + i;
     exit when i = n;
  end loop;
end;

Nous convaincre que loop_2 termine est facile au vu des hypothèses initiales et du comportément des instructions dans son corps:

1.

n est un nombre strictement positif: n > 0 (hypothèse du problème),

2.

i vaut 0 avant de commencer la boucle (par initialisation), donc, avant la première itération, la propriété i < n est vrai,

3.

à chaque tour de boucle, la valeur de i est incrémentée de 1.

Pour montrer la terminaison de loop_2:

Puisque i < n, le fait d'incrémenter i de 1 fait que chaque itération ``rapproche'' la valeur de i de celle de n. De plus, n étant un nombre de la machine, il est forcément fini. Ainsi, il est facile de voir qu'inévitablement i sera un jour égal à n, et donc la condition de sortie i = n deviendra vrai au bout d'un nombre fini d'itérations. Le tableau suivant montre les tests qui sont éffectués lors des premières itérations:

Boucle loop_2	0	1	2	3	4	...	n-1	Arrêt
i	0	1	2	3	4	...	n-1	n
somme	0	1	3	6	10	...	1+2+ ...+n-1	1+2+ ...+n-1 + n
i = n	-	1 = n	2 = n	3 = n	4 = n	...	n-1 = n	n = n

Conclusion: loop_2 termine pour n'importe quel n, tel que n > 0.

Terminaison dans tous les cas?

Cette petite boucle mérite une dernière considération. Nous avons supposé n > 0 en tant qu'hypothèse du problème. Supposons un moment que ce ne soit pas le cas. Qu'en est-il de la terminaison de loop_2? Si n <= 0, elle ne termine jamais. En effet, alors que les valeurs de i déviennent succéssivement 1,2,3, ..., la valeur de n reste constante et inférieure ou égale à zéro. Il n'y a donc, aucun espoir que la condition i = n soit jamais vrai.

La question que l'on peut se poser est: pouvons nous être sûrs de l'hypothèse n > 0 avant le début de la loop_2? La réponse est bien entendu négative. Pour garantir la terminaison, nous sommes forcés, soit de nous assurer que n est positif avant l'entreée en boucle, (et dans le cas contraire, interdire son exécution!), soit de faire en sorte qu'elle s'arrête même si n <= 0.

La boucle loop_3 présentée plus bas termine pour n'mporte quelle valeur de n, et ceci tout en réalisant le bon calcul dans le cas où l'hypothèse n > 0 est vérifiée. Elle est est identique à loop_2, sauf pour la condition de sortie qui change de i = n dans loop_2, à i >= n ici:

-- Boucle loop_3
  i, somme : integer := 0;
begin
  loop
     i := i + 1;
     somme := somme + i;
     exit when i >= n;
  end loop;
end;

Terminaison de loop_3:

Il y a deux cas:

• si n > 0, loop_3 se comporte comme loop_2, et donc, elle termine.

• sinon, alors n <= 0, et c'est la partie i > n de la condition qui permet de terminer l'exécution. En effet, si n <= 0, le corps de loop_3 s'exécute une première fois et alors i prend la valeur 1. A la fin de cet itération, la condition de sortie i >= n devient vraie car i = 1 et n <= 0, et donc la boucle termine.

Boucle loop_3	0	1
i	0	1
somme	0	1
i >= n	-	1 >= n	Arrêt ( n <= 0)

Conclusion: loop_3 termine pour n'importe quelle valeur de n.

En résumé, pour se convaincre de la terminaison d'une boucle loop, on peut se poser les questions suivantes:

• possède-t-elle au moins une instruction exit?
• les actions de la boucle font qu'au bout d'un nombre fini d'itérations au moins l'une des conditions de sortie devient vraie?
• ou plus précisement: ces actions permettent qu'à chaque itération au moins l'une des conditions de sortie ``se rapproche de la vérité'' ?
• avons nous vérifié qu'elle termine pour tous les cas des variables qui apparaissent dans les tests de sortie?

Terminaison d'une boucle while:

Pour qu'une boucle while termine, on doit montrer qu'au bout d'un nombre fini d'étapes, la condition d'entrée à la boucle devient fausse. Examinons la terminaison de la boucle:

-- Boucle while_2
   i, somme : integer := 0; 
begin
   while i < n loop
       i:= i + 1;
       somme := somme + i;
   end loop;
end;

Terminaison de while_2:

Il y a deux cas:

• Si n <= 0, et puisque i = 0 par initialisation, alors la condition d'entrée i < n est d'emblée fausse, et le corps de la boucle ne s'éxécute jamais. Donc, elle termine.
• Si n > 0, par un raissonnement similaire à celui employé pour loop_2 (partie 6.1), après chaque itération la valeur de i se rapproche de la valeur de n, et donc, après un nombre fini d'itérations, la condition i < n devient fausse et la boucle termine.
  

Boucle while_2	0	1	2	3	4	...	n	Arrêt
i < n	-	0 < n	1 < n	2 < n	3 < n	...	n-1 < n	not(n < n)
i	0	1	2	3	4	...	n	-
somme	0	1	3	6	10	...	1+2+ ...+n	-

Conclusion: while_2 termine pour n'importe quelle valeur de n.

En résumé, pour raissonner sur la terminaison d'une boucle while on peut se poser les questions suivantes:

• les actions de la boucle font qu'au bout d'un nombre fini d'itérations la condition d'entrée de la boucle devient fausse?
• ou plus particulièrement: ces actions font qu'à chaque itération la condition d'entrée de la boucle ``se rapproche de la valeur faux'' ?