How can I prove this binary search algorithm is correct using hoare logic?

Question

This is the algorithm:

// Precondition: n > 0

l = -1;
r = n;

while (l+1 != r) {
    m = (l+r)/2;

    // I && m == (l+r)/2

    if (a[m] <= x) {
        l = m;
    } else {
        r = m;
    }
}
// Postcondition: -1 <= l < n

I have done some research and narrowed the invariant down to if x is in a[0 .. n-1] then a[l] <= x < a[r].

I have no idea how to progress from there though. The precondition seems too broad, so I'm having trouble showing that P -> I.

Any help is extremely appreciated. These are the logic rules that can be used to prove the algorithm's correctness:

Answer 1

The invariant is

-1 <= l and l + 1 < r <= n and a[l] <= x < a[r]

with the implicit convention a[-1] = -∞, a[n] = +∞.

Then in the if statement

a[l] <= x < a[r] and a[m] <= x implies a[m] <= x < a[r]

and

a[l] <= x < a[r] and x < a[m] implies a[l] <= x < a[m].

In either case, the assignment establishes a[l] <= x < a[r].

At the same time, -1 <= l and l + 1 < r <= n ensures -1 < m < n, so that the evaluation of a[m] is possible.

Upon termination, l + 1 = r and by the invariant

-1 <= l < n and a[l] <= x < a[l + 1].