Semantique Axiomatique X: Les Boucles a Test Initial
La regle d’inference qui permet de trouver la pre-condition d’une boucle “while” est la suivante:
{I} while B do S end {I and (not B)}
I represente l’invariant de la boucle mais il n’est . pas fourni. C’est a nous de le trouver!
Comment? En calculant la pre-condition pour un certain nombre de repetitions et en essayant de deviner un motif.