Find the loop invariant of the given while loop
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.