Dafny中两种数组递增描述为何导致二分搜索验证失败？

验证通过的二分搜索代码 #

method BinarySearch(a: array<int>, key: int) returns (index: int)
    requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]

    ensures 0 <= index ==> index < a.Length && a[index] == key
    ensures index < 0 ==> forall k :: 0 <= k < a.Length ==> a[k] != key
{
    var l, r := 0, a.Length;
    while l < r
        invariant 0 <= l <= r <= a.Length
        invariant forall i ::
         0 <= i < a.Length && !(l <= i < r) ==> a[i] != key
    {
        var m := (l + r) / 2;
        if a[m] < key {
            l := m + 1;
        } else if key < a[m] {
            r := m;
        } else {
            return m;
        }
    }

    return -1;
}

问题描述 #

原前置条件requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j]用于描述数组递增，但将其替换为requires forall i :: 0 < i < a.Length ==> a[i - 1] <= a[i]后，验证失败，编译器提示无法证明循环不变式invariant forall i :: 0 <= i < a.Length && !(l <= i < r) ==> a[i] != key。从逻辑上看两个表达式语义相同，请问二者存在什么差异？

差异解析 #

这两个表达式逻辑语义完全等价，核心差异在于Dafny自动定理证明器对它们的处理能力不同：

• 原前置条件是全局递增的直接断言：直接声明数组中任意两个索引i<j都满足a[i]<=a[j]，证明器可以直接使用这个全局性质，快速推导数组任意区间内的元素大小关系。比如在循环中调整l或r时，证明器能直接利用该条件得出“a[m]<key则所有<=m的元素都小于key”这类结论，从而顺利维护循环不变式。

• 替换后的前置条件是相邻元素递增的局部断言：虽然它逻辑上等价于全局递增，但证明器无法自动完成从“相邻递增”到“全局递增”的归纳推理。Dafny的自动证明器默认不会触发归纳步骤，当循环中需要用到全局递增性质时，它无法从局部条件推导出来，导致无法证明循环不变式的维护过程。

解决思路 #

如果要使用相邻递增的前置条件，需要手动给证明器提供额外的推理依据：

• 编写辅助引理（lemma），证明“相邻元素递增的数组必是全局递增数组”，并在方法中调用该引理；
• 在循环不变式中补充区间内的递增性质，比如添加invariant forall i,j :: l <= i < j < r ==> a[i] <= a[j]，帮助证明器逐步维护全局递增的推导链。

内容的提问来源于stack exchange，提问作者ZhouTi