将循环语义转换为 SMT-LIB [英] translating loop semantics to SMT-LIB

问题描述

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

Are there standard approaches to translate the semantics of for loops in imperative languages (say C or Java) to SMT-LIB? I was thinking of defining them as SMT-LIB axioms but it seems ad-hoc, and I understand that the translation will not always be decidable by solvers say z3.

推荐答案

经典的技巧"是在边界内展开循环.这个想法源于硬件社区，在那里有界证明更为常见.但它也适用于软件.CBMC (https://www.cprover.org/cbmc/) 是一个执行此操作的系统对于 C 程序.显然，这只会为 unroll-number 足够的情况提供证据".

The classic "trick" is to unroll your loops within a bound. This idea originates from the hardware community where bounded-proofs are much more common. But it also applies to software. CBMC (https://www.cprover.org/cbmc/) is a system that does this for C programs. Obviously this'll only provide "proof" for cases the unroll-number is sufficient.

请注意，展开可能不切实际，因为它可能导致代码爆炸，在这种情况下，您可以使用未解释函数"技巧:即，展开固定次数，然后对剩余的部分进行抽象计算.这可能会导致误报，即求解器可能会返回虚假模型.但是这个想法可以用在基于 CEGAR(反例引导抽象细化)的系统中.

Note that unrolling may not be practical as it can lead to code-explosion, in such cases, you can use the "uninterpreted-function" trick: i.e., you unroll a fixed number of times and then abstract over the remainder of the computation. This can lead to false-positives, i.e., the solver can return a bogus model. But this idea can be used in a CEGAR (counter-example-guided-abstraction-refinement) based system.

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

In general, loops imply invariants, and proofs for programs involving loops (or recursion) require figuring out what those invariants are and proving them by induction. SMT solvers don't do inductive proofs. For such problems, it's best to use a genuine theorem prover (Isabelle, HOL, HOL-Light, Coq, Agda, Lean; take your pick). Note that most of these systems these days can use an SMT-solver as an "oracle" to speed-up/discover proofs for subgoals, so in that sense, you get the best of both worlds. In particular, Lean comes from the z3 lineage and is definitely worth checking out: https://leanprover.github.io/

这篇关于将循环语义转换为 SMT-LIB的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！