CODEWITHSUNDEEP
dafny
mazin
mazin

Reputation: 395

Why is my Dafny assertion failing on both x == y and x != y?

I'm following the tutorials here and the code seems correct but when I test using assertions I get an error!

Running the program prints the correct answer, but the assertions seem to be paradoxical. When a show the counter examples it seems that -1 is considered even though it shouldn't be.

method binarySearch(a:array<int>, key:int) returns (r:int) 
    requires forall i,j :: 0 <= i <= j < a.Length ==> a[i] <= a[j]
    ensures 0 <= r ==> r < a.Length && a[r] == key 
    ensures r < 0 ==> forall i :: 0 <= i < a.Length ==> a[i] != key
{

    var lo, hi := 0, a.Length;

    while (lo < hi) 
        invariant 0 <= lo <= hi <= a.Length
        invariant forall i :: 0 <= i < lo ==> a[i] < key
        invariant forall i :: hi <= i < a.Length ==> a[i] > key
        decreases hi - lo;
    {
        var mid := (lo + hi) / 2;
        if key < a[mid] 
        {
            hi := mid;
        }
        else if key > a[mid]
        {
            lo := mid + 1;
        }
        else 
        {
            return mid;
        }
    }

    return -1;
}


// tests
method Main() 
{
    var a := new int[6][1,2,3,4,5,6];
    var r := binarySearch(a, 5);

    assert r == 4;  // fails
    assert r != 4;  // also fails
}

Is this a bug or am I missing something?

Upvotes: 1

Views: 282

Answers (1)

Divyanshu Ranjan
Divyanshu Ranjan

Reputation: 1625

Dafny uses post-condition of method to reason about result of method call.

Here post-condition is

  • If r is between 0 to array length, element at r is equal to key
  • If r is less than 0, it is not in array.

Dafny doesn't know which of these is vacuous, but you can hint it. Guarding assert r == 4 with if r >= 0 && r < a.Length will make it verify.

Alternatively after adding assert a[4] == 5 before assert r == 4, verification will go through.

Reason for strange error is after call to binary search, these are facts known to dafny

  • assert (r < 0) || (0 <= r < 6)
  • assert (r < 0) ==> forall i :: 0 <= i < a.Length ==> a[i] != 5
  • assert (0 <= r < 6) ==> a[r] == 5

Using these it can neither prove r == 4 nor r != 4. Dafny doesn't seem to propagate information like assert a[0] == 1 etc by default to prover, you have to explicitly ask for it.

Upvotes: 2

Related Questions