Binary search tree: remove node: Difference between revisions
Line 20: | Line 20: | ||
'''Invariant:''' | '''Invariant:''' | ||
# The [[Directed Tree#Immediate Predecessor and Successor|immediate predecessor]] of '''''K''''' is in the [[Directed Tree#Ranges of Search Tree Nodes|range]] of <math>p'</math>. | # The [[Directed Tree#Immediate Predecessor and Successor|immediate predecessor]] of '''''K''''' is in the [[Directed Tree#Ranges of Search Tree Nodes|range]] of <math>p'</math>. | ||
# It is <math>p'</math>.right | # It is <math>p'</math>.right <math>\neq</math> void. | ||
'''Variant:''' The pointer <math>p'</math> descends one level deeper, namely to <math>p</math>'.right. | '''Variant:''' The pointer <math>p'</math> descends one level deeper, namely to <math>p</math>'.right. |
Revision as of 08:08, 26 June 2015
General Information
Algorithmic problem: See the remark clause of Binary Search Tree; pointer [math]\displaystyle{ p }[/math] as defined there is the input.
Prerequisites: [math]\displaystyle{ p }[/math].left [math]\displaystyle{ \neq }[/math] void.
Type of algorithm: loop
Auxiliary data: A pointer [math]\displaystyle{ p' }[/math] of type "pointer to a binary search tree node of type [math]\displaystyle{ \mathcal{K} }[/math]."
Abstract View
Invariant:
- The immediate predecessor of K is in the range of [math]\displaystyle{ p' }[/math].
- It is [math]\displaystyle{ p' }[/math].right [math]\displaystyle{ \neq }[/math] void.
Variant: The pointer [math]\displaystyle{ p' }[/math] descends one level deeper, namely to [math]\displaystyle{ p }[/math]'.right.
Break condition: It is [math]\displaystyle{ p' }[/math].right.right = void.
Induction Basis
Abstract view: If [math]\displaystyle{ p.left }[/math] is the immediate predecessor of K, overwrite K by its immediate predecessor and terminate; otherwise, initialize [math]\displaystyle{ p' }[/math].
Implementation:
- If [math]\displaystyle{ p }[/math].left.right = void:
- Set [math]\displaystyle{ p }[/math].key := p.left.key.
- Set [math]\displaystyle{ p }[/math].left := p.left.left.
- Terminate the algorithm.
- Otherwise, set [math]\displaystyle{ p' }[/math] := p.left.
Proof: Obvious.
Induction Step
Abstract view: If [math]\displaystyle{ p' }[/math].right is the immediate predecessor of [math]\displaystyle{ K }[/math], overwrite [math]\displaystyle{ K }[/math] by its immediate predecessor and terminate; otherwise, let [math]\displaystyle{ p }[/math] descend one level deeper.
Implementation:
- If [math]\displaystyle{ p' }[/math].right.right = void:
- Set [math]\displaystyle{ p }[/math].key := [math]\displaystyle{ p' }[/math].right.key.
- Set [math]\displaystyle{ p' }[/math].right := [math]\displaystyle{ p' }[/math].right.left.
- Terminate the algorithm.
Correctness: Obvious.
Complexity
Statement: The complexity is in [math]\displaystyle{ \mathcal{O}(T\cdot h)\subseteq\mathcal{O}(T\cdot n) }[/math] in the worst case, where [math]\displaystyle{ n }[/math] is the length of the sequence, [math]\displaystyle{ h }[/math] the height of the tree, and [math]\displaystyle{ T }[/math] the complexity of the comparison.
Proof: Obvious.