Trova il ciclo invariante del singolo loop mentre

Question

Non so come trovare un loop invariante. Non sono sicuro da dove cominciare. Chiunque può trovare l'invariante del loop del programma dato e spiegare il tuo metodo per favore.

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