将循环语义翻译成SMT-LIB

Question

是否有标准方法将命令式语言(例如C或Java)中的for循环的语义转换为SMT？z3说:我想把它们定义为SMT-LIB公理，但它似乎是临时性的，而且我知道，翻译并不总是由求解者决定的。

Answer 1

经典的“技巧”是在一个范围内展开你的循环。这种想法起源于硬件社区，在那里，有界证明更常见。但它也适用于软件。CBMC (https://www.cprover.org/cbmc/)是一个用于C程序的系统。显然，这只会提供“证据”的情况下，未登记号码是足够的。

请注意，展开可能不实用，因为它可能导致代码爆炸，在这种情况下，您可以使用“未解释-函数”技巧:即，您展开固定次数，然后抽象对其余的计算。这可能导致假阳性，也就是说，求解者可以返回一个假模型.但是这一思想可以用于基于CEGAR的(counter-example-guided-abstraction-refinement)系统中。

一般来说，循环隐含不变量，而涉及循环(或递归)的程序的证明需要找出这些不变量是什么，并通过归纳法证明它们。SMT解算器不做归纳证明。对于这样的问题，最好使用一个真正的定理证明(伊莎贝尔，HOL，HOL，Coq，Agda，精益，你的选择)。请注意，这些系统中的大多数都可以使用SMT-解算器作为“先知”来加速/发现子目标的证明，因此在这个意义上，您可以从这两个世界中获得最佳效果。尤其是，精益来自于z3血统，绝对值得一看：https://leanprover.github.io/

Answer 2

不，没有标准的方法。关于循环的推理通常是无法判定的。处理循环是一半的科学，一半的艺术。

这些日子来处理循环的一种流行方法是通过霍恩条款。下面是一个很好的介绍：https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-yurifest.pdf