我在 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);
      }  
    }

错误是：

1. 断言违反

   assert a[i] <= a[i+1];
   

2. 这个循环不变量可能不会由循环维护。

   invariant left <= storeIndex < right + 1
   

3. 未能减少终止措施

   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 通常需要一些帮助才能证明这一点。

1. Dafny 只会通过后置条件（ensures 子句）来推断方法调用。由于您的 qsort 方法没有后置条件，因此 Dafny 会假设它可以做任何事情。这解释了为什么Testing 方法无法证明断言。如果你给qsort添加一个后置条件，那么你必须证明它！这将是一个很好的练习！

2. Dafny 根据其不变量来解释循环。如果循环体修改的变量未在循环不变量中提及，则 Dafny 假定其值是任意的。如果不知何故，i 小于 storeIndex，则您关于 storeIndex 的不变量不正确。您可以通过在循环中添加额外的不变量 storeIndex <= i 来解决此问题。然后两个不变量都会通过。

3. 之前的修复也修复了终止问题。

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

---

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