For a proposed loop invariant , initial condition , guard , body , and postcondition , establish these Hoare logic obligations:The first establishes before the loop; the second preserves it after each iteration; the third derives the desired result when the guard is false. Together they prove partial correctness. For total correctness, also prove algorithm termination, for example by a nonnegative integer loop variant that strictly decreases whenever the body executes. The loop invariant need not be the postcondition: it generally describes completed and unfinished work together.
Let denote the original array, used only in the proof. Save its first entry before overwriting it:The loop invariant is
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;saved = A[0], for , and for . 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 . The result is . This also handles , and uses exactly element reads and element writes, counting the saved read and final write, with one extra value of type T.Save the last entry and shift in decreasing index order, so no source is overwritten before being used:The loop invariant is
PROCEDURE RightOne;
VAR saved: T; i: INTEGER;
BEGIN
saved := a[N-1]; i := N-1;
WHILE i > 0 DO
a[i] := a[i-1]; i := i-1
END;
a[0] := saved
END RightOne;saved = A[N-1], for , and for . The decreasing loop variant is . At exit the untouched saved value fills index zero. The result is , again with reads, writes, and one extra value of type T. Applying this after part (b) restores every original entry.Normalize the amount to , with ; negative then naturally denotes a right rotation. When , return without touching the elements. Otherwise the map has disjoint permutation cycles, each of length . Use representatives :The conditional calculation of
PROCEDURE RotateLeft(k: INTEGER);
VAR r, g, x, y, h, s, j, next: INTEGER; saved: T;
BEGIN
r := k MOD N;
IF r # 0 THEN
x := N; y := r;
WHILE y # 0 DO h := x MOD y; x := y; y := h END;
g := x; s := 0;
WHILE s < g DO
saved := a[s]; j := s;
IF j >= N-r THEN next := j-(N-r) ELSE next := j+r END;
WHILE next # s DO
a[j] := a[next]; j := next;
IF j >= N-r THEN next := j-(N-r) ELSE next := j+r END
END;
a[j] := saved; s := s+1
END
END
END RotateLeft;next implements addition modulo without first forming a possibly overflowing j+r. Oberon's MOD with positive divisor supplies the nonnegative remainder. The first loop is the Euclidean algorithm, with loop invariant and decreasing nonzero remainder.For the outer loop, cycles with representatives below
s are complete and every other cycle retains its original values. In one cycle, write . The inner loop invariant is saved = A[s], , and for , with the remaining sources still untouched. When the next index returns to s, the saved value closes the cycle. The cycle length is : writing and with , the least positive with is . Each residue class modulo is one cycle, justifying the chosen representatives.Every element is read once and written once: element accesses, compared with for repetitions of part (b). The zero rotation uses none. The running time is and auxiliary space is constant; the original array is proof notation, not a copy made by the program.
Use the convention , as required by the paper's rotation example. Follow each permutation cycle once. Temporarily encode a visited value as , and restore the whole permutation before returning:Require
PROCEDURE Permute(VAR p: ARRAY OF INTEGER);
VAR s, j, next: INTEGER; saved: T;
BEGIN
s := 0;
WHILE s < N DO
IF p[s] >= 0 THEN
IF p[s] = s THEN
p[s] := -p[s]-1
ELSE
saved := a[s]; j := s;
next := p[j]; p[j] := -next-1;
WHILE next # s DO
a[j] := a[next]; j := next;
next := p[j]; p[j] := -next-1
END;
a[j] := saved
END
END;
s := s+1
END;
s := 0;
WHILE s < N DO p[s] := -p[s]-1; s := s+1 END
END Permute;LEN(p) >= N and that p[0..N) is the stipulated permutation. Its cells must be writable and distinct from the data array. The marking map is reversible and fits whenever the original valid indices and fit in the signed integer type.At each outer test, all marked indices belong to fully completed cycles; all unmarked cycles still contain their original data and permutation entries. Within a cycle the same shifting loop invariant as part (d) applies, with successor given by the original
p: all previously filled positions have their final values, and saved preserves the overwritten first source. A permutation has no path into a different cycle, so every new successor is unmarked until it returns to s; no encoded negative value is used as a source index. At outer-loop exit every index is marked and correct. The restoration loop has decoded precisely the indices below s.The procedure uses one extra value of type
T, time, and at most data reads plus data writes, with no data access for fixed points. It returns p unchanged, though it marks it temporarily. If p must remain read-only even during execution, test whether each index is its cycle's smallest member by traversing p before moving that cycle. That preserves constant space and the same optimal data accesses, but can require index-array accesses. Articles by others on the same topic
There are currently no matching articles.