循环不维护 Dafny 循环不变量

Question

我的任务是初始化一个 8x8 矩阵并确保矩阵内的所有元素都设置为零。我还需要使用 while 循环和循环不变量来实现。我的实现如下所示：

method initMatrix(a: array2<int>)
    modifies a
    // require an 8 x 8 matrix
    requires a.Length0 == 8 && a.Length1 == 8
    // Ensures that all rows in the matrix are zeroes
    ensures forall row, col :: 0 <= row < a.Length0 && 0 <= col < a.Length1 ==> a[row, col] == 0
{
  var row : nat := 0;
  while(row < a.Length0)
    invariant 0 <= row <= a.Length0
    invariant forall i,j :: 0 <= i < row && 0 <= j < a.Length1 ==> a[i,j] == 0
  {
    var col : nat := 0;
    while(col < a.Length1)
      invariant 0 <= row <= a.Length0
      invariant 0 <= col <= a.Length1
      invariant forall i,j :: i == row && 0 <= j < col ==> a[i,j] == 0
    {
        a[row, col] := 0;
        col := col + 1;
    }
    row := row + 1;
  }
}

从逻辑上讲，我认为我所有的量词都是正确的。但是，Dafny 认为我的循环在外部 while 循环中是不变的

invariant forall i,j :: 0 <= i < row && 0 <= j < a.Length1 ==> a[i,j] == 0

没有被循环维护。

我首先怀疑我的实现中存在问题。所以我首先在没有任何前置条件和后置条件的情况下运行该方法并打印数组中的所有元素；输出是一个充满零的矩阵。

为了更加确定它正在替换所有元素，而不仅仅是使用矩阵实例化时的零，我将矩阵中的所有元素初始化为 1 并打印出其中的所有值。结果是一样的——矩阵中的所有元素都是 1。

从这个实验中，我可以得出结论，问题不存在于我的实现中，而是我定义规范的方式。

我手动浏览了我的算法，发现它在逻辑上应该可以工作，但是，我认为我对量词如何在 Dafny 中的循环不变量中工作的理解可能存在偏差。

当条件0 <= i < row && 0 <= j < a.Length1 为假时，究竟发生了什么？在第一次迭代中，变量row 等于0，不满足条件0 <= i < row。它是遍历第一行并检查该行中的所有元素是否为零还是跳过它？

现在，当它在初始迭代中到达语句 row := row + 1; 时会发生什么？循环不变量invariant forall i,j :: 0 <= i < row && 0 <= j < a.Length1 ==> a[i,j] == 0 在进入时使用row 的值（为零）还是使用row (1) 的递增值？

Answer 1

原因是你的内循环的不变量不够强。它只讨论了i == row 的情况，而没有说明你已经为i < row 完成了什么。

由于循环不变量的工作方式，Dafny 基本上“忘记”了这些信息，因为您不会在内部循环不变量中“记住”它。

你可以通过加强内循环不变量来修复你的程序来谈论i < row。例如如下：

invariant 
  forall i,j :: 
    ((0 <= i < row && 0 <= j < a.Length1) || (i == row && 0 <= j < col)) ==> 
    a[i,j] == 0

这表示a 在这些行的所有列中row 之前的所有先前行中为零，在row 中也是如此，但随后仅在列col 中为零。

---

让我也借此机会解决您在描述调试过程时提出的其他几个问题。

当条件0 <= i < row && 0 <= j < a.Length1 为假时，究竟发生了什么？第一次迭代，变量row等于0，不满足条件0 <= i < row。它是遍历第一行并检查该行中的所有元素是否为零还是跳过它？

它“跳过它”。如果某个公式A 为假，那么A ==> B 为真，甚至不用看B。

现在，当它在初始迭代中到达语句 row := row + 1; 时会发生什么？循环不变量不变量forall i,j :: 0 <= i < row && 0 <= j < a.Length1 ==> a[i,j] == 0 在进入时使用row 的值（为零）还是使用row 的递增值（1）？

循环不变量必须在每个循环的顶部为真。当您第一次进入循环时（甚至在评估分支条件之前）它必须为真。另外，在每次执行body之后，它必须是真的。

换句话说，它使用row的递增值（循环体第一次执行后为1）。

---

最后让我更一般地评论一下循环不变量以及如何调试它们。

首先，让我介绍一下詹姆斯的达夫尼验证第一定律（我刚刚编造的）：

Just because Dafny reports a verification error doesn't mean the program is wrong.

Dafny 的错误信息（大部分）通过使用“可能不成立”之类的短语来提醒您这条法则，例如

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

确实，您的示例程序实际上是正确的，正如您通过实际运行它所证明的那样。运行时，它按预期打印全零。然而，Dafny 仍然报错。

这是我们为解决程序验证等无法确定的问题而付出的代价。使用 Dafny 时，您的工作是说服它您的程序是正确的。当 Dafny 报告错误时，仅表明 Dafny 尚未被说服。

现在，回到循环不变量。为什么达芙妮不信服？ Dafny 验证了关于循环不变量的三件事。

1. 循环之前的前提条件意味着循环不变量（即循环不变量在入口处成立）。
2. 循环不变量由主体保留。
3. 循环不变量意味着循环之后的后置条件。

困难的通常是#2。如果您不习惯编程验证，Dafny 会以一种奇怪且不直观的方式检查 #2。 Dafny 试图证明，从满足循环不变量的 任意 状态使得循环的分支条件为真，如果您随后执行循环的一次迭代，则循环不变量仍然成立。

这里的关键是任意。它确实不检查“在程序执行期间可能实际发生的状态开始的循环的每次迭代都保留循环不变性”。不会。它会检查从 任意 状态开始的执行是否保持循环不变。

回到您的示例程序，您有一个双重嵌套循环。 Dafny 说，它不相信外循环的其中一个不变量被外循环体的执行所保留。什么是外循环体？这是执行内部循环的一堆迭代吗？ Dafny 如何解释内循环？仅通过其循环不变量。

因此，当证明#2 关于外循环时，内循环的后置条件是它需要重新建立外循环不变量，请注意，这说明了直到row 的所有行。然后，Dafny 试图证明这一点，假设 only 内部循环不变量（以及循环分支条件的否定），它只讨论行row。由于状态不受约束，我们可以看到为什么 Dafny 不相信。