Z3 或 Smt2 的 While 循环答案

【问题标题】：While loop for Z3 or Smt2Z3 或 Smt2 的 While 循环
【发布时间】：2017-07-27 19:39:56
【问题描述】：

如何将简单的while循环（c-code）转换为smt2语言或z3？例如：

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

【问题讨论】：

标签： z3 smt

【解决方案1】：

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

你可以

要么使用循环不变量对任意循环迭代（以及循环的前后状态）进行编码，并证明与该任意迭代相关的相关属性，这就是演绎程序验证器，例如Boogie、Dafny 或 Viper 都可以
或者，如果迭代次数是静态已知的，则展开循环并基本上使用单个静态赋值形式来编码不同的展开

对于您的循环，后者如下所示（此处未使用正确的 SMT 语法，因为我很懒）：

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
...

【讨论】：