Semantique Axiomatique IX: Les Boucles a Test Initial
Dans une boucle a test initial (ou une boucle “while”), on a une repetition d’instruction. Le probleme avec ces boucles, cependant, est qu’on ne sait pas combien de repetitions il y a => il est assez difficile de determiner l’exactitude de ces boucles.
La methode utilisee est similaire a la methode mathematique d’induction.
L’hypothese inductive s’appelle l’invariant de la boucle (loop invariant)