# 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 < n − 1 loop
b[i] := a[i + 1];
i:=i + 1
end loop
{∀j.(0 ≤ j < n − 1 → b[j] = a[j + 1])}

• What did you try? Where did you get stuck? If you don't know where to start, that usually means you need to go back and review your lecture notes. – David Richerby Mar 20 '18 at 9:43
• The invariant expresses that the array copy has been partially performed. – Yves Daoust Mar 20 '18 at 10:57

At the end of each iteration you have $$\forall j: 0 \leq j < 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 < 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.
• In general if you are trying to end up with post-condition R(n) then at the end of each iteration you may have R(i) ;-) – Musa Al-hassy Mar 20 '18 at 11:40