z3 - 将循环语义转换为 SMT-LIB

Question

for是否有标准方法可以将命令式语言（例如 C 或 Java）中的循环语义转换为 SMT-LIB？我正在考虑将它们定义为 SMT-LIB 公理，但它似乎是临时的，而且我知道翻译并不总是可以由解算器决定，比如 z3。

标签： z3smt

Answer 1

经典的“技巧”是在一定范围内展开循环。这个想法源于有界证明更为普遍的硬件社区。但它也适用于软件。CBMC ( https://www.cprover.org/cbmc/ ) 是一个为 C 程序执行此操作的系统。显然，这只会为展开数量足够的情况提供“证明”。

请注意，展开可能不实用，因为它可能导致代码爆炸，在这种情况下，您可以使用“未解释函数”技巧：即，您展开固定次数，然后对剩余的计算进行抽象。这可能导致误报，即求解器可能返回虚假模型。但是这个想法可以用在基于 CEGAR（counter-example-guided-abstraction-refinement）的系统中。

一般来说，循环意味着不变量，涉及循环（或递归）的程序的证明需要弄清楚这些不变量是什么并通过归纳来证明它们。SMT 求解器不进行归纳证明。对于此类问题，最好使用真正的定理证明器（Isabelle、HOL、HOL-Light、Coq、Agda、Lean；任君选择）。请注意，如今这些系统中的大多数都可以使用 SMT 求解器作为“预言机”来加速/发现子目标的证明，因此从这个意义上说，您可以两全其美。特别是，精益来自 z3 血统，绝对值得一试：https ://leanprover.github.io/