# Proof of correctness of binary search

I have just written a pseudo-code (actually in Python) of a binary search algorithm.

def binSearch(lst, number):
left = 0
right = len(lst) - 1
while left <= right:
middle = left + ((right - left) / 2)
if number == lst[middle]:
return True
else:
if number < lst[middle]:
right = middle - 1
else:
left = middle + 1
return False


It seems intuitively correct, but I'd like to use some stronger tool to be absolutely sure that my algorithm is correct.

I've read on Wikipedia, that I have to prove two things: Convergence (the algorithm will stop) and partial correctness (the algorithm will end with the right result). This is the proof of total correctness.

Could you demonstrate the proof of my binSearch in theoretical computer science speech?

thank you

-

You need to prove the only thing that the algorithm returns the index of $number$ if $number \in lst$, or $false$ if $number \notin lst$.

The proof is based on induction $n=right - left +1$. The main thing is to show that on every step the algorithm preserves the invariant.

The base case if, $n=1$, the algorithm clearly returns the correct answer.

In the general case, it doesn't matter on which side the $number$ is, the main thing is that the algorithms does the next iteration on a stricly smaller subarray.

if $number < lst[middle]$, then if it occurs in $lst$ at all, it must occur at a position prior to middle. Hence, the invariant is preserved if we recur on $lst[left..(middle − 1)]$.

If $number \geq lst[middle]$, then if it occurs in $lst$ at all, it must occur at position mid or later. Hence, the invariant is preserved if we recur on $lst[middle..rigth]$

For further information about correctness and complexity of binary search Binary Search Algorithm

-
Thank you. the algorithm preserves the invariant means right - left + 1 doesn't change? I think that n is changing in every cycle. I understand the induction for n = 1 but I'm not sure if it proofs correctness. I will look at your pdf. – xralf Mar 6 '12 at 14:47
The pdf helped me a lot in understanding. – xralf Mar 6 '12 at 14:53

First you need to define what the algorithm is supposed to do. It looks like you are given a sorted list and looking for whether number is in it. To prove convergence, just observe that right-left always decreases and is bounded below by 0. To prove correctness you argue that lst[left]<=number<=lst[right]. Note that it will fail if lst is not sorted.

Which Python are you using? I think in version 3 the divide is a true divide so your calculation of middle could return 10.5-you need an int operation.

-
Yes, the algorithm do exactly what you said and the list is sorted. The convergence proof is acceptable for me (though maybe it could be written with some reasoning more in detail, e.g. with induction. I see it but don't know how to write it mathematically), but don't know if correctness looks like a proof. – xralf Mar 6 '12 at 14:22
I'm using Python 2.7, the division is integer division. – xralf Mar 6 '12 at 14:23