Past exam of the year 1 of the computer science course of the University of Oxford / 2016 / Imperative programming (resit) / 4 / b

Let $A$ denote the original array, used only in the proof. Save its first entry before overwriting it:The loop invariant is saved = A[0], $a[j]=A[j+1]$ for $0\le j<i$, and $a[j]=A[j]$ for $i\le j<N$. Thus the next source is untouched, and the assignment extends the completed prefix. At exit, the saved entry supplies the last position. The loop variant is $N-1-i$. The result is $a[j]=A[(j+1)\mathrm{mod}N]$. This also handles $N=1$, and uses exactly $N$ element reads and $N$ element writes, counting the saved read and final write, with one extra value of type T.