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

Question

有人可以告诉我为什么这段代码会在input[i*cols + j]上生成"索引越界"错误吗？

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能够在没有任何进一步帮助的情况下证明这一点。(我们称之为"开-闭大括号证明"！

然后，我将foo体中的引理称为x、y和z的一些特定值。我通过手动证明索引在边界内来选择这些值。

Dafny 能够验证引理是否为真，并且给定引理，访问是否在边界内。这将导致程序没有错误。万岁！

---

有人可能会问：为什么Dafny能够在没有任何帮助的情况下证明引理，但它不能证明原始程序？

这是一件值得怀疑的事情。这样的奇迹是自动验证所付出的代价。通常，可能有多种等效的逻辑查询公式，这些方法的性能与求解器大不相同。哄骗求解者听从你的命令是一门艺术。

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