Binary search tree: remove node

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:

1. The immediate predecessor of K is in the range of [math]\displaystyle{ p' }[/math].
2. 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].

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:

1. If [math]\displaystyle{ p.left.right = void }[/math]:
   1. Set [math]\displaystyle{ p.key := p.left.key }[/math]
   2. Set [math]\displaystyle{ p.left := p.left.left }[/math].
   3. Terminate the algorithm.
2. Otherwise, set [math]\displaystyle{ p' := p.left }[/math].

Proof: Obvious.

Induction Step

Abstract view: If [math]\displaystyle{ p'.right }[/math] is the immediate predecessor of K, overwrite K by its immediate predecessor and terminate; otherwise, let p' descend one level deeper.

Implementation:

1. If [math]\displaystyle{ p'.right.right = void }[/math]:
   1. Set [math]\displaystyle{ p.key := p'.right.key }[/math].
   2. Set [math]\displaystyle{ p'.right := p'.right.left }[/math].
2. Terminate the algorithm.

Correctness: Obvoius.