= Solution
Let $A$ denote the original <array>, used only in the proof. Save its first entry before overwriting it:
``
PROCEDURE LeftOne;
VAR saved: T; i: INTEGER;
BEGIN
saved := a[0]; i := 0;
WHILE i < N-1 DO
a[i] := a[i+1]; i := i+1
END;
a[N-1] := saved
END LeftOne;
``
The <loop invariant> is `saved = A[0]`, $a[j]=A[j+1]$ for $0\leq j<i$, and $a[j]=A[j]$ for $i\leq 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$. \b[The result is $a[j]=A[(j+1)\bmod 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`.
Back to article page
