Controlla se gli invarianti del loop sono corretti?

Question

Sto cercando di dimostrare che un codice è corretto, usando la logica Hoare. Come posso controllare se i miei invarianti ad anello sono corretti?

Mi viene chiesto di dimostrare (usando la logica Hoare) che il seguente programma è valido:

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

con la pre-condizione che N>=0 e post-condizione x=A^N.

Questo è il mio tentativo:

{ 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}

Le parentesi ricci rappresentano gli invarianti che dovrebbero trattenere a quel punto nel codice. I 2 invarianti ad anello sembrano reggere per ogni istanza del ciclo.

Il mio tentativo è corretto? I miei invarianti ad anello sono sufficienti? Ne ho troppi?

So che {i>=0} è dato dalla definizione del ciclo. Dovrei rimuovere quel loop invariante allora, poiché è il caso per impostazione predefinita?

EDIT: il mio nuovo tentativo

{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}