将WhyML映射到SMT逻辑的确切机制-Java 学习之路

美好的一天，自动扣除和验证黑客！

为了更深入地了解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翻译技术的论文 .

我应该学习哪些材料才能获得这种理解？您能否提供一些见解和/或链接到描述将命令式代码转换为多排序一阶逻辑的机制的论文 .

我将不胜感激 . 谢谢！

祝你好运，Evgeniy .

1 回答

3
WP 0.8 plugin manual和论文“Why3: Shepherd Your Herd of Provers”提供了如何将带注释的C代码转换为为什么逻辑的高级概述，以及如何将为什么逻辑转换为定理证明器的输入逻辑 .

如WP插件手册第1.3节所述，首先考虑Hoare的三元组：

stmt

读取：每当前提条件P保持，然后运行stmt后，后置条件Q保持 . WP插件将最弱的前提条件视为对stmt的函数和后置条件，使得以下Hoare三元组成为：

{wp（stmt，Q）} stmt

在某种意义上，最弱的前提条件是在执行stmt之前必须保持的最简单的属性，使得在执行stmt之后Q保持 .

例如，考虑stmt为 x = x + 1 且为{x> 0}的情况 . 根据Hoare演算的赋值规则，我们知道{x 1> 0} x = x + 1 {x> 0}成立 . 事实上，{x 1> 0}是 x = x + 1 和{x> 0}的最弱前提 .

更一般地，可以确定任何语句和任何后置条件的最弱前提条件 .

现在假设你有一个带有前置条件P和后置条件Q的函数f：

f

定义W = wp（f，Q） . 我们根据wp的定义知道以下Hoare三元组：

f

如果我们能够证明P⇒W（这是提交给定理证明者的那个），则 Build f的属性P和Q的有效性 .

WP插件生成为什么逻辑 . 正如“Why3：Shepherd Your Herd of Provers”一文中的第4节所述，Why3的操作被描述为处理证明任务，这是一系列以目标结束的声明 . 这就是为什么逻辑被转换为特定定理证明器的输入逻辑 .

对于一个具体的例子，本文概述了将为什么逻辑转换为Z3 . 不仅输入语言不同（Z3使用SMT-LIB2语法），在Why和Z3的逻辑上存在显着差异 . 本文给出了Z3不支持多态性或归纳谓词的例子 .

为了将逻辑转换为定理证明器的输入逻辑，Why3使用一系列转换，逐步将Why逻辑转换为目标输入逻辑 . Why3使用称为驱动程序的配置文件来定义所有转换，一个输出证明器本机输入格式的漂亮打印机，以及用于解释证明器输出的正则表达式 .

假设您已运行 why3config ，您可以查看主目录中自动生成的 .why3.conf 配置文件，以确定Why3用于特定证明器的驱动程序 . 例如，在我的系统上，当使用Z3时，Why3使用 ~/.opam/system/share/why3/drivers/z3_432.drv . z3_432.drv 将 smt-libv2.drv 驱动程序作为SMT-LIB2兼容校准器的基本驱动程序导入 .

我知道你知道检查生成的SMT2，但我想我会提到如何为感兴趣的人做这个 . 如果将 -wp-out DIR 和 -wp-proof-trace 选项传递给 frama-c ，则WP将保存输出，以便在各个属性上运行证明器 . 然后，您可以找到感兴趣的属性的相应 .err 文件 . 就我而言，它是 main_assert_final_a_Why3_z3.err . 在文本编辑器中打开该文件，您将看到如下内容：
```
Call_provers: command is: /Users/dtrebbien/.opam/system/lib/why3/why3-cpulimit
  10 1000 -s z3 -smt2 sat.random_seed=42 nlsat.randomize=false
  smt.random_seed=42
  /var/folders/1v/2nkqhkgx0qnfwd75h0p3fcsc0000gn/T/why_9f8a52_main_Why3_ide-T-WP.smt2
```
这个 .smt2 文件包含对Why3的Z3的SMT-LIB2输入产生 .

如果您愿意，可以运行该命令 . 就我而言，我看到：
```
WARNING: pattern does contain any variable.
WARNING: pattern does contain any variable.
WARNING: pattern does contain any variable.
WARNING: pattern does contain any variable.
unsat
why3cpulimit time : 0.020000 s
```
虽然略有违反直觉，但 unsat 表示该 property 的有效性已确立 .
回复于 2024-05-03T19:41:46+08:00

将WhyML映射到SMT逻辑的确切机制

1 回答

相关问题