The following is a Binary Search algorithm verified with Dafny:

以下是与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;
}

The pre-condition requires forall i, j :: 0 <= i < j < a.Length ==> a[i] <= a[j] describes the array as incremental. However, when I replace it with another expression:requires forall i :: 0 < i < a.Length ==> a[i - 1] <= a[i], the verification failed, and the compiler said the invariant invariant forall i :: 0 <= i < a.Length && !(l <= i < r) ==> a[i] != key cannot be proved.

前置条件要求for all i，j：：0<=i a[i]<=a[j]将数组描述为增量数组。但是，当我将其替换为另一个表达式：Requires for all i：：0 a[i-1]<=a[i]时，验证失败，编译器说for all i：：0<=i a[i]！=键的不变不变量无法证明。

To me, the two expressions show the same meaning. What's the difference?

对我来说，这两个短语的意思是一样的。有什么关系呢？

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]

需要所有的i，j：：0<=i a[i]<=a[j]->需要所有的i：：0 a[i-1]<=a[i]

The issue is that the first form explicitly encodes the transitive relationship between elements, whilst the second does not. Transitivity is needed to show, for example, that a[l] <= a[m] in the loop body. Thus, in the second form, the verifier must extract the transitive relationship itself (which it cannot).

问题是，第一种形式显式地编码了元素之间的传递关系，而第二种形式没有。例如，需要及物性来表明循环体中的a[L]<=a[m]。因此，在第二种形式中，验证器必须提取传递关系本身(它不能)。

We can see this by trimming the example down:

我们可以通过缩减示例来了解这一点：

method BinarySearch(a: array<int>, key: int) returns (index: int)
requires forall i :: 0 < i < a.Length ==> a[i-1] <= a[i]
{
    //
    assert forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j];
    //
    return -1;
}

This assertion fails to verify. However, we can get it to verify by adding in the missing transitivity information using a lemma:

这一断言没有得到证实。然而，我们可以通过使用引理添加缺失的传递性信息来验证它：

lemma LemmaTransitivity(a: seq<int>)
requires forall i :: 0 < i < |a| ==> a[i-1] <= a[i]
ensures forall i,j :: 0 <= i < j < |a| ==> a[i] <= a[j]
{
    if |a| > 2 {
        LemmaTransitivity(a[1..]);
        assert a[0] <= a[1];
    }
}

method BinarySearch(a: array<int>, key: int) returns (index: int)
requires forall i :: 0 < i < a.Length ==> a[i-1] <= a[i]
{
    //
    LemmaTransitivity(a[..]);
    assert forall i,j :: 0 <= i < j < a.Length ==> a[i] <= a[j];
    //
    return -1;
}

This now verifies. Furthermore, we can use it to verify your original example. Note: a[..] converts an array into a seq which is just an easier form to work with in the lemma.

这一点现在得到了验证。此外，我们还可以用它来验证您的原始示例。注：A[..]将数组转换为SEQ，这只是在引理中更容易使用的形式。