= Solution
Exchange symmetric pairs, stopping before the middle:
``
PROCEDURE reverse(i, n: INTEGER);
VAR t: INTEGER;
BEGIN
t := 0;
WHILE t < n DIV 2 DO
swap(i+t, i+n-1-t);
t := t + 1
END
END reverse;
``
Writing $m_0$ for the pre-call <array>, the <loop invariant> says that the first and last `t` positions of the segment already satisfy $m[i+s]=m_0[i+n-1-s]$, all positions between them retain their original values, and positions outside the segment are unchanged. Each <swap> fixes the next symmetric pair. The <loop variant> $\lfloor n/2\rfloor-t$ decreases; the two indices are distinct and in bounds whenever the body executes. \b[Exactly $\lfloor n/2\rfloor$ swaps reverse the segment], with the odd-length middle element left in place and no accesses for $n\leq1$.
Back to article page
