1

有人能告诉我为什么这段代码会生成“索引越界”错误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;
   }
}
4

1 回答 1

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, and z, if 0 <= zand x <= ythen x * z <= y * z。Dafny 无需任何进一步的帮助即可证明这一点。（我们称之为“开闭大括号证明”！）

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

Dafny 能够验证引理是真的，并且在给定引理的情况下，访问是有界的。这导致程序没有错误。万岁！

有人可能会想：Dafny 怎么能在没有任何帮助的情况下证明引理，却不能证明原程序呢？

这是一个合理的问题。这些奇迹是人们为自动验证付出的代价。一般来说，可能有多种等效的方式来制定逻辑查询，这些方式与求解器的性能大相径庭。有一种艺术可以诱使求解器按照您的意愿行事。

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

于 2017-07-28T23:57:12.070 回答