Knuth says “Although the basic idea of binary search is comparatively straightforward, the details can be surprisingly tricky…” Numerous incorrect versions have appeared in print, even if we forgive integer overflow, which has bitten many implementations. Hopefully I didn't make any mistakes here.

The BinarySearch method finds an occurence of the specified key in the array, and returns its index. If the array does not contain the key, the negative value -(i+1) is returned, where i is the insertion index for the key. The keys must be sorted in monotonically increasing order. They need not be distinct.

An iteration of the loop either finds the key, or reduces the length

right - left + 1

of the subarray being searched by at least half. Termination of the while loop is guaranteed in at most lg(n)+1 iterations, where lg(n) is the binary logarithm of the array length.

If the array contains the key, the while loop satisfies the invariant

left <= right

and can terminate only by finding the key. If the array does not contain the key, the while loop exits with

left == right + 1.

For convenience, define keys[-1] and keys[keys.Length] to be negative and positive infinity, respectively. With this abuse of notation,

keys[left - 1] < key < keys[right + 1]

is an invariant of the loop. It follows that

keys[left - 1] < key < keys[left]

when the loop terminates without finding the key. In other words, left is the key's natural insertion index.

For simplicity, the BinarySearch method above is nongeneric. A more flexible implementation would use a method parameter T as the array element type, and constrain it to implement IComparable<T>.

Interval bisection is the analogue of binary search for finding zeros of continuous functions. Newton's Method is a slightly more elaborate algorithm that's much faster in some cases, but is unreliable even for solving polynomials. It's probably not of interest to many programmers, yet I can't resist mentioning Curt McMullen's striking work involving iteration of rational functions, as with Newton's Method, to find roots of polynomials. A brief description of his results can be found in an interview. I clearly remember sitting in a mathematics colloquium long ago, in which Steve Smale hypothesized results of the type found later by McMullen. At the time, I didn't understand why he had gone off on this tangent (pun intended), but now I know!