Boucle while

Le cas particulier où le test de sortie se trouve en début de boucle est si courant, qu'il existe en Ada une syntaxe particulière qui lui est consacrée. La syntaxe suit le schéma:

while condition_entree loop

sequence_instructions

end loop

Sémantique: ``tant que condition_entree est vraie, exécuter sequence_instructions''. On teste condition_entree avant de commencer chaque nouvelle itération. Si elle est vraie, on exécute la sequence_instructions, puis le contrôle du programme passe à nouveau au point de test de condition_entree en début de boucle. Si condition_entree est fausse, le contrôle du programme passe à l'instruction juste après le end loop.

Considérons la boucle loop_1 de la la partie précédente (6.1). Elle est très facilement transformable en boucle while: en effet, dans loop_1, le test de sortie se trouve en début de boucle, et dans une boucle while la suite à donner à l'exécution est décidée également au début des itérations. Cependant, une différence importante démeure: alors que dans une boucle loop on termine lorsque la condition de sortie est vérifiée, dans une boucle while l'arrêt intervient quand la condition d'entrée à la boucle devient fausse.

Ainsi, pour traduire la boucle loop_1 vers une boucle while_1, on reprend les actions de loop_1 telles qu'elles, mais l'on pose en tant que condition d'entrée à while₂, la négation de la condition de sortie de loop_1:

-- Rappel de la boucle loop_1
 loop     
    exit when i = n;
    i := i + 1;
    somme := somme + i;
 end loop;

-- Boucle while_1
while i /= n loop
   i:= i + 1;
   somme := somme + i;
end loop;

On peut signaler une dernière différence entre les boucles loop et while. Le corps d'une boucle loop est toujours exécutée au moins une fois (quoique éventuellement de manière partielle, si la sortie se fait avant la fin), alors que le corps d'une boucle while peut ne jamais être exécuté: cela arrive si la condition d'entrée à la boucle n'est jamais vraie. Par exemple, si n = 0, et sachant que i = 0 par l'initialisation, le corps de while_1 n'est jamais exécuté.

Propriétés à la sortie d'un while

Une boucle while possède une unique condition d'arrêt: la condition d'entrée à la boucle doit devenir fausse. Que peut-on conclure quant aux propriétés à la sortie d'une boucle while quelconque?

while C loop
    I;
end loop;

Juste après le end loop, la propriété

not(C)

est vraie. En effet, après le end loop on se trouvera dans deux cas: soit la boucle ne s'est jamais exécutée car la condition C était au départ fausse; soit elle s'est exécuté un certain nombre de fois jusqu'à ce que C devienne fausse. Dans les deux cas not(C) est vérifié.