选择在Dafny中排序

Question

我正在尝试在Dafny中实现选择排序.

我sorted和FindMin函数确实有效,但selectionsort它本身包含Dafny无法证明的断言,即使它们是正确的.

这是我的计划:

predicate sorted(a:array<int>,i:int)
  requires a != null;
  requires 0 <= i <= a.Length;
  reads a;
{
  forall k :: 0 < k < i ==> a[k-1] < a[k]
}
method FindMin(a:array<int>,i:int) returns(m:int)
  requires a != null;
  requires 0 <= i < a.Length;
  ensures i <= m < a.Length;
  ensures forall k :: i <= k < a.Length ==> a[k] >= a[m];
{
  var j := i;
  m := i;
  while(j < a.Length)
    decreases a.Length - j;
    invariant i <= j <= a.Length;
    invariant i <= m < a.Length;
    invariant forall k :: i <= k < j ==> a[k] >= a[m];
  {
    if(a[j] < a[m]){m := j;}
    j := j + 1;
  }
}
method selectionsort(a:array<int>) returns(s:array<int>)
  requires a != null;
  modifies a;
  ensures s != null;
  ensures sorted(s,s.Length);
{
  var c,m := 0,0;
  var t;
  s := a;
  assert s != null;
  assert s.Length == a.Length;
  while(c<s.Length)
    decreases s.Length-c;
    invariant 0 <= c <= s.Length;
    invariant c-1 <= m <= s.Length;
    invariant sorted(s,c);
  {
    m := FindMin(s,c);
    assert forall k :: c <= k < s.Length ==> s[k] >= s[m];
    assert forall k :: 0 <= k < c ==> s[k] <= s[m];
    assert s[c] >= s[m];
    t := s[c];
    s[m] := t;
    s[c] := s[m];
    assert s[m] >= s[c];
    assert forall k :: c <= k < s.Length ==> s[k] >= s[c];
    c := c+1;
    assert  c+1 < s.Length ==> s[c-1] <= s[c];
  }
}

为什么这是错的？"postcondtion可能不成立"是什么意思？达夫能举一个反例吗？

Answer 1

您似乎理解循环不变量背后的基本思想,这是使用Dafny验证程序所必需的.

你的程序不正确.发现这种情况的一种方法是在Visual Studio中使用Dafny IDE中的验证调试器.点击报告的最后一个错误(在增量前行的断言c),你会看到,阵列的上半部分包含比两个小的元素s[c]和s[m].然后选择3语句交换操作周围的程序点,你会发现你的交换实际上没有交换.

要修复交换,请交换3语句交换的第二个和第三个语句.更好的是,利用Dafny的多重赋值语句,使代码更容易正确:

s[c], s[m] := s[m], s[c];

还有另外两个问题.一个是循环内的第二个断言不验证:

assert forall k :: 0 <= k < c ==> s[k] <= s[m];

虽然s[m]是数组上半部分中的最小元素,但循环不变量需要记录数组下半部分中的元素不大于上部中的元素 - 这是选择排序算法的基本属性.以下循环不变量可以解决问题:

invariant forall k, l :: 0 <= k < c <= l < a.Length ==> s[k] <= s[l];

最后,关于sorted(s,c)不被循环维护的属性的抱怨源于你定义sorted为严格增加的事实,除非数组的元素最初都是不同的,否则交换永远不会实现.因此,Dafny指出了您必须对排序例程做出的设计决定.您可以决定您的selectionsort方法仅适用于没有重复元素的数组,您可以通过添加来实现

forall k, l :: 0 <= k < l < a.Length ==> a[k] != a[l];

作为(并循环不变)的前提条件selectionsort.或者,更传统,可以解决您的定义sorted,以取代a[k] > a[m]用a[k] >= a[m].

要稍微清理代码,您现在可以删除所有断言语句和声明t.由于m仅在循环内部使用,因此可以将声明移动m到调用语句FindMin,这也表明c-1 <= m <= s.Length不需要循环不变量.这两个decreases条款可以省略; 对于您的程序,Dafny将自动提供这些.最后,您的selectionsort方法修改了给定的数组,因此没有真正的理由a在out参数中返回引用s; 相反,你可以省略out-parameter并s在a任何地方替换.