嵌套循环中的索引越界错误

Question

有人能告诉我为什么这段代码会在 input[i*cols + j] 上生成 "index out of bounds" 错误吗？

method foo(input: array<int>, rows:int, cols:int)
requires input != null 
requires rows > 0 && cols > 0
requires rows * cols == input.Length
{
   var i := 0;
   while i < rows
   {
     var j := 0;
     while j < cols
     {
       var s := input[i*cols + j];
       j := j + 1;
     }
     i := i + 1;
   }
}

Answer 1

您的程序没有错误，但 Dafny 无法证明这一点。

为了证明索引在边界内，Dafny 需要证明：

i*cols + j < rows * cols

给定 i < rows 和 j < cols（并给出一些其他事实）。

这个公式是非线性的（意味着它包含两个变量的乘积）。一般来说，这样的公式不存在于可判定的逻辑片段中，在实践中，这意味着 Dafny 底层的求解器无法有效地推理它们。

现在，事实上，这个公式是正确的。只是求解器无法理解原因。我们可以通过将证明分解成更小的步骤来帮助解决这个问题。

这里是你的程序的完整版本，可以验证。

lemma lemma_mul_le(x: int, y: int, z: int)
  requires 0 <= z
  requires x <= y
  ensures x * z <= y * z
{}

method foo(input: array<int>, rows:int, cols:int)
  requires input != null 
  requires rows > 0 && cols > 0
  requires rows * cols == input.Length
{
   var i := 0;
   while i < rows
   {
     var j := 0;
     while j < cols
     {
       lemma_mul_le(i, rows-1, cols);
       var s := input[i*cols + j];
       j := j + 1;
     }
     i := i + 1;
   }
}

我引入了一个引理，它表示对于任何 x、y 和 z，如果 0 <= z 和 x <= y 则 x * z <= y * z。 Dafny 能够在没有任何进一步帮助的情况下证明这一点。（我们称之为 "proof by open-close brace"！）

然后我用 x、y 和 z 的一些特定值调用 foo 正文中的引理。我通过手动证明索引在边界内来选择这些值。

Dafny 能够验证引理是否正确，以及在给定引理的情况下，访问是在边界内的。这导致程序没有错误。万岁！

有人会疑惑：为什么Dafny可以在没有任何帮助的情况下证明引理，却无法证明原程序？

这是一件值得怀疑的事情。这些奇迹是人们为自动验证付出的代价。通常，可能有多种等效的方式来制定逻辑查询，这些方式从求解器中获得截然不同的性能。诱使求解器执行您的命令是一门艺术。

在这个程序的特定情况下，一种思考方式是根据 Dafny 将发送给求解器的查询。为了验证 foo，Dafny 将向具有 "in scope" 所有相关变量和事实的求解器发送查询。当被要求证明一个看似简单的非线性算术查询时，这可能会导致求解器偏离轨道或以其他方式感到困惑。通过将有问题的公式分解为引理，我们实质上是通过消除推理 foo 时范围内的所有不相关事实，迫使求解器专注于困难的部分。在这种情况下，事实证明这足以让证明通过。在更困难的情况下，可能需要其他技巧。

嵌套循环中的索引越界错误

index out of bounds error in nested loop

dafny