Trouvez la boucle invariante de la boucle donnée

Question

Je ne sais pas comment trouver une boucle invariante. Je ne sais pas par où commencer. Quelqu'un peut-il trouver la boucle invariante du programme donné et expliquer votre méthode s'il vous plaît.

{n ≥ 0 ∧ i = 0}
while i < n − 1 loop
b[i] := a[i + 1];
i:=i + 1
end loop
{∀j.(0 ≤ j < n − 1 → b[j] = a[j + 1])}