Array list: insert at position

Algorithmic problem: Ordered sequence: insert at position

Prerequisites: Parameters: A key [math]\displaystyle{ \Kappa \in K }[/math], a position [math]\displaystyle{ I \in \{0, \ldots, number()\} }[/math].

Type of algorithm: loop

Auxiliary data:

1. A natural number sum [math]\displaystyle{ \in \mathbb{N}_0 }[/math], which contains the total number of all elements seen so far in the visited arrays.
2. Two pointers, [math]\displaystyle{ p }[/math] and [math]\displaystyle{ p' }[/math], of type "pointer tolist item of type array of component type [math]\displaystyle{ \Kappa }[/math]".

Abstract view

Invariant:After [math]\displaystyle{ i \ge 0 }[/math] iterations:

1. The pointer [math]\displaystyle{ p }[/math] points to the array at position [math]\displaystyle{ i+1 }[/math] in the array list.
2. It is [math]\displaystyle{ sum = n_1 + \ldots + n_i }[/math], where [math]\displaystyle{ n_j }[/math] is the value of the component n of the array list item at position [math]\displaystyle{ j \in \{1, \ldots,i\} }[/math].

Varian: The pointer [math]\displaystyle{ p }[/math] is moved one step forward to the next array.

Break condition: It is sum [math]\displaystyle{ + p.n \ge l }[/math].

Induction basis

Abstract view: Set [math]\displaystyle{ p:= }[/math]first and [math]\displaystyle{ sum:=0 }[/math].

Implementation: Obvious.

Proof: Nothing to show.

Induction step

Abstract view: If the position [math]\displaystyle{ l }[/math] is in the current array, insert [math]\displaystyle{ \Kappa }[/math] (if the array is full, split it first).

Implementation:

1. If sum[math]\displaystyle{ + p.n \lt l }[/math]:
   1. Set sum[math]\displaystyle{ := }[/math]sum[math]\displaystyle{ + p.n }[/math].
   2. Set [math]\displaystyle{ p:=p.next }[/math].
2. Otherwise:
   1. If [math]\displaystyle{ p.n=N }[/math]:
      1. Create a new array list item and let [math]\displaystyle{ p' }[/math] point to this new list item.
      2. Set [math]\displaystyle{ p'.next=p.next }[/math].
      3. Set [math]\displaystyle{ p.next:=p' }[/math].
      4. For [math]\displaystyle{ j \in \{1, \ldots, \lfloor p.n/2 \rfloor \} }[/math], set [math]\displaystyle{ p'.A[\lceil p.n/2 \rceil + j] }[/math] and [math]\displaystyle{ p.A[\lceil p.n/2 \rceil + j]:= }[/math]void.
      5. Set [math]\displaystyle{ p'.n:=\lfloor p.n/2 \rfloor }[/math] and, afterwards, [math]\displaystyle{ p.n:=p.n - \lfloor p.n/2 \rfloor }[/math].
   2. If [math]\displaystyle{ l - sum \gt p.n }[/math]:
      1. Set [math]\displaystyle{ m:=l - sum - p.n + 1 }[/math].
      2. Set [math]\displaystyle{ p:=p' }[/math].
   3. Otherwise, set [math]\displaystyle{ m:=l - sum + 1 }[/math].
   4. For [math]\displaystyle{ j=p.n, \ldots, m }[/math] (in this order), set [math]\displaystyle{ p.A[j+1]:=p.A[j] }[/math].

Correctness: Note that, in an implementation of Ordered sequence: insert at position, we may assume [math]\displaystyle{ l \leq }[/math]number(). Therefore, we do not have to care about the end of the list. In the case sum[math]\displaystyle{ + p.n \lt l }[/math], we simply have to update sum and [math]\displaystyle{ p }[/math], which is obviously done correctly. So consider the case sum[math]\displaystyle{ + p.n \ge l }[/math], which means that the position where [math]\displaystyle{ \Kappa }[/math] has to be inserted is in the array list item to which [math]\displaystyle{ p }[/math] currently points. If that array is full, new space must be allocated. Step 2.1 does that and distributes the elements roughly equally over both items. Steps 2.2 - 2.3 ensure that [math]\displaystyle{ p }[/math] points to the array where to insert [math]\displaystyle{ \Kappa }[/math] and [math]\displaystyle{ m }[/math] identifies the correct insert position. Step 2.4 empties the array component where to insert the new element by moving, exactly one position forward, the value at the position and the values at all later position (which is possible because the array is not full in any case).

Complexity

Statement: Linear in the length of the sequence in the worst case.

Proof: Obvious.