Un exercice

if
   a < b -> a := a+1;
   []
   a > 0 -> a := a-1;
fi

do
   a < b -> a := a+1;
   []
   a > 0 -> a := a-1;
od

après DO		avant		après IF
a	b	a	b	a	b
boucle infinie		5	10	6,4	10
0	-10	5	-10	4	-10
boucle infinie		-5	10	-4	10
-5	-10	-5	-10	échec