是否有标准方法将命令式语言（比如C或Java）中的 for 循环的语义转换为SMT-LIB？我正在考虑将它们定义为SMT-LIB公理，但它似乎是临时的，我理解翻译并不总是由解算器说明z3 .
for
经典的"trick"是在一个边界内展开你的循环 . 这个想法源于硬件社区，其中有界证明更为常见 . 但它也适用于软件 . CBMC（https://www.cprover.org/cbmc/）是为C程序执行此操作的系统 . 显然，只有在unroll-number足够的情况下才会提供"proof" .
请注意，展开可能不实用，因为它可能导致代码爆炸，在这种情况下，您可以使用“未解释函数”技巧：即，您展开固定次数，然后抽象计算的其余部分 . 这可能导致误报，即解算器可能返回虚假模型 . 但是这个想法可以用在基于CEGAR（反例引导 - 抽象 - 细化）的系统中 .
通常，循环意味着不变量，并且涉及循环（或递归）的程序的证明需要确定那些不变量是什么并通过归纳证明它们 . SMT解决方案最好使用真正的定理证明器（Isabelle，HOL，HOL-Light，Coq，Agda，Lean;请选择） . 请注意，如今这些系统中的大多数都可以使用SMT求解器作为"oracle"来加速/发现子目标的样张，因此从这个意义上讲，您可以获得两全其美的效果 . 特别是，精益来自z3血统，绝对值得一试：https://leanprover.github.io/
不，没有标准的方法 . 关于循环的推理通常是不可判定的 . 处理循环是半科学，半艺术 .
如今处理循环的一种流行方式是通过Horn条款 . 这是一个很好的介绍：https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-yurifest.pdf
2 回答
经典的"trick"是在一个边界内展开你的循环 . 这个想法源于硬件社区，其中有界证明更为常见 . 但它也适用于软件 . CBMC（https://www.cprover.org/cbmc/）是为C程序执行此操作的系统 . 显然，只有在unroll-number足够的情况下才会提供"proof" .
请注意，展开可能不实用，因为它可能导致代码爆炸，在这种情况下，您可以使用“未解释函数”技巧：即，您展开固定次数，然后抽象计算的其余部分 . 这可能导致误报，即解算器可能返回虚假模型 . 但是这个想法可以用在基于CEGAR（反例引导 - 抽象 - 细化）的系统中 .
通常，循环意味着不变量，并且涉及循环（或递归）的程序的证明需要确定那些不变量是什么并通过归纳证明它们 . SMT解决方案最好使用真正的定理证明器（Isabelle，HOL，HOL-Light，Coq，Agda，Lean;请选择） . 请注意，如今这些系统中的大多数都可以使用SMT求解器作为"oracle"来加速/发现子目标的样张，因此从这个意义上讲，您可以获得两全其美的效果 . 特别是，精益来自z3血统，绝对值得一试：https://leanprover.github.io/
不，没有标准的方法 . 关于循环的推理通常是不可判定的 . 处理循环是半科学，半艺术 .
如今处理循环的一种流行方式是通过Horn条款 . 这是一个很好的介绍：https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-yurifest.pdf