1

我想在该方法中做的只是覆盖前一个数组并用排序的数字填充它，但是 dafny 说后置条件不成立，我终生无法弄清楚原因。我猜我需要在循环中添加一些不变量，但是由于在进入循环之前检查了它们，所以我不知道如何放置有效的不变量。

method sort2(a : array<int>)
modifies a;
requires a != null && a.Length >= 2;
ensures sorted2(a[..]);
{
  var i := a.Length - 1;
  while (i >= 0)
  decreases i
 {
     a[i] := i;
     i := i - 1;
 }
}

predicate sorted2(s: seq<int>)
{
    forall i :: 1 <= i < |s| ==> s[i] >= s[i-1]
}

我之前的尝试只是重新初始化 a 但 dafny 显然不允许内部方法。

4

1 回答 1

1

你确实需要一个循环不变量来证明这个程序是正确的。

请参阅Dafny 教程的第 6 节，了解循环不变量的一般介绍以及如何提出它们。

在这种情况下，一个好的循环不变量将类似于sorted(a[i+1..])，它表示索引之后的数组部分i已排序。这样，当循环终止并且i为零时，您将知道整个数组已排序。

您还需要一个或两个更多的循环不变量来描述i数组本身的边界和元素。

于 2017-12-06T17:01:28.610 回答