B-tree: find
General Information
Algorithmic problem: Sorted sequence: find
Type of algorithm: loop
Auxiliary data: A pointer p of type "pointer to a B-tree node".
Abstract View
Invariant: Before and after each iteration:
- p points to some node N of the B-tree and
- the searched key is in the range of N.
Variant: p is redirected from the current node N to some child of the current node.
Break condition:
- p points to a leaf of the B-tree or (that is, inclusive-or)
- the searched key is in the node to which p points.
Induction Basis
Abstract view: p is initialized so as to point to the root of the B-tree.
Implementation: Obvious.
Proof: Obvious.