Dafny实现快速排序的验证错误求助

1. 解决Partition方法的数组访问越界问题 #

你添加的requires lower <= upper <= arr.Length存在逻辑漏洞——Dafny数组采用0索引，最大合法访问索引是arr.Length - 1，若upper == arr.Length，访问arr[upper]必然触发越界。

具体修复： #

• 调整前置条件：将约束改为requires 0 <= lower <= upper < arr.Length，直接限定upper在合法索引范围内。
• 为Partition的循环添加不变式（invariant），让验证器确认所有数组访问的索引始终合法。以标准双指针实现为例：

  method partition(arr: array<int>, lower: int, upper: int) returns (j: int)
    requires 0 <= lower <= upper < arr.Length
    modifies arr
    ensures lower <= j <= upper
  {
    var pivot := arr[upper];
    var i := lower - 1;
    var curr := lower;
    while curr <= upper
      invariant lower - 1 <= i <= upper
      invariant lower <= curr <= upper + 1
      invariant forall k :: lower <= k <= i ==> arr[k] <= pivot
      invariant forall k :: i < k < curr ==> arr[k] > pivot
    {
      if arr[curr] <= pivot {
        i := i + 1;
        swap(arr, i, curr);
      }
      curr := curr + 1;
    }
    swap(arr, i + 1, upper);
    return i + 1;
  }
  

  其中invariant lower <= curr <= upper + 1确保循环中arr[curr]的访问不会超过upper（循环条件限制curr最大为upper），i的范围约束也保证了交换操作的索引合法性。

2. 解决Quicksort递归终止验证错误 #

递归终止的核心是证明：每次递归调用的decreases表达式严格递减，且存在下界0。

具体修复： #

• 为Quicksort方法指定decreases upper - lower：该表达式代表当前排序区间的长度差值，当区间长度为0（upper < lower）时递归自动终止。
• 利用Partition的后置条件ensures lower <= j <= upper，确保递归调用的区间严格小于原区间——因为Partition会将pivot放到正确位置，j必然满足lower <= j < upper，因此递归调用quicksort(arr, lower, j-1)和quicksort(arr, j+1, upper)的upper - lower值会严格小于原调用值。
• 补充Quicksort的前置条件约束区间合法性：

  method quicksort(arr: array<int>, lower: int, upper: int)
    requires 0 <= lower <= upper < arr.Length
    modifies arr
    decreases upper - lower
    ensures is_sorted(arr, lower, upper)
  {
    if lower < upper {
      var j := partition(arr, lower, upper);
      // 若验证器仍存疑，可手动添加断言辅助证明
      assert j < upper;
      quicksort(arr, lower, j - 1);
      quicksort(arr, j + 1, upper);
    }
  }
  

关键证明逻辑： #

• 当lower < upper时，upper - lower >= 1，递归调用的区间差值(j-1)-lower和upper-(j+1)均小于原差值upper-lower，满足严格递减要求。
• 当lower >= upper时，递归分支不执行，自然终止。

内容的提问来源于stack exchange，提问作者doomedCoder