断言涉及序列的方法的返回值答案

【问题标题】：Asserting about the return value of a method involving sequences断言涉及序列的方法的返回值
【发布时间】：2019-10-10 08:32:40
【问题描述】：

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

【问题讨论】：

标签： seq formal-verification dafny

【解决方案1】：

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

首先，请记住，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 的模块化验证、不完整性和量词触发器的更多信息。

【讨论】：