断言涉及序列的方法的 return 值

Question

我是 Dafny 的初学者，我想知道为什么违反了 Main 方法中打印之前的断言。我正在尝试找到应该插入项目的最右边的索引，以便保留序列中的顺序，在这种特定情况下是 4。

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

Answer 1

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

首先，请记住 Dafny 分别对每种方法进行推理，仅使用其他方法的规范。所以在 Main 中，Dafny 唯一知道的关于 BinarySearchInsertionHint 的就是它的后置条件。现在事实证明 hint == 4 实际上确实遵循后置条件，但要让 Dafny 相信这一点并不容易。

这将我们带到这里发生的第二件事，即量词触发器。 BinarySearchInsertionHint 的后置条件使用通用量词 (forall)，这是 Dafny 使用句法启发式进行实例化的原因。此示例中的两个量词均在 a[i] 上触发，这意味着它们不会在值 v 时使用，除非 a[v] is "in scope" 给验证者。

您可以通过提及 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 的模块化验证、不完整性和量词触发器的更多信息

断言涉及序列的方法的 return 值

Asserting about the return value of a method involving sequences

formal-verification

seq

dafny