Comment obtenir des invariants de boucle pour prouver le programme est correct dans la logique Hoare

Question

Commencez par indiquer la définition d'une boucle invariante. C'est une condition qui doit être vraie au début de la boucle et doit être vraie après chaque itération de la boucle. Je comprends ce que c'est, mais j'ai du mal à en trouver un.

Voici un programme que je sais correct et j'ai déclaré l'invariant de la boucle. Quelqu'un pourrait-il s'il vous plaît expliquer simplement pourquoi c'est la boucle invariante. Je le regarde depuis un certain temps maintenant, mais je ne vois pas pourquoi l'invariant de la boucle est ce qu'il est. Je suis très nouveau dans Hoare Logic.

{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