Array list: remove

Algorithmic problem: Ordered sequence: remove

Prerequisites:

Type of algorithm: loop

Auxiliary data: A pointer $p$ of type "pointer to array list item of type $\mathcal{K}$".

Abstract view

Invariant: After $i\ge 0$ iterations:

1. The pointer $p$ points to the array list item at position $i+1$ (or is void if no such item exists).
2. None of the arrays at positions $1,...,i+1$ contains $K$.

Variant: The pointer $p$ is moved one step forward to the next array list item.

Break condition: Either it is $p$.next$=$void or, otherwise, it is $K=p$.next.A$[j]$ for some $j\in \{1,...,p$.next.n $\}$.

Induction basis

Abstract view: If the list is empty, the algorithm terminates. Otherwise, if the key to be removed is in the first array, it is removed and the algorithm terminates again (if this was the only element of the array, that array list item is removed as well).

Implementation:

1. If first$=$void, terminate the algorithm and return false.
2. Otherwise, if $K\in \{$first.A $[1],...,$first.A[first.n] $\}$:
   1. If first.n$=1$, set first$=$first.next.
   2. Otherwise:
      1. Let $j\in \{1,...,$first.n $\}$ such that first.A$[j]=K$.
      2. For $h=j,...,$first.n$-1$ (in this order): Set first.A $[h]:=$first.A$[h+1]$.
      3. Set first.A$[$first.n$]:=$void.
      4. Set first.n:=first.n$-1$.
   3. Terminate the algorithm and return true.
3. Otherwise (that is, first$\ne$void and $K\notin \{$first.A $[1],...,$first.A[first.n]$\}$), set $p:=$first.

Proof: If $p$.first$=$void or $K\notin \{$first.A$[1],...,$first.A[first.n]$\}$, correctness is obvious. So consider the case that first$\ne$void and $K\in \{$first.A[1],...,first.A[first.n]$\}$. If first.n$=1$, the array would be empty after removing $K$, so Step 2.1 is right to decouple the first list item from the list. Otherwise (that is, first.n$>1$), $K$ is removed and the array is rearranged accordingly in Steps 2.2.2-2.2.4.

Induction step

Abstract view: If $p$ has reached the tail of the array list, the algorithm terminates. Otherwise, if the key to be removed is in the array of the very next array list item, it is removed and the algorithm terminates again (if this was the only element of the array, that array list item is removed as well).

Implementation:

1. If $p$.next$=$void, terminate the algorithm and return false.
2. Otherwise, if $K\in \{p$.next.A[$1$],...,$p$.A.next.A[$p$.next.n]$\}$:
   1. If $p$.next.n$=1$, set $p$.next$:=$.next.next.
   2. Otherwise:
      1. Let $j\in \{1,...,p$.next.n$\}$ such that $p$.next.A.$[j]=K$.
      2. For $h=j,..,p$.next.n$-1$ (in this order): Set $p$.next.A$[h]:=p$.next.A$[h+1]$.
      3. Set $p$.next.A$[p$.next.n$]:=$void.
      4. Set $p$.next.n$:=p$.next.n $-1$.
   3. Terminate the algorithm and return true.
3. Otherwise (that is, $p$.next$\ne$void and $K\notin \{p$.next.A$[1],...,$.next.A[p.next.n]$\}$), set $p:=p$.next.

Correctness: If $p$.next$=$void or $K\notin \{p$.next.A$[1],...,p$.next.A[first.n]$\}$, correctness is obvious. So consider the case that $p$.next$=$void and $K\in \{p$.next.A$[1],...,p$.next.A[$p$.next.n]$\}$. If $p$.next.n$=1$, the array would be empty after removing $K$, so Step 2.1 is right to decouple this list item from the list. Otherwise, $K$ is overwritten and the array is rearranged accordingly in Step 2.2.

Complexity

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

Proof: Obvious.