对于正确的方法，Z3能否找到该方法验证条件的模型？
我原以为不会，但这里有一个例子，该方法是正确的
但验证发现了一个模型。
这是 Dafny 1.9.7 的情况。
Malte 所说的是正确的（我发现它也得到了很好的解释）。
Dafny 是健全的，因为它只会验证正确的程序。换句话说，如果一个程序不正确，Dafny 验证者永远不会说它是正确的。然而，潜在的决策问题通常是不可判定的。因此，不可避免地会出现程序满足其规范而验证者仍然给出错误消息的情况。事实上，在这种情况下，验证者甚至可能会显示据称反例。它可能是一个错误的反例（如上例所示）——它只是意味着，据验证者所知，这是一个反例。如果验证者只是多花一点时间，或者足够聪明，展开更多函数定义，应用归纳假设，或者做许多其他好事，那么就有可能确定反例是假的。因此，您收到的任何错误消息（包括可能伴随此类错误消息的任何反例）都应解释为possible错误（和possible反例）。
如果您尝试验证循环的正确性并且没有提供足够强大的循环不变量，则经常会发生类似的情况。然后，Dafny 验证器可能会在进入循环时显示一些实际上永远不会出现的变量值。然后，反例试图让您了解如何适当地增强循环不变性。
最后，让我对马尔特所说的话补充两点。
首先，这个例子中至少还有另一个不完整性的来源，即非线性算术。有时可能很难导航。
二、函数的使用技巧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);
}
}
不过，我更喜欢其他两个手动证明，因为它们可以更好地向用户解释证明是什么。
Rustan
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
