Discussion :

[molo1987]

Bonsoir tlm,

je suis depuis 8 heure sur un petit probleme en ce qui concerne la logique de Hoare.mon question tout d'abord comment trouver l'invariant d'une boucle.
J'ai deja un exemple :

a = 0;
b = 1;
c = 0;
while (c != n) {
a = a + b;
c = c + 1;
b = b + 6 * c;
}


il faut prouver que {n > 0} P {a = n puissance 3}

J'ai trouvé que l invariant => a = c puissance 3 mais comme meme j'ai quelques doutes.

une idée svp?

[Franck Dernoncourt]

comment trouver la invariant d'une boucle.

En fonction de ce que tu veux démontrer !
Si tu veux prouver que {n > 0} P {a = n^3}, effectivement la seule façon de le faire est de prouver que a = c^3 est un invariant de la boucle.

J'avais justement traduit en français et édité un peu l'article sur la logique de Hoare de Wikipedia, regarde la règle de l'itération : http://fr.wikipedia.org/wiki/Logique...it.C3.A9ration