如何使用 dafny 证明冒泡排序的时间复杂度？

Question

dafny 中有没有办法创建特定于单个循环迭代的不变量？下面我试图创建一个愚蠢的程序来限制冒泡排序的交换次数。该值存储在变量 n 中。所以我想将 n 上限设为 (a.Length * (a.Length - 1))/2。原因是可能发生的最大交换次数是，如果数组的顺序相反，那么内部循环的第一次迭代必须有 n 次交换，然后内部循环的第二次迭代必须有 n-1 次交换循环等，直到数组排序完毕。这相当于 1+2+3+...+n-1+n = n(n-1)/2，这正是我要展示的。我想知道 dafny 中是否有一种方法可以根据内部循环的迭代来限制下面代码中 i-j 或 n 的值。有这样的方法吗？

如果没有，是否有另一种方法可以根据上面提供的解释来上限此 n 值？也许我没有想到其他不变量？

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;
          decreases i;
           {
            var j := 0;
            while (j < i)
            invariant i - j <= old(i) - old(j);
            invariant i < 0 && j < 0 ==> 0 <= n <= a.Length;
            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;
          }
    }

Answer 1

这是一种方法。首先，我们介绍两个辅助函数。 NChoose2 只是为了方便 n * (n - 1) / 2 的包装。 SumRange(lo, hi)是从lo（含）到hi（不含）的整数之和。我们将需要下面的 SumRange 来表达一些循环不变量。

function NChoose2(n: int): int
{
  n * (n - 1) / 2
}

// sum of all integers in the range [lo, hi)
// (inclusive of lo, exclusive of hi)
function SumRange(lo: int, hi: int): int
  decreases hi - lo
{
  if lo >= hi then 0
  else SumRange(lo, hi - 1) + hi - 1
}

这是 BubbleSort 的新注释版本。

method BubbleSort(a: array<int>) returns (n: nat) 
  modifies a
  ensures n <= NChoose2(a.Length)
{
  // it simplifies the remaining invariants to handle the empty array here
  if a.Length == 0 { return 0; }  

  var i := a.Length - 1;
  n := 0;

  while i > 0
    invariant 0 <= i < a.Length
    invariant n <= SumRange(i+1, a.Length)
  {
    var j := 0;
    while j < i
      invariant n <= SumRange(i+1, a.Length) + j
      invariant j <= i
    {
      if a[j] > a[j+1]
      {
        a[j], a[j+1] := a[j+1], a[j];
        n := n + 1;
      }
      j := j + 1;
    }

    assert n <= SumRange(i, a.Length) by {
      SumRangeUnrollLeft(i, a.Length);  // see lemma below
    }

    i := i - 1;
  }

  calc <= {
    n;  // less or equal to next line by the loop invariant
    SumRange(1, a.Length);
    { SumRangeNChoose2(a.Length); }  // see lemma below
    NChoose2(a.Length);
  }
}

更改摘要：

（无关紧要）根据 NChoose2.
（无关紧要但简化）立即处理空数组的特殊情况，并与循环分开。
外层循环的循环不变量是 SumRange，而不是 NChoose2。如果你考虑一下你对参数的非正式描述，外循环的第一次迭代最多贡献 a.Length - 1 次交换；第二次迭代 a.Length - 2 次交换，等等。所以要汇总到目前为止的交换次数，它是 (a.Length - 1) + ... + (i + 1)。这正是 SumRange(i+1, a.Length).
内部循环的循环不变量只是说到目前为止，内部循环最多进行了 j 次额外交换。
要从内循环不变量重新建立外循环不变量，需要证明SumRange(i+1, a.Length) + i == SumRange(i, a.Length)。这是由引理 SumRangeUnrollLeft 处理的，它通过归纳法自动证明。
要从外循环不变量建立后置条件，我们需要证明SumRange(1, a.Length) == NChoose2(a.Length)。这是由引理 SumRangeNChoose2 处理的，它也可以通过归纳法自动证明。

这里是确切的引理陈述和证明。请注意，SumRangeUnrollLeft 的 decreases 子句是必需的，因为默认的推断子句始终是词典顺序。

// dafny proves this automatically by induction
lemma SumRangeNChoose2(n: nat)
  ensures SumRange(0, n) == NChoose2(n)
{}

// dafny proves this automatically by induction
// (given the correct decreases clause)
lemma SumRangeUnrollLeft(lo: int, hi: int)
  decreases hi - lo
  ensures SumRange(lo, hi) ==
          if lo >= hi then 0 else lo + SumRange(lo + 1, hi)
{}

如何使用 dafny 证明冒泡排序的时间复杂度？

How to prove time complexity of bubble sort using dafny?

proof

bubble-sort

time-complexity

dafny