Iterative binary search

Those who have taken an algorithms course should have realized that, in the above case, we proved the correctness of the recursive implementation of binary search. Another implementation, using iterations, is used more often in practice. How can we prove correctness of such an implementation?

SEARCH($D,W$)

1. $\ell \leftarrow 1, r\leftarrow n$.
2. While $\ell < r$
   1. $m \leftarrow \lceil (\ell+r)/2 \rceil$
   2. Let $W'$ be the first word on the $m$-th page.
   3. If $W$ should come before $W'$, then $r \leftarrow m-1$; otherwise, $\ell \leftarrow m$.
3. Search for $W$ in the $\ell$-th page of $D$ line-by-line.

Lemma 2 (Loop invariant)

If $W$ is in $D$, then it appears in one of the pages $[\ell, r]$.

This kind of statement is called loop invariant. It holds at the beginning of the loop, and if we can prove that it holds at the end of the loop, the correctness of the program would follow.

Proof:

Notice that the statement holds before the program enters the loop. We argue that if it holds before executing the instructions in the loop, then it holds after the execution. To see this, we can consider two cases: (a) If $W$ should come before $W'$, then it means that $W$ cannot be in page $m$ or after, so updating $r \leftarrow m-1$ would maintain the validity of the statement. (b) Otherwise, we know that $W$ cannot appear in $[1,m-1]$, so we can update $\ell \leftarrow m$, maintaining the validity of the statement.