new*_*gic 2 verification while-loop smt z3 z3py
考虑证明以下 while 循环的正确性，即我想表明，给定循环条件开始时，它最终将终止并导致最终断言为真。
int x = 0;
while(x>=0 && x<10){
x = x + 1;
}
assert x==10;
在不使用循环展开的情况下，用于检查正确性的 SMT-LIB 的正确翻译是什么？
这种陈述的典型证明将通过经典的霍尔逻辑来完成，我想您已经熟悉了。如果没有，请参阅： https: //en.wikipedia.org/wiki/Hoare_logic
这个想法是为你的循环提出一个不变量。这个不变量在循环开始之前必须为真，它必须由循环体维护，并且它必须暗示循环条件不再为真时的最终结果。此外，您还需要通过测量函数证明循环最终会终止。（稍后会详细介绍。）
您可以说服自己为什么这就足够了：不变量是“总是”正确的东西。如果它暗示了你的最终结果，那么你的证明就完成了。我上面概述的证明步骤确保不变量确实是不变量，即它的真实性始终由您的程序维护。
对于你的循环来说，什么是一个好的不变量？让我们给这个不变量命名为I。稍微思考一下，一个不错的选择I是：
I = x >= 0 && x <= 10
请注意，这与您的循环条件多么相似（但不完全相同！），这并非偶然。循环不变式并不是唯一的，想出一个好的循环不变式确实很困难。自动合成循环不变量是一个活跃的研究领域（自 60 年代以来）。看看那里有大量的研究。https://en.wikipedia.org/wiki/Loop_invariant是一个很好的起点。
现在我们“神奇地”提出了循环不变式，让我们使用 SMT 来证明它确实是正确的。我将使用 z3-python 接口作为足够接近的替代品，而不是编写 SMTLib（它很冗长并且主要仅适用于机器）。为了完成证明，我需要展示 4 件事：
让我们依次看一下。
由于我们将使用 z3 的 python 界面，因此我们必须做一些跑腿工作才能开始。这是我们需要的骨架：
I = x >= 0 && x <= 10
请注意，我们使用参数对循环条件 (C) 和不变量 (I) 进行参数化，因此可以轻松使用不同的参数调用它们。这是编程中的常见技巧，从数据中抽象出控制。这种编码方式将简化我们以后的生活。
这个很容易。就在循环之前，我们知道x = 0. 因此，我们需要询问 SMT 求解器是否x == 0蕴涵我们的不变量：
from z3 import *
def C(p):
return And(p >= 0, p < 10)
def I(p):
return And(p >= 0, p <= 10)
x = Int('x')
瞧！如果您想查看 SMTLib 以了解证明义务，您可以要求 z3 为您打印：
>>> print(Implies(x == 0, I(x)).sexpr())
(=> (= x 0) (and (>= x 0) (<= x 10)))
循环体仅在循环条件 ( C) 为真时运行。主体加x一。因此，我们需要证明的是，如果我们的不变式 ( I) 为真，如果循环条件 ( C) 为真，并且如果我加x一，则I保持为真。让我们直接问 z3：
>>> prove (Implies(x == 0, I(x)))
proved
几乎太容易了！
这次，我们需要要求求解器证明I成立时所需的结论，但C不证明：
>>> print(Implies(x == 0, I(x)).sexpr())
(=> (= x 0) (and (>= x 0) (<= x 10)))
现在我们已经完成了所谓的部分正确性主张。也就是说，如果循环终止，那么x确实会10结束。这就是你一开始想要证明的。
到目前为止我们所做的被称为部分正确性。它表示如果循环终止，则后置条件（即x == 10）成立。但它不保证循环总是终止。
为了获得完整的证明，我们必须证明终止。这是通过提出一个测量函数来完成的：测量函数是一种将（通常）数值分配给程序变量集的函数，该程序变量集从下往上界定。然后我们证明它在每次迭代中都会下降，并且初始值高于其下限。然后我们知道循环不能永远继续下去：度量必须在每次迭代中下降，但它不能这样做，因为它有下界。
终止证明通常比较困难，并且想出一个好的措施可能很棘手。但在这种情况下，很容易想出：
>>> prove(Implies(And(I(x), C(x)), I(x+1)))
proved
主张在这种情况下该度量始终是非负的。让我们证明在循环开始之前，即，当x == 0：
>>> prove(Implies(And(I(x), Not(C(x))), x == 10))
proved
它在每次迭代中都会下降：
def M(x):
return 10-x
最后，如果循环执行，结果总是为正：
>>> prove (Implies(x == 0, M(x) >= 0))
proved
现在我们知道循环将终止，因此我们的证明已经完成。
你可能想知道我是不是从帽子里变出了一只兔子。我们如何知道上述步骤是否足够？或者当我在你的程序上挥手并神奇地将其翻译为 z3-python 时，我在编码中没有犯错误？
对于第一个问题：已有研究表明，对于传统的命令式程序语义，霍尔逻辑风格的推理是合理的。这是一个很好的幻灯片：https://www.cl.cam.ac.uk/teaching/1617/HLog+ModC/slides/lecture2.pdf
对于第二个问题：这就是橡胶上路的地方。你必须将我的论点进行同行评审，可能使用已建立的定理证明者来对整个事情进行编码，并相信机械化是正确的。Why3 ( https://why3.lri.fr ) 是开始这种推理风格的良好平台。
这个证明最棘手的部分是提出正确的不变量。一个“好的”不变量不仅是正确的，而且可以让你证明你想要的结果。例如，考虑以下不变量：
>>> prove (Implies(C(x), M(x) > M(x+1)))
proved
这个不变量显然也适用于所有程序！但是，如果您尝试运行我们对此版本的证明I，您会发现它不会通过，并且您会得到一个反例。（这样做非常有启发性。）一般来说，您可以：
选择一个并非由您的程序真正强制执行的“不变量”，即它不会如上所述始终保持正确。希望您从求解器获得的反例将有助于确定问题所在。
或者，更有可能的是，您选择的不变量确实是程序的不变量，但它不足以证明您想要的结果。在这种情况下，反例的用处就不那么大了，而且对于复杂的程序来说，很难找出原因。
允许您证明最终结果的不变量称为“归纳不变量”。“改进”不变量以获得证明的过程称为“强化不变量”。所有这些主题都有大量的研究，特别是在模型检查领域。Bradley 的“Understanding IC3：” https://theory.stanford.edu/~arbrad/papers/Understanding_IC3.pdf是这些主题中值得阅读的一篇好论文。
这里概述的策略是“元”级证明：它相当于确定证明目标的纸质证明，并将其发送到 SMT 求解器（在本例中为 z3）以完成工作。这是现代证明中的常见做法，即提出子目标并使用自动求解器来实现它们。像 ACL2、Isabelle、Coq 等定理证明器在很大程度上机械化了“提出子目标”部分，确保整个证明对于一组可信（但通常非常小）的核心公理来说是合理的。（这就是所谓的 LCF 方法，请参阅https://www.cl.cam.ac.uk/~jrh13/slides/manchester-12sep01/slides.pdf了解一个不错的幻灯片。）
希望这是一个足够详细的答案，帮助您开始使用 SMT 求解器进行程序验证。也许这超出了你的要求；但经验法则是验证方面没有免费的午餐。这是很多工作！然而，随着自动定理证明器、SMT 求解器和许多人多年来构建的其他框架的进步，如今您已经非常接近按钮推理（至少对于某些类型的程序而言）。祝你好运，但请注意，经过近 7 年的研究，程序验证仍然是计算机科学的圣杯。事情总是会变得更好/更容易，但该领域还有很多工作要做。