美好的一天,自动扣款和验证黑客!
为了更深入地了解WhyML 究竟如何为 ACSL 注释的 C 程序提供证明,我试图手动“重现”Why3 对 WhyML 程序所做的工作,同时将其转换为 SMT 逻辑并将其输入 Z3 证明程序。
假设我们有以下 C 片段:
const int L = 3;
int a[L] = {0};
int i = 0;
while (i < L) {
a[i] = i;
i++;
}
assert (a[1] == 1);
我正在尝试将其编码为 SMT 逻辑,如下所示:
(set-logic AUFNIRA)
(define-sort _array () (Array Int Int))
(declare-const ar _array)
(declare-fun set_a_i (_array Int Int) _array)
(assert (forall ((ar0 _array) (i Int) (j Int))
(ite (< i j)
(= (set_a_i ar0 i j)
(set_a_i (store ar0 i i) (+ i 1) j))
(= (set_a_i ar0 i i) ar0) )))
(assert (= (select (set_a_i ar 0 3) 1) 1))
(check-sat)
Z3 给出“未知”。
这可能是因为在指定 set_a_i 函数时使用了量化。但我看不到其他方法来指定它。
我知道以下陈述:
- SMT 求解器通常不能(或以不好的方式)处理数组上的量化。
- 如果我提供前后条件和循环不变量,WhyML 能够证明这样的程序。
- 即使后端设置为 Z3,WhyML 也能够证明此类程序,因此 SMT 求解器本身不是问题。
- WhyML 可以生成 z3 smt 文件,但要理解它是一件很辛苦的事情,部分原因是由于 whyML->smt 翻译的自动性质(例如,它不保留变量名)
我阅读了几乎所有为 WhyML、Frama-C WP 插件和 Z3 提供的材料。我还阅读了几篇关于验证 C 代码的论文,但没有发现任何关于 C --> SMT 翻译技术的文章。
我应该学习哪些材料来获得这种理解?您能否提供见解和/或链接到描述这种将命令式代码转换为多排序一阶逻辑的机制的论文。
我将不胜感激任何评论。谢谢!
祝你好运,叶夫根尼。