为什么这个达夫尼方法在应该成立的时候却没有成立？

Question

method search(a: array<int>) returns (i : int)
  requires a.Length > 1 && a[0] == a[a.Length-1]
  ensures 0 <= i < a.Length-1 && a[i] >= a[i + 1]
{
  i := ......;
  var j := ......;
  while i != j
    invariant ......;
  {
    var m := (i + j) / 2;
    if a[....] >= a[....] {
      i := .....;
    } else {
      j := .....;

    }
  }
}

这是我在大学介绍 Dafny 课程时遇到的一个实验室问题。您只能修改 5 个空格，并根据需要添加任意数量的断言，以使该方法可验证。这是我解决这个问题的尝试：

method search(a: array<int>) returns (i: int)
  requires a.Length > 1 && a[0] == a[a.Length-1]
  ensures 0 <= i < a.Length-1 && a[i] >= a[i+1]
{  
  i := 0;
  var j := a.Length - 2;
  while i != j
    invariant 0 <= i <= j < a.Length - 1;
  {
    var m := (i + j) / 2;

    if a[j] >= a[j + 1]{
      i := j;
      assert a[j] >= a[j + 1] && a[i] >= a[i + 1];
      assert i == j;
    } else {
      j := j - 1;
    }
  }
  
  assert 0 <= i < a.Length - 1; 
  assert a[j] >= a[j + 1] && a[i] >= a[i + 1];
}

最后一个断言显然应该成立，但它似乎并不成立。由于该算法是线性搜索（遍历所有可能性），并且当循环执行时我们实际上找到了正确的值。完全相同的断言在循环终止之前成立。但是，它在循环之外并不成立，我不明白。有什么想法吗？

Answer 1

首先，Dafny 并没有准确地运行代码。它在循环块/方法之外唯一知道的是 invariant/ensures 子句指定的内容。目前，您的循环没有说明

a[i]

和

a[j]

或

a[i+1]

之间的关系。因此，在循环之外它只知道

i == j

并且忘记了循环内完成的工作。

其次，您没有将变量

m

用于任何用途。

他们的关键是从一开始就进行归纳思考

a[i] == a[j+1]

因为

a[0] == a[a.Length-1]

，所以你的目标是找到能够维持这种关系向前发展的关系。

我找到了几个解决方案，但它们不是给定存根的正确解决方案，因为我更改了

if

块中分配的变量。他们应该让您了解您错过了什么，而不透露答案。

method search(a: array<int>) returns (i: int)
        requires a.Length > 1 && a[0] == a[a.Length-1]
        ensures 0 <= i < a.Length-1 && a[i] >= a[i+1]
    {  
        i := 0;
        var j := a.Length - 2;
        while i != j
            invariant 0 <= i <= j < a.Length - 1
            invariant a[i] >= a[j + 1]
        {
            var m := (i + j) / 2;

            if a[i] >= a[m+1] {
                //assigning j instead of i
                j := m;
            } else {
                // assert a[i] >= a[j + 1];
                // assert a[i] < a[m+1];
                i := m + 1;
                // assert a[i] >= a[j + 1];
            }
        }
    }

    method search1(a: array<int>) returns (i: int)
        requires a.Length > 1 && a[0] == a[a.Length-1]
        ensures 0 <= i < a.Length-1 && a[i] >= a[i+1]
    {  
        i := 0;
        var j := a.Length - 2;
        while i != j
            invariant 0 <= i <= j < a.Length - 1
            invariant a[i] >= a[j + 1]
        {
            var m := (i + j) / 2;
            //Isn't using m

            if a[j] >= a[j + 1]{
            i := j;
            assert a[j] >= a[j + 1] && a[i] >= a[i + 1];
            assert i == j;
            } else {
            j := j - 1;
            }
        }
        
        assert 0 <= i < a.Length - 1; 
        assert a[i] >= a[i + 1];
    }