我在 dafny 中的代码有什么问题？

Question

我尝试使用 dafny 来验证我的 qsort 函数的正确性，但我不知道为什么我的代码验证失败。这是我的代码：

    method Testing (a: array<int>)
      requires  a.Length > 0
      modifies a
    {
        qsort(a,0,a.Length-1);
        var i :int := 0;
        while(i<a.Length-1)
          decreases a.Length - 1 - i
        {
          assert a[i] <= a[i+1];
          i := i+1;
        }
    }
    method qsort(a: array<int>,left: int,right: int)
        requires left>=0 && right < a.Length
        modifies a
        decreases right - left
    {
      if (right > left)
      {
          var pivotValue: int := a[left];
          var t: int := a[left];
          a[left] := a[right-1];
          a[right-1] := t;
          var storeIndex: int := left;
          var i :int := left;
          while i < right - 1
            invariant left <= storeIndex < right
            decreases right - i
          {
              if a[i] < pivotValue
              {
                t := a[storeIndex];
                a[storeIndex] := a[i];
                a[i] := t;
                storeIndex := storeIndex+1;
              }
              i := i+1;
          }
          t := a[right-1];
          a[right-1] := a[storeIndex];
          a[storeIndex] := t;
          qsort(a,left,storeIndex);
          qsort(a,storeIndex+1,right);
      }  
    }

错误是：

断言违规
```
assert a[i] <= a[i+1];
```
这个循环不变量可能不会被循环维护。
```
invariant left <= storeIndex < right + 1
```

未能减少终止措施

qsort(a,left,storeIndex);

感谢@James Wilcox 的回答，我将代码重写为：

method qsort(a: array<int>,left: int,right: int)
requires left>=0 && right <= a.Length
ensures (exists p | left<=p<right :: (forall k: int :: left < k < p ==> a[k] <= a[p]) && (forall j: int :: p < j < right ==> a[j] >= a[p]))
modifies a
decreases right - left
{
  if (right > left)
  {
      var pivotValue: int := a[left];
      var t: int := a[left];
      a[left] := a[right-1];
      a[right-1] := t;
      var storeIndex: int := left;
      var i :int := left;
      while i < right - 1
        invariant left <= storeIndex < right
        invariant storeIndex <= i
        decreases right - i
      {
          if a[i] < pivotValue
          {
            t := a[storeIndex];
            a[storeIndex] := a[i];
            a[i] := t;
            storeIndex := storeIndex+1;
          }
          i := i+1;
      }
      t := a[right-1];
      a[right-1] := a[storeIndex];
      a[storeIndex] := t;
      qsort(a,left,storeIndex);
      qsort(a,storeIndex+1,right);
  }  
}
method Testing (a: array<int>)
  requires  a.Length > 0
  modifies a
{
    qsort(a,0,a.Length);
    var i :int := 0;
    while(i<a.Length-1)
      decreases a.Length - 1 - i
    {
      assert a[i] <= a[i+1];
      i := i+1;
    }    
}

但是 qsort 的后置条件可能不成立，我该如何纠正它？

我的最终验证码：

    method qsort(a: array<int>,left: int,right: int)
        requires 0<= left <= right <= a.Length
        requires  0 <= left <= right < a.Length ==> forall j:: left <= j < right ==> a[j] < a[right]
        requires  0 < left <= right <= a.Length ==> forall j:: left <= j < right ==> a[left-1] <= a[j]
        ensures forall j,k:: left <= j < k < right ==> a[j] <= a[k]
        ensures forall j:: (0<= j < left) || (right <= j < a.Length) ==> old(a[j])==a[j]
        ensures 0<= left <= right < a.Length ==> forall j:: left <= j < right ==> a[j] < a[right]
        ensures 0< left <= right <= a.Length ==> forall j:: left <= j < right ==> a[left-1] <= a[j]
        modifies a
        decreases right - left
    {
      if (right > left)
      {
          var pivot := left;
          var i :int := left + 1;
          while i < right
            invariant left <= pivot < i <= right
            invariant forall j::left <= j < pivot ==> a[j] < a[pivot]
            invariant forall j::pivot < j < i ==> a[pivot] <= a[j]
            invariant forall j::0 <= j < left || right <= j < a.Length ==> old(a[j])==a[j]
            invariant 0 <= left <= right < a.Length ==> forall j:: left <= j < right ==> a[j] < a[right]
            invariant 0 < left <= right <= a.Length ==> forall j:: left <= j < right ==> a[left-1] <= a[j]
            decreases right - i
          {
              if a[i] < a[pivot]
              {
                var count :=i -1;
                var tmp:=a[i];
                a[i] := a[count];
                while (count>pivot)
                  invariant a[pivot] > tmp
                  invariant forall j::left <= j < pivot ==> a[j]<a[pivot]
                  invariant forall j::pivot< j < i+1 ==> a[pivot]<=a[j]
                  invariant forall j::0<=j<left || right <= j <a.Length ==> old(a[j])==a[j]
                  invariant 0 <= left <= right < a.Length ==> forall j:: left <= j < right ==> a[j] < a[right]
                  invariant 0 < left <= right <= a.Length ==> forall j:: left <= j < right ==> a[left-1] <= a[j]
                  {
                    a[count+1]:=a[count];
                    count:=count-1;
                  }
            a[pivot+1]:=a[pivot];
            pivot:=pivot+1;
            a[pivot-1]:=tmp;
            }
              i := i+1;
          }
          qsort(a,left,pivot);
          qsort(a,pivot+1,right);
      }  
    }
    method Testing (a: array<int>)
      requires  a.Length > 0
      modifies a
    {
        qsort(a,0,a.Length);
        var i :int := 0;
        while(i<a.Length-1)
          decreases a.Length - 1 - i
        {
          assert a[i] <= a[i+1];
          i := i+1;
        }
    }

Answer 1

您的代码可能是正确的，但 Dafny 通常需要一些帮助才能证明它。

Dafny 只会根据其后置条件（ensures 子句）对方法调用进行推理。由于您的 qsort 方法没有后置条件，Dafny 会假设它可以做任何事情。这解释了为什么 Testing 方法无法证明断言。如果给qsort加上后置条件，那你就得证明了！那将是一个很好的练习！
Dafny 根据循环的不变量来解释循环。如果循环体修改的变量没有在循环不变量中提及，Dafny 假定它的值是任意的。如果 i 以某种方式小于 storeIndex，则关于 storeIndex 的不变量不成立。您可以通过向循环添加额外的不变量 storeIndex <= i 来解决此问题。那么两个不变量都会通过。
之前的修复也修复了终止问题。

为了更好地理解Dafny是如何使用pre/postconditions和循环不变量来分解验证问题的，建议阅读the guide。然后，您可以向 qsort 添加合适的后置条件，并尝试使用其他循环不变量来证明它。如果您遇到困难，请随时提出更多问题！

在你的第二个版本的代码中，后置条件似乎太弱了，因为 qsort 是一个 sorting 方法，似乎后置条件应该是数组是排序。（因为它是递归的，实际上后置条件应该只讨论 left 和 right 之间的数组区域。）如果你这样做，那么 Testing 中的断言应该通过。然后，您仍然需要做一些工作来证明 qsort 的后置条件，方法是向其中的 while 循环添加不变量。

我在 dafny 中的代码有什么问题？

What is the wrong with my code in dafny?

dafny