正确的 Dafny 方法的 Z3 模型

Question

对于一个正确的方法，Z3能否找到方法验证条件的模型？

我原以为不是，但这是一个方法正确的例子

但验证找到了一个模型。

这是 Dafny 1.9.7。

Answer 1

Malte 所说的是正确的(我发现它的解释也很好)。

Dafny 是可靠的，因为它只会验证正确的程序。换句话说，如果一个程序不正确，Dafny 验证器永远不会说它是正确的。然而，潜在的决策问题通常是不可判定的。因此，难免会出现程序符合规范，而验证者仍然给出错误信息的情况。事实上，在这种情况下，验证者甚至可能会显示一个据称的反例。它可能是一个错误的反例(如上例所示)——它只是意味着，就验证者而言，这是一个反例。如果验证者只是多花一点时间，或者如果它足够聪明来展开更多的函数定义、应用归纳假设或做许多其他好事，则有可能确定反例是伪造的.因此，您收到的任何错误消息(包括可能伴随此类错误消息的任何反例)都应解释为可能错误(和可能反例)。

如果您尝试验证循环的正确性但没有提供足够强大的循环不变式，则经常会出现类似的情况。然后 Dafny 验证器可能会在进入循环时显示一些实际上永远不会出现的变量值。然后，反例试图让您了解如何适本地加强循环不变量。

最后，让我对 Malte 所说的话补充两点。

首先，这个例子中至少有另一个不完整的来源，即非线性算术。有时很难四处导航。

其次，可以简化使用函数Dummy 的技巧。提到 Pow 调用就足够了(至少在这个例子中)，例如:

lemma EvenPowerLemma(a: int, b: nat)
  requires Even(b)
  ensures Pow(a, b) == Pow(a*a, b/2)
{
  if b != 0 {
    var dummy := Pow(a, b - 2);
  }
}

不过，我更喜欢其他两个手动证明，因为它们在向用户解释证明是什么方面做得更好。

鲁斯坦