Proving things about algorithms

📄️ Recursive binary search

We consider the abstraction of binary search. Given a dictionary, our goal is to find word $W$ in the dictionary. This abstraction can be implemented by the following pseudocode.

📄️ 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?

📄️ Loop invariants

More generally, to argue about the behavior of our loop, consider the following while loop: