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?