# 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. Mar 20, 2018 at 9:43
• The invariant expresses that the array copy has been partially performed.
– user16034
Mar 20, 2018 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) ;-) Mar 20, 2018 at 11:40