Array list: remove
Algorithmic problem: Linear sequence: remove
Prerequisites:
Type of algorithm: loop
Auxiliary data: A pointer [math]\displaystyle{ p }[/math] of type "pointer to array list item of type [math]\displaystyle{ \mathcal{K} }[/math]".
Abstract view
Invariant: After [math]\displaystyle{ i \ge 0 }[/math] iterations:
- The pointer [math]\displaystyle{ p }[/math] points to the array list item at position [math]\displaystyle{ i+1 }[/math] (or is void if no such item exists).
- None of the arrays at positions [math]\displaystyle{ 1,...,i+1 }[/math] contains [math]\displaystyle{ K }[/math].
Variant: The pointer [math]\displaystyle{ p }[/math] is moved one step forward to the next array list item.
Break condition: Either it is [math]\displaystyle{ p }[/math].next[math]\displaystyle{ = }[/math]void or, otherwise, it is [math]\displaystyle{ K=p }[/math].next.A[math]\displaystyle{ j }[/math] for some [math]\displaystyle{ j \in {1,...,p }[/math].next.n [math]\displaystyle{ } }[/math].
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:
- If first[math]\displaystyle{ = }[/math]void, terminate the algorithm and return [math]\displaystyle{ false }[/math].
- Otherwise, if [math]\displaystyle{ K \in { }[/math]first.A [math]\displaystyle{ [1],..., }[/math]first.A[first.n] [math]\displaystyle{ } }[/math]:
- If first.n[math]\displaystyle{ n=1 }[/math], set first[math]\displaystyle{ = }[/math]first.next.
- Otherwise:
- Let [math]\displaystyle{ j \in{1,..., }[/math]first.n [math]\displaystyle{ } }[/math] such that first.A[math]\displaystyle{ [j]=K }[/math].
- For [math]\displaystyle{ h=j,..., }[/math]first.n[math]\displaystyle{ -1 }[/math] (in this order): Set first.A [math]\displaystyle{ [h]:= }[/math]first.A[math]\displaystyle{ [h+1] }[/math].
- Set first.A[math]\displaystyle{ [ }[/math]first.n[math]\displaystyle{ ]:= }[/math]void.
- Set first.n:=first.n[math]\displaystyle{ -1 }[/math].
- Terminate the algorithm and return [math]\displaystyle{ true }[/math].
- Otherwise (that is, [math]\displaystyle{ first /ne void }[/math] and [math]\displaystyle{ K \notin{ }[/math]first.A [math]\displaystyle{ [1],...,first.a[first.n]} }[/math]), set [math]\displaystyle{ p:= }[/math]first.
Proof: If [math]\displaystyle{ p }[/math].first[math]\displaystyle{ = }[/math]void or [math]\displaystyle{ K \notin{ }[/math]first.A[math]\displaystyle{ [1],..., }[/math]first.A[first.n][math]\displaystyle{ } }[/math], correctness is obvious. So consider the case that [math]\displaystyle{ first \ne void }[/math] and [math]\displaystyle{ K \in {first.A[1],...,first.A[first.n] }[/math]. If first.n[math]\displaystyle{ =1 }[/math], the array would be empty after removing [math]\displaystyle{ K }[/math], so the first list item is decoupled from the list in Step 2.1. Otherwise, [math]\displaystyle{ K }[/math] is removed and the array is rearranged accordingly in Steps 2.2.2-2.2.4.
Induction step
Abstract view: If has reached the end of the array list, the algorithm terminates. Otherwise, if the key to be removed is in the current 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: If .nextvoid, terminate the algorithm and return . Otherwise, if .next.A.next.A[.next.n]: If .next.n, set .next.next.next. Otherwise: Let .next.n such that .next.A. For .next.n (in this order): Set .next.A.next.A. Set .next.A.next.nvoid. Set .next.n.next.n. Terminate the algorithm and return . Otherwise (that is, .nextvoid and .next.A.next.A[p.next.n]), set .next. Correctness: If .nextvoid or .next.A.next.A[first.n], correctness is obvious. So consider the case that .nextvoid and .next.A.next.A[.next.n]. If .next.n, the array would be empty after removing , so this list item is decoupled from the list in Step 2.1. Otherwise, it is removed and the array is rearranged accordingly in Steps 2.2.2-2.2.4.
Complexity
Statement: Linear in the length of the sequence in the worst case. Proof: Obvious.
Further information