Binarysearch

binarysearch.dfy

datatype Option<T> = None | Some(x: T)

method BinarySearch(haystack: array<int>, needle: int) returns (n: Option<int>) 


requires forall i, j :: 0 <= i <= j < haystack.Length ==> haystack[i] <= haystack[j]
ensures n.Some? ==> 
    0 <= n.x < haystack.Length && haystack[n.x] == needle
ensures n.None? ==> 
    forall i :: 0 <= i < haystack.Length ==> haystack[i] != needle
{
    n := None;
    var low, high: int := 0, (haystack.Length - 1);
    while low <= high
    decreases high - low
    invariant low <= haystack.Length
    invariant high < haystack.Length
    invariant forall i :: 0 <= i < low ==> haystack[i] != needle
    invariant forall i :: i >= 0 && high < i < haystack.Length ==> haystack[i] != needle
    {
        assert high >= low;
        var lh: int := (low + high);
        var m := (low + high) / 2 + (low + high) % 2;
        assert m >= 0;
        if haystack[m] == needle 
        {
            return Some(m);
        } 
        else if haystack[m] < needle
        {
            low := m + 1;
        }
        else
        {
            high := m - 1;
        }
    }
    return None;
}