Array list: remove: Difference between revisions
Line 35: | Line 35: | ||
'''Proof:''' If <math>p</math>.first<math>=</math>void or <math>K \notin\{</math>first.A<math>[1],...,</math>first.A[first.n]<math>\}</math>, correctness is obvious. So consider the case that first<math>\neq</math>void and <math>K \in \{</math>first.A[1],...,first.A[first.n]<math>\}</math>. | '''Proof:''' If <math>p</math>.first<math>=</math>void or <math>K \notin\{</math>first.A<math>[1],...,</math>first.A[first.n]<math>\}</math>, correctness is obvious. So consider the case that first<math>\neq</math>void and <math>K \in \{</math>first.A[1],...,first.A[first.n]<math>\}</math>. | ||
If first.n<math>=1</math>, the array would be empty after removing <math>K</math>, so Step 2.1 is right to decouple the first list item from the list. Otherwise, <math>K</math> is removed and the array is rearranged accordingly in Steps 2.2.2-2.2.4. | If first.n<math>=1</math>, the array would be empty after removing <math>K</math>, so Step 2.1 is right to decouple the first list item from the list. Otherwise (that is, first.n<math>>1</math>), <math>K</math> is removed and the array is rearranged accordingly in Steps 2.2.2-2.2.4. | ||
==Induction step== | ==Induction step== |
Revision as of 08:29, 17 May 2015
Algorithmic problem: Ordered 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 false.
- 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{ =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 true.
- Otherwise (that is, first[math]\displaystyle{ \neq }[/math]void and [math]\displaystyle{ K \notin\{ }[/math]first.A [math]\displaystyle{ [1],..., }[/math]first.A[first.n][math]\displaystyle{ \} }[/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 first[math]\displaystyle{ \neq }[/math]void and [math]\displaystyle{ K \in \{ }[/math]first.A[1],...,first.A[first.n][math]\displaystyle{ \} }[/math]. If first.n[math]\displaystyle{ =1 }[/math], the array would be empty after removing [math]\displaystyle{ K }[/math], so Step 2.1 is right to decouple the first list item from the list. Otherwise (that is, first.n[math]\displaystyle{ \gt 1 }[/math]), [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 [math]\displaystyle{ p }[/math] 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 [math]\displaystyle{ p }[/math].next[math]\displaystyle{ = }[/math]void, terminate the algorithm and return .
- Otherwise, if [math]\displaystyle{ K \in \{p }[/math].next[math]\displaystyle{ ,...,p }[/math].A.next.A[[math]\displaystyle{ p }[/math].next.n][math]\displaystyle{ \} }[/math]:
- If [math]\displaystyle{ p }[/math].next.n[math]\displaystyle{ =1 }[/math], set .[math]\displaystyle{ p }[/math]next[math]\displaystyle{ p:= }[/math].next.next.
- Otherwise:
- Let [math]\displaystyle{ j \in \{1,...,p }[/math].next.n[math]\displaystyle{ \} }[/math] such that [math]\displaystyle{ p }[/math].next.A.[math]\displaystyle{ [j]=K }[/math].
- For [math]\displaystyle{ h=j,..,p }[/math].next.n[math]\displaystyle{ -1 }[/math] (in this order): Set [math]\displaystyle{ p }[/math].next.A[math]\displaystyle{ [h]:=p }[/math].next.A[math]\displaystyle{ [h+1] }[/math].
- Set [math]\displaystyle{ p }[/math].next.A[math]\displaystyle{ [p }[/math].next.n[math]\displaystyle{ ]:= }[/math]void.
- Set [math]\displaystyle{ p }[/math].next.n[math]\displaystyle{ :=p }[/math].next.n[math]\displaystyle{ -1 }[/math].
- Terminate the algorithm and return [math]\displaystyle{ true }[/math].
- Otherwise (that is, [math]\displaystyle{ p }[/math].next[math]\displaystyle{ \ne }[/math]void and [math]\displaystyle{ K\notin\{p }[/math].next.A[math]\displaystyle{ [1],..., }[/math].next.A[p.next.n][math]\displaystyle{ \} }[/math]), set [math]\displaystyle{ p:=p }[/math].next.
Correctness: If [math]\displaystyle{ p }[/math].next[math]\displaystyle{ = }[/math]void or [math]\displaystyle{ K\notin\{p }[/math].next.A[math]\displaystyle{ [1],...,p }[/math].next.A[first.n][math]\displaystyle{ \} }[/math], correctness is obvious. So consider the case that [math]\displaystyle{ p }[/math].next[math]\displaystyle{ = }[/math]void and [math]\displaystyle{ K\in\{p }[/math].next.A[math]\displaystyle{ [1],...,p }[/math].next.A[[math]\displaystyle{ p }[/math]next.n][math]\displaystyle{ \} }[/math]. If [math]\displaystyle{ p }[/math].next.n[math]\displaystyle{ =1 }[/math], the array would be empty after removing [math]\displaystyle{ K }[/math], 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.