如何使用Dafny证明冒泡排序时间复杂度并设置循环不变式

核心问题回应 #

Dafny完全支持为单轮循环迭代设置专属不变式，你需要的交换次数上界可以通过补充两层循环的对应不变式实现，不需要额外特殊方法。

原有代码的问题 #

你当前写的不变式存在两个明显缺陷：

• 内层循环中old(i)、old(j)的用法错误：old关键字指向方法初始状态，无法获取外层循环当前轮次启动时的变量值。
• 约束i < 0 && j < 0 ==> 0 <= n <= a.Length永远不会触发：外层循环运行条件为i>0，内层循环启动时j=0，不可能出现i、j同时小于0的情况，没有实际约束效果。

补充不变式的实现思路 #

我们可以通过两层不变式的配合完成上界证明：

1. 外层循环不变式：约束截至当前外层迭代，已发生的交换次数不超过「总最大交换量 - 剩余迭代最多可产生的交换量」。总最大交换量为a.Length*(a.Length-1)/2，剩余i轮迭代最多可产生i*(i+1)/2次交换（对应i + (i-1) + ... + 1的求和结果），因此不变式为：

   invariant n <= (a.Length * (a.Length - 1)) / 2 - (i * (i + 1)) / 2
   

   当外层循环结束i=0时，该式直接退化为n <= (a.Length * (a.Length - 1)) / 2，刚好匹配后置条件。
2. 内层循环不变式：约束单轮内层循环的交换次数上限。首先在外层循环内部、内层循环启动前保存当前的n值，再给内层加不变式：当前总n不超过进入内层前的n值加j（每轮内层迭代最多发生1次交换，到j位置时最多新增j次交换），即：

   invariant n <= inner_old_n + j
   

修改后的完整代码 #

method BubbleSort(a: array<int>) returns (n: nat) 
  modifies a
  requires a != null
  ensures n <= (a.Length * (a.Length - 1))/2
{
  var i := a.Length - 1;
  n := 0;
  while (i > 0)
    invariant 0 < a.Length ==> 0 <= i < a.Length;
    invariant n <= (a.Length * (a.Length - 1)) / 2 - (i * (i + 1)) / 2;
    decreases i;
  {
    var inner_old_n := n; // 保存进入内层前的n值
    var j := 0;
    while (j < i)
      invariant n <= inner_old_n + j; // 单轮内层交换次数不超过j
      decreases i - j;
    {
      if(a[j] > a[j+1])
      {
        a[j], a[j+1] := a[j+1], a[j];
        n := n + 1;
      }
      j := j + 1;
    }
    i := i -1;
  }
}

上述代码可以直接通过Dafny的验证，满足你要求的交换次数上界证明。

额外说明 #

如果你需要同时证明冒泡排序的排序正确性，还需要补充两类不变式：

• 外层循环不变式：数组下标i+1到a.Length-1的元素已经有序且为全局最大的对应个数元素
• 内层循环不变式：数组下标j位置的元素是前j+1个元素中的最大值

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