如果数组从0到i-1排序，并且a [i-1]小于a [i]，为什么达夫尼不能证明数组从0到i排序？

问题描述

考虑以下代码：

predicate sorted(a:array<int>,min:int,max:int)
    requires a != null
    requires 0 <= min <= max <= a.Length 
    reads a
{
    forall i,j | min <= i < j < max :: a[i] <= a[j] 
}

method test(a:array<int>,i:int)
    requires a!=null 
    requires a.Length>i
    requires i>0
    requires sorted(a,i-1)
    requires a[i-1]<a[i]
    ensures sorted(a,i)
{
    
}

方法test要求数组a从0到i-1排序，并且a[i-1] < a[i]排序。但是Dafny报告了一个错误，其后置条件是a从0到i进行排序。这不是很明显吗？达夫妮为什么不能证明呢？

解决方法

Dafny无法证明它的原因是因为它是错误的。我们可以使用test来证明错误，如下所示：

method using_test_proves_false()
{
  var a := new int[3];
  a[0] := 8;
  a[1] := 7;
  a[2] := 9;
  assert sorted(a,1);
  assert a[0] > a[1];
  assert !sorted(a,2);
  assert a[1] < a[2];
  test(a,2);
  assert sorted(a,2);
  assert false;
}

基本问题是i要求中的test上存在一个错误的错误。我想您可能想说a[i-2] < a[i-1]？

---

另外，根据您的要求a != null，您似乎使用的是Dafny的较旧版本。我建议升级到最新版本。