How to know if incorrect binary search algorithm always terminates without testing

Question

Consider the following algorithm where target = 13 and array = [5,10,15,20,25] where N = length of array

lo = 1
hi = N
while lo < hi:
    mid = (lo+hi)//2
    if target >= array[mid]:
        lo = mid
    else:
        hi = mid
if array[lo] == target:
    return lo
return False

I know that the above algorithm doesn't terminate for the above case where array = [5,10,15,20,25] and target = 13. And so, we can conclude that the algorithm doesn't always terminate.

But say if I had array = [5,10,15,20,25] and target = 1, then the algorithm would terminate.

So, using inputs to determine whether an algorithm always terminates or not is not good because it is not a foolproof way of determining whether an algorithm always terminates or not.

And so my question is, is there a way I can prove that the above algorithm always terminates without using any inputs/cases?

Thank you for any suggestions and insights. Appreciate the help.

Answer 1

Loop termination proofs can be carried by means of a variant function, that can be proven to decrease and to have a lower bound. In the given case, consider the quantity hi - lo.

After a single iteration, the new value is one of

• hi - mid = hi - (hi + lo)//2 = (hi - lo)\\2

• mid - lo = (hi + lo)//2 - lo = (hi - lo)//2

(We used the notation // for the by-default quotient and \\ for by-excess.)

We see that the variant function always decreases, except when hi - lo = 1 and lo = mid is chosen.

---

In general, the variant function can be drawn from the rationale of the algorithm, in which you "do something to get closer to the solution". Here, you reduce the interval of uncertainty. Common problems are off-by-one situations, as is the case here.

Answer 2

In a binary search, if you want to make sure that the loop terminates, then you need to make sure that the range (hi-lo) shrinks with every iteration. You also need to make sure that lo and hi are within the valid range (1-N in your case).

It starts with your test:

if target >= array[mid]:

If this test is false, then mid is too high. If this test passes, though, then mid is not necessarily too low. It might be the value you're looking for. Knowing that, you can can handle the cases:

if target >= array[mid]:
    # answer is >= mid
    lo = mid
else:
    # answer is < mid
    hi = mid-1

So here you see the first problem fixed -- because you're using a "too high" test instead of a "too low" test, you get hi = mid-1 -- a little bit unusual, but we can make it work.

So, now you know how the range is going to change. Given lo < hi and mid, the two possible new ranges are [lo,mid-1] and [mid,hi]. BOTH of these ranges must be smaller than [lo,hi] if you want the loop to terminate in all cases. so you require mid-1 < hi, which is the same as mid <= hi, and you require mid > lo, which is the same as lo <= mid-1. Those ranges also need to be valid, so you require lo <= mid-1 and mid <= hi, which happen to be the same as the above conditions.

With all of that together, you need: lo <= mid-1 < mid <= hi. The way you currently calculate mid does NOT ensure this. In order to make sure that lo < mid, you need to round UP, so you should set mid like this:

mid = (lo+hi+1)//2

Or even better, like this:

mid = lo + (hi+1-low)//2

That gives the same answer, but avoids overflowing integers in some languages. It's a good habit.

With these changes, your binary search will work.