# Proof of correctness for Binary Search algorithm to find length of array for unknown length

For the algorithm provided in answer to this question, how would I go about proving the correctness of the algorithm?

The referenced question is:

“You are given an array $$A$$ of length $$n$$. Each value is $$1$$. However, you do not know what the value of $$n$$ is. You are allowed to access an element $$i$$ of the array by calling $$A[i]$$. If $$i < n$$, this will return $$1$$, and if $$i \geq n$$, this will return a message saying that the location does not exist (you can think of this as an error message, but it will not crash your program). Describe an $$O(\log(n))$$ algorithm to determine the value of $$n$$.”

Here is the algorithm given to solve the problem:

def length(L):
lo = 0
hi = 1

while 1:
hi *= 2

try:
L[hi]
except IndexError:
break

while lo < hi:
mid = (lo + hi) // 2

try:
L[mid]
lo = mid + 1
except IndexError:
hi = mid

return hi



I tried proving it by strong induction on the length of the array, where hi would be equal to the length (i.e., at the end of the algorithm, hi would be set to the last out of bounds element and would therefore be the length of the array), but the proof didn’t really make sense

The length of the array is $$n_{min} \le n \le n_{max}$$. Initially all you know is that $$n_{min} = 0$$ and $$n_{max} = \inf$$. Every step of the algorithm gives you more information. If $$n_{min} = n_{max}$$ then you know n. You need to examine the steps of the algorithm and show that it ends with that condition.