Semantique Axiomatique XI: Les Boucles a Test Initial

• Mais trouver l’invariant de boucle n’est pas tout!!!

• Etant donne l’instruction {P} while B do S end {Q}, et l’invariant de boucle, I , voici un resume de toutes les choses qui doivent etre demontrees afin de prouver l’exactitude d’une boucle “while”:

P => I

{I} B {I}

{I and B} S {I}

(I and (not B)) => Q

La boucle se termine.

Previous slide

Back to first slide

View graphic version