sorting - 选择排序在达夫尼

我正在尝试在Dafny中实施选择排序。

我的sorted和FindMin函数可以工作，但是selectionsort本身包含达夫尼不会证明的断言，即使它们是正确的。

这是我的程序：

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];
  }
}

为什么会这样呢？ “后处理可能不成立”是什么意思？达夫妮能举个反例吗？

最佳答案

您似乎了解了循环不变式背后的基本思想，这是使用Dafny验证程序所必需的。

您的程序不正确。一种发现方法是在Visual Studio的Dafny IDE中使用验证调试器。单击最后报告的错误（在c增量之前的行上的断言），您将看到数组的上半部分包含一个小于s[c]和s[m]的元素。然后选择三语句交换操作周围的程序点，您会注意到交换实际上并没有进行交换。

要解决此交换问题，请交换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]。

为了稍微清理代码，您现在可以删除所有assert语句和t声明。由于m仅在循环内使用，因此您可以将m的声明移到调用FindMin的语句，这也很明显不需要循环不变的c-1 <= m <= s.Length。可以省略两个decreases子句；对于您的程序，Dafny将自动提供。最后，您的selectionsort方法在适当的位置修改了给定的数组，因此没有真正的理由在输出参数a中返回引用s。取而代之的是，您可以忽略输出参数，并在任何地方用s替换a。