Binary search
Binary search
Algorithmic problem: Finding an element in a sorted array
Type of algorithm: recursion
Abstract view
The subroutine does nothing but calling another, recursive subroutine with the same output and the following input: array [math]\displaystyle{ A }[/math], comparison [math]\displaystyle{ cmp }[/math], element [math]\displaystyle{ s }[/math] and, in addition, two indices of [math]\displaystyle{ A }[/math], [math]\displaystyle{ \ell }[/math] and [math]\displaystyle{ r }[/math], such that [math]\displaystyle{ \ell\lt r }[/math]. In the original call to this recursive subroutine, [math]\displaystyle{ \ell }[/math] is the first and [math]\displaystyle{ r }[/math] the last index of [math]\displaystyle{ A }[/math].
Invariant: For every recursive call: If [math]\displaystyle{ s }[/math] is present at least once in [math]\displaystyle{ A }[/math], then all indices of [math]\displaystyle{ A }[/math] where [math]\displaystyle{ s }[/math] is present are in the interval [math]\displaystyle{ [\ell,\ldots,r] }[/math].
Variant: The value [math]\displaystyle{ r-\ell }[/math] is roughly halved in every descent in the recursion tree.
Break condition: Either an occurrence of [math]\displaystyle{ s }[/math] is found or it is [math]\displaystyle{ \ell\gt r }[/math]
Induction basis
The invariant is trivially fulfilled because [math]\displaystyle{ [\ell,\ldots,r] }[/math] is the entire index range of [math]\displaystyle{ A }[/math].
Induction step
Abstract view:
If p points to a node but not with key K, p descends in the appropriate direction, left or right.
Implementation:
- If [math]\displaystyle{ p.key = K }[/math], terminate the algorithm and return true.
- Otherwise:
- If [math]\displaystyle{ K \lt p.key }[/math], set [math]\displaystyle{ p }[/math] to the sequence element [math]\displaystyle{ k_{i+1}=k_i-n/2^i }[/math].
- If [math]\displaystyle{ K \gt p.key }[/math], set [math]\displaystyle{ p }[/math]to the sequence element [math]\displaystyle{ k_{i+1}=k_i-n/2^i }[/math].
Correctnes: Obvious.
Complexity
Statement: Log(n)
Proff: Obvious.