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:

Post-condition of the `while` loop is the inverse of its continuation condition, so in your case it is `!(l+1 != r)`, i.e. `l+1 == r`. — Sergey Kalinichenko, Oct 26 '16 at 12:46

score 1 · Accepted Answer · 2016-10-26T13:01:14.480

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].

edited Oct 26 '16 at 13:01

answered Oct 26 '16 at 12:51

But according to hoare's logic rules, I must begin by proving that the precondition implies the invariant. How could I do that? – Marcos Pereira Oct 26 '16 at 13:12
1

precond `n>0` and then two first assignments `l=-1; r=n` leads to `l=-1` and `r=n>0`, then it obviously implies `l>=-1` and `l+1 – Jean-Baptiste Yunès Oct 26 '16 at 14:38
1

@marcospgp: yep, this is quasi-trivial: certainly `-∞ <= x < +∞`. – Oct 26 '16 at 14:49
You said "upon termination, l + 1 = r", but the invariant says `l + 1 < r`. Shouldn't the invariant say `l < r`? – Marcos Pereira Oct 26 '16 at 16:19
@marcospgp: no, the invariant is invariant as long as you are in the loop and can be invalidated when you exit. – Oct 26 '16 at 16:40
1

Are you sure? The invariant is supposed to be true before and after any iteration of the loop, and can only not be true during the loop. "The loop invariants will be true on entry into a loop and following each iteration, so that on exit from the loop both the loop invariants and the loop termination condition can be guaranteed." from https://en.wikipedia.org/wiki/Loop_invariant – Marcos Pereira Oct 26 '16 at 16:49
@YvesDaoust, no, the invariant should hold after the loop as well. `[inv] while (cond) { [inv /\ cond] ... [inv] } [inv /\ !cond]` – aioobe Jan 03 '17 at 09:02

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

1 Answers1