Vérifiez si les invariants de boucle sont corrects?

Question

J'essaie de prouver qu'un code est correct, en utilisant Hoare Logic. Comment puis-je vérifier si mes invariants de boucle sont corrects?

On me demande de prouver (en utilisant Hoare Logic) que le programme suivant est valide:

x=1; 
i=N;
while (i!=0){ 
    i--;
    x*=A;
}

avec la précondition N>=0 et après la condition x=A^N.

C'est ma tentative:

{ N>=0 }
x=1; 
i=N;
{i >= 0}
while (i!=0){
    {i>=0}
    {x = product(i in (0:N-i); A)}    (loop invariant)
    i--;
    x*=A;
}
{x = A^N}

Les supports bouclés représentent des invariants qui sont censés tenir à ce moment-là du code. Les 2 invariants de la boucle semblent tenir pour chaque instance de la boucle.

Ma tentative est-elle correcte? Mes invariants de boucle sont-ils suffisants? Ai-je trop?

Je sais que {i>=0} est donné par la définition de la boucle. Dois-je supprimer cette boucle invariant alors, car c'est le cas par défaut?

Edit: ma nouvelle tentative

{N>=0}
x=1;
{x = A^(N-N)=A^0=1} 
i=N;
{x = A^(N-i)}
while (i!=0){
    {i>=0} 
    i--;
    {x = product(i in (0:N-i-1);A)} 
    x*=A;
    {x = product(i in (0:N-i);A)}
}
{x=A^N}