seq - 声明涉及序列的方法的返回值

我是Dafny的初学者，我想知道为什么违反了Main方法中打印之前的断言。我试图找到应该在其中插入项目的最右边的索引，以保留顺序(在此特定情况下为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;
}

最佳答案

这确实令人困惑!这里发生了一些事情。

首先，请记住，Dafny仅使用其他方法的规范来分别说明每种方法的原因。因此，在Main中，Dafny对BinarySearchInsertionHint唯一了解的就是它的后置条件。现在，事实证明hint == 4实际上确实遵循了后置条件，但是说服Dafny做到这一点并不容易。

这将我们带到第二件事，即量词触发器。 BinarySearchInsertionHint的后置条件使用通用量词(forall)，这是Dafny提出的使用句法启发式进行实例化的原因。此示例中的两个量词都是在a[i]上触发的，这意味着除非对验证者v在“范围内”，否则它们将不会在a[v]值上使用。

您可以通过提及a[3]和a[4]来传递断言，这足以让Dafny从hint必须为4的后置条件中找出来。像这样:

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;
}

您可以在Dafny FAQ中阅读有关Dafny的模块化验证，不完整性和数量触发器的更多信息。