Binary search tree: remove node: Difference between revisions
Jump to navigation
Jump to search
| Line 11: | Line 11: | ||
== Abstract View == | == Abstract View == | ||
'''Invariant:''' | |||
# The [[Directed tree|immediate predecessor]] of '''''K''''' is in the [[Directed tree|range]] of <math>p'</math>. | |||
# It is <math>p'.right = void</math>. | |||
'''Variant:''' The pointer <math>p'</math> descends one level deeper to <math>p'.right</math>. | |||
'''Break condition:''' It is <math>p'.right.right = void</math>. | |||
== Induction Basis == | == Induction Basis == | ||
Revision as of 21:27, 25 September 2014
General Information
Algorithmic problem: See the remark clause of Binary Search Tree; pointer p as defined there is the input.
Prerequisites: [math]\displaystyle{ p.left \neq void }[/math]
Type of algorithm: loop
Auxiliary data: A pointer [math]\displaystyle{ p' }[/math] of type "pointer to a binary search tree node".
Abstract View
Invariant:
- The immediate predecessor of K is in the range of [math]\displaystyle{ p' }[/math].
- It is [math]\displaystyle{ p'.right = void }[/math].
Variant: The pointer [math]\displaystyle{ p' }[/math] descends one level deeper to [math]\displaystyle{ p'.right }[/math].
Break condition: It is [math]\displaystyle{ p'.right.right = void }[/math].