Find the loop invariant of the given while loop I don't know how to find a loop invariant.  I'm not sure where to start.  Can anyone find the loop invariant of the given program and explain your method please.

{n ≥ 0 ∧ i = 0}
while i &lt; n − 1 loop
b[i] := a[i + 1];
i:=i + 1
end loop
{∀j.(0 ≤ j &lt; n − 1 → b[j] = a[j + 1])}
At the end of each iteration you have 
$$
\forall j: 0 \leq j &lt; i \implies b[j] = a[j+1]
$$
which you can prove by induction. Thus, when the algorithm terminates, $i$ has reached $n-1$ and you have 
$$
\forall j: 0 \leq j &lt; n-1 \implies b[j] = a[j+1]\,.
$$

I figured this out by just asking myself what kind of statement I can make at the end of each iteration. In this case it's that the first $i$ elements have been copied. Then I just turned that into a formal statement.