Question

Prove binary search (Seen below) is correct using a loop invariant.

def search_binary(arr, val):
    low, up = 0, len(arr) - 1
    while low != up:
        # binary search
        mid = (low + up) / 2

        if arr[mid] == val:
            return mid
        elif val < arr[mid]:
            up = mid - 1
        else:
            low = mid + 1

    return low

Answer 1

def binsearch(int x, int[] A, int n)
    //@requires 0 <= n && n <= \length(A);
    //@requires is_sorted(A, 0, n);
    /*@ensures (-1 == \result && !is_in(x, A, 0, n))
    || ((0 <= \result && \result < n) && A[\result] == x);
    @*/
    { int lo = 0;
    int hi = n;
    while (lo < hi)
    //@loop_invariant 0 <= lo && lo <= hi && hi <= n;
    //@loop_invariant (lo == 0 || A[lo-1] < x);
    //@loop_invariant (hi == n || A[hi] > x);
        { int mid = lo + (hi-lo)/2;
        //@assert lo <= mid && mid < hi;
        if (A[mid] == x) return mid;
        else if (A[mid] < x) lo = mid+1;
        else /*@assert(A[mid] > x);@*/
        hi = mid;
        }
    return -1;
}

Drop a comment for any clarification or update, I would love to assist you.