z3 - 用于正确 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);
  }
}

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

鲁斯坦

Answer 2

Dafny 未能证明引理是由于两种可能的不完整性来源的组合：递归定义（此处Pow）和归纳。由于信息太少，证明实际上是失败的，即因为问题是欠约束的，这反过来解释了为什么可以找到反例。

就职

自动化归纳很困难，因为它需要计算归纳假设，而这并不总是可能的。但是，Dafny 有一些启发式方法来应用归纳（可能有效也可能无效），并且可以切换，如下面的代码所示：

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

在启发式关闭的情况下，您需要手动“调用”引理，即使用归纳假设（这里，仅在 的情况下b >= 2），以便通过证明。

在您的情况下，启发式已激活，但它们还不够“好”以完成证明。接下来我会解释为什么。

递归定义

通过展开它们来静态推理递归定义很容易导致无限下降，因为通常无法确定何时停止。因此，Dafny 默认只展开一次函数定义。在您的示例中，Pow仅展开一次的定义不足以使归纳启发式起作用，因为归纳假设必须应用于Pow(a, b-2)，它不会“出现”在证明中（因为展开一次只会让您到达Pow(a, b - 1)）。在证明中明确提及Pow(a, b-2)，即使是在其他没有意义的公式中，也会触发归纳启发式，但是：

function Dummy(a: int): bool
{ true }

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

该Dummy函数用于确保断言不提供超出语法的信息，包括Pow(a, b-2). 一个看起来不那么奇怪的断言是assert Pow(a, b) == a * a * Pow(a, b - 2).

计算证明

仅供参考：您还可以明确证明步骤并让 Dafny 检查它们：

lemma {:induction false} EvenPowerLemma_manual(a: int, b: nat)
  requires Even(b);
  ensures Pow(a, b) == Pow(a*a, b/2);
{
  if (b != 0) {
    calc {
         Pow(a, b);
      == a * Pow(a, b - 1);
      == a * a * Pow(a, b - 2);
      == {EvenPowerLemma_manual(a, b - 2);}
         a * a * Pow(a*a, (b-2)/2);
      == Pow(a*a, (b-2)/2 + 1);
      == Pow(a*a, b/2);
    }
  }
}