如何在Dafny中对整数序列排序？遇类型转换与证明难题求助

核心方向：用数组做中间可变容器 #

序列的不可变性会导致原地排序操作（比如冒泡）的验证逻辑极度复杂，最优方案是先将序列转换为可变数组，利用Dafny中更易验证的数组排序实现完成排序，再转回序列。

1. 实现可验证的数组冒泡排序 #

先编写一个针对数组的冒泡排序方法，该方法的验证条件已经成熟，容易通过Dafny的验证：

method bubbleSort(arr: array<int>)
  modifies arr
  ensures multiset(arr[..]) == multiset(old(arr[..]))
  ensures forall i,j :: 0 <= i <= j < arr.Length ==> arr[i] <= arr[j]
{
  var n := arr.Length;
  var i := 0;
  while i < n
    invariant 0 <= i <= n
    invariant forall k :: n - i <= k < n ==> forall l :: k <= l < n ==> arr[k] <= arr[l]
    invariant multiset(arr[..]) == multiset(old(arr[..]))
  {
    var j := 0;
    while j < n - i - 1
      invariant 0 <= j <= n - i - 1
      invariant forall k :: n - i <= k < n ==> forall l :: k <= l < n ==> arr[k] <= arr[l]
      invariant multiset(arr[..]) == multiset(old(arr[..]))
      invariant forall l :: j <= l < n - i - 1 ==> arr[l] <= arr[l+1] || arr[l] == arr[l+1]
    {
      if arr[j] > arr[j+1] {
        arr[j], arr[j+1] := arr[j+1], arr[j];
      }
      j := j + 1;
    }
    i := i + 1;
  }
}

2. 封装序列排序方法 #

在目标sort方法中，完成序列转数组→数组排序→数组转序列的流程：

method sort(a: seq<int>) returns (r: seq<int>)
  ensures |a| == |r|
  ensures multiset(a) == multiset(r)
  ensures forall i,j :: 0 <= i <= j < |r| ==> r[i] <= r[j]
{
  // 初始化与原序列等长的数组
  var arr := new int[|a|];
  // 将序列元素拷贝到数组
  var k := 0;
  while k < |a|
    invariant 0 <= k <= |a|
    invariant arr[0..k] == a[0..k]
  {
    arr[k] := a[k];
    k := k + 1;
  }
  // 调用数组排序方法
  bubbleSort(arr);
  // 将排序后的数组转回序列
  r := arr[..];
}

3. 验证条件的自动满足逻辑 #

• 长度不变：数组长度与原序列完全一致，转回序列后|a| == |r|自然成立。
• 多重集相等：bubbleSort的ensures保证排序后数组的多重集与原数组一致，而原数组是原序列的完整拷贝，因此multiset(a) == multiset(r)成立。
• 非递减性：bubbleSort的ensures保证数组元素非递减，数组切片转序列后，自然满足forall i,j :: 0 <= i <= j < |r| ==> r[i] <= r[j]。

直接操作序列的替代方案（不推荐） #

若必须直接操作序列，可采用递归选择排序思路：每次提取剩余序列的最小值，拼接进结果，再递归处理剩余元素。但需要额外编写引理证明最小值的正确性、剩余序列的多重集关系，验证成本远高于数组中转方案。

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