CODEWITHSUNDEEP
seqformal-verificationdafny
lilezek
lilezek

Reputation: 7374

Asserting about the return value of a method involving sequences

I'm a beginner with Dafny, and I'm wondering why the assertion just before the print in the Main method is violated. I'm trying to find the rightmost index where an item should be inserted in order to preserve the order in the sequence, which in this specific case is 4.

https://rise4fun.com/Dafny/4lR2

method BinarySearchInsertionHint(a: seq<int>, key: int) returns (r: int) 
    requires forall i,j :: 0 <= i < j < |a| ==> a[i] <= a[j]
    ensures 0 <= r <= |a|
    ensures forall i :: 0 <= i < r ==> a[i] <= key
    ensures r < |a| ==> forall i :: r <= i < |a| ==> key < a[i]
{
    var lo, hi := 0, |a|;
    while lo < hi
        decreases hi - lo
        invariant 0 <= lo <= hi <= |a|
        invariant forall i :: 0 <= i < lo ==> a[i] <= key
        invariant forall i :: hi <= i < |a| ==> key < a[i]
    {
        var mid := (lo + hi) / 2;
        assert(lo <= mid < hi);
        if a[mid] <= key {
            lo := mid + 1;
        } else if key < a[mid] {
            hi := mid;
        }
    }
    assert(lo == hi);
    r := lo;
}

method Main() {
    var a := [0, 1, 1, 1, 2];
    var hint := BinarySearchInsertionHint(a, 1);
    assert hint == 4; // assertion violation
    print hint;
}

Upvotes: 3

Views: 200

Answers (1)

James Wilcox
James Wilcox

Reputation: 5663

This can indeed be confusing! There are a few things going on here.

First, remember that Dafny reasons about each method separately, using only the specifications of other methods. So in Main, the only thing Dafny will know about BinarySearchInsertionHint is its postconditions. Now it turns out that hint == 4 actually does follow from the postconditions, but it's a little nontrivial to convince Dafny of this.

This brings us to the Second Thing going on here, which is quantifier triggers. The postconditons of BinarySearchInsertionHint use universal quantifiers (forall), which Dafny reasons about using syntactic heuristics for instantiation. Both of the quantifiers in this example are triggered on a[i], which means that they will not be used at value v unless a[v] is "in scope" for the verifier.

You can get the assertion to pass by mentioning a[3] and a[4], which is enough for Dafny to figure out from the postconditions that hint must be 4. Like this:

method Main() {
    var a := [0, 1, 1, 1, 2];
    var hint := BinarySearchInsertionHint(a, 1);
    assert a[3] == 1;  // these assertions just "mention" a[3] and a[4]
    assert a[4] == 2;
    assert hint == 4;  // assertion now passes
    print hint;
}

You can read more about Dafny's modular verification, incompleteness, and quantifier triggers in the Dafny FAQ.

Upvotes: 3

Related Questions