Z3 或 Smt2 的 While 循环 [英] While loop for Z3 or Smt2

问题描述

如何将简单的while循环(c-代码)转换为smt2语言或z3?例如:

How to convert a simple while loop(c- code) to smt2 language or z3? For ex :

int x,a;
while(x > 10 && x < 100){
    a = x + a;
    x++;
}

推荐答案

SMT 求解器的输入语言是一阶逻辑(带有理论)，因此没有循环等计算操作的概念.

The input language to an SMT solver is first-order logic (with theories) and as such has no notion of computational operations such as loops.

你可以

• 要么使用循环不变式对任意循环迭代(以及循环的前后状态)进行编码，并证明与该任意迭代相关的属性，这就是演绎程序验证器，例如Boogie、Dafny 或 Viper 做

• either use a loop invariant to encode an arbitrary loop iteration (and the pre- and post-state of the loop) and prove your relevant properties with respect to that arbitrary iteration, which is what deductive program verifiers such as Boogie, Dafny or Viper do

或者，如果迭代次数是静态已知的，则展开循环并基本上使用单个静态赋值形式对不同的展开进行编码

or, if the number of iterations is statically known, you unroll the loop and basically use single static assignment form to encode the different unrollings

对于您的循环，后者将如下所示(这里没有使用正确的 SMT 语法，因为我很懒惰):

For your loop, the latter would look as follows (not using proper SMT syntax here because I'm lazy):

declare x0, a0 // initial values
declare a1, x1 // values after first unrolling
x0 > 10 && x0 < 100 ==> a1 == a0 + x0 && x1 == x0 + 1
declare a2, x2 // values after second unrolling
x1 > 10 && x1 < 100 ==> a2 == a1 + x1 && x2 == x1 + 1
...

这篇关于Z3 或 Smt2 的 While 循环的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！