Keep For insertion, conceptually treat index
u[0..len) sorted, with the coupling invariantThe abstract list retains insertion order, while the concrete array retains its sorted multiset. Initially both are empty.PROCEDURE Add(x: INTEGER);
VAR i: INTEGER;
BEGIN
ASSERT(len < N);
i := len;
WHILE i > 0 DO
IF u[i-1] <= x THEN EXIT END;
u[i] := u[i-1];
i := i-1
END;
u[i] := x;
len := len+1
END Add;
PROCEDURE Get(k: INTEGER): INTEGER;
BEGIN
ASSERT((0 <= k) & (k < len));
RETURN u[k]
END Get;i as a hole. If is the old sorted prefix of length , the loop invariant is , and , with every shifted value strictly greater than . The loop variant is . The exit condition gives either no left neighbour or a left neighbour at most ; filling the hole establishes sortedness and adds exactly one occurrence, preserving the coupling invariant.When the new entry is smaller than every old entry, all old values must move in this contiguous sorted-prefix representation. Binary search can reduce comparisons to locate the insertion point, but cannot remove that linear movement cost. Appending a new largest value takes constant time in this implementation. Articles by others on the same topic
There are currently no matching articles.