1

我想实现一个方法，它接受一个输入的字符数组并以相反的顺序输出另一个由输入数组组成的数组。但我收到错误“索引我们的范围”和“后置条件可能不成立”我不知道会发生什么

这是我的代码：

predicate reversed (arr : array<char>, outarr: array<char>)
requires arr != null && outarr != null
//requires 0<=k<=arr.Length-1
reads arr, outarr
{
  forall k :: 0<=k<=arr.Length-1 ==> outarr[k] == arr[(arr.Length-1-k)]
}

method yarra(arr : array<char>) returns (outarr : array<char>)
requires arr != null && arr.Length > 0
ensures outarr != null && reversed(arr,outarr)
{
  var i:= 0;
  var j:= arr.Length-1;
  outarr := new char[arr.Length];
  outarr[0] := arr[j];
  i := i+1;
  j := j-1;
  while i<arr.Length && 0<=j<arr.Length
  invariant 0<=i<=arr.Length
  decreases arr.Length-i, j
  {
    outarr[i] := arr[j];
    i:=i+1;
    j:=j-1;
  }
  //return outarr;
 }

method Main()
{
  var s := ['a','b','a','b','a','b','a','b','a','b','a','b'];
  var a,b,c,d := new char[5], new char[5], new char[5], new char[5];
  a[0], a[1], a[2], a[3], a[4] := 'y', 'a', 'r', 'r', 'a';
  d[0], d[1], d[2], d[3], d[4] := 'y', 'a', 'r', 'r', 'a';
  b := yarra(a);
  c := yarra(b);
  assert c[..] == a[..];
  //assert c.Length > -2;
  //assert d[0] == a[0];
  //print c; print a;
}
  1. 错误 1 ​​索引超出范围 6 43
  2. 错误 2 后置条件可能在此返回路径上不成立。21 2

  3. 这是可能不成立的后置条件。13 26

    stdin.dfy(6,43)：错误：索引超出范围
    stdin.dfy(21,2)：错误 BP5003：后置条件可能不会在此返回路径上成立。
    stdin.dfy(13,26)：相关位置：这是可能不成立的后置条件。
    stdin.dfy(6,2)：相关位置
    stdin.dfy(6,47)：相关位置

4

1 回答 1

1

这是您的程序可以验证的版本。

有几个问题需要解决。

首先，您的定义reversed不正确，因为 Dafny 看不到访问权限outarr[k]。我通过arr.Length == outarr.Length向reversed.

接下来，在任何地方都需要考虑新的前提条件reversed。唯一这样的地方是在 的后置条件中yarra，我通过添加一个额外的后置条件来修复它arr.Length == outarr.Length。

然后，Dafny 抱怨后置条件reversed可能不成立yarra。这需要加强循环不变量。这是一个典型的例子，我们试图通过一个一个地建立每个索引来证明数组的所有索引。在这种情况下，正确的循环不变量是“我已经在小于当前索引的每个索引处建立了它”。我们在这个循环中建立的是outarr[k] == arr[arr.Length-1-k]，所以正确的不变量是：

forall k | 0 <= k < i :: outarr[k] == arr[arr.Length-1-k]

最后，为此，我们需要不变量j == arr.Length - 1 - i. （事实上​​，这个不变量意味着我们可以完全摆脱j，但我并没有费心去做。）

于 2017-07-30T06:14:09.763 回答