Come ottenere invarianti a loop per dimostrare il programma è corretto nella logica di hoare

Question

Inizia affermando la definizione di un loop invariante. È una condizione che deve essere vera all'inizio del ciclo e deve essere vera dopo ogni iterazione del ciclo. Capisco di cosa si tratta, ma ho difficoltà a provare a trovarne uno.

Qui sotto c'è un programma che so è corretto e ho dichiarato l'invariante loop. Qualcuno potrebbe passare attraverso spiegare semplicemente perché questo è l'invariante loop. Lo guardo da un po 'adesso, ma non riesco a capire perché l'invariante in loop sia quello che è. Sono molto nuovo nella logica di Hoare.

{N >=0}//Pre condition

x = 1;

i = 0;

{x == A^i}//Invariant

while (i != N)

{x == A^i || i != N}//Invariant and Guard

x = x * A;

i = i + 1;

{x == A^i} //invariant

{x == A^i    ||    i==N}// Invariant and !Guard

{x == A^N}//Post condition