时间戳

首页 > 解决方案 > 如果一个数组从 0 到 i-1 排序，并且 a[i-1] 小于 a[i]，为什么 Dafny 不能证明该数组是从 0 到 i 排序的呢？

dafny - 如果一个数组从 0 到 i-1 排序，并且 a[i-1] 小于 a[i]，为什么 Dafny 不能证明该数组是从 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,0,i-1)
    requires a[i-1]<a[i]
    ensures sorted(a,0,i)
{
    
}

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

标签： dafny

解决方案

Dafny 无法证明的原因是因为它是假的。我们可以用test如下方式证明假：

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

i基本问题是需求中有一个错误test。我想你可能是想说a[i-2] < a[i-1]？

此外，根据您的要求a != null，您可能使用的是相当旧的 Dafny 版本。我建议升级到最新版本。

推荐阅读