Version imprimable
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?
En fonction de ce que tu veux démontrer !Citation:
Envoyé par molo1987
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