验证条件生成 | Codeboy's Blog

形式陈述

固定一种有明确操作语义的顺序命令语言。对命令 $C$ 和期望后置条件 $Q$ ，验证条件生成器返回

\operatorname{vcgen}(C,Q)=(P,\mathcal V),

其中 $P$ 是执行 $C$ 前需要建立的入口断言， $\mathcal V$ 是有限个待证公式。它的部分正确性可靠性定理应写成：若 $P_0\Rightarrow P$ 与 $\mathcal V$ 中每个公式在断言语义下都有效，则 Hoare 三元组 $\{P_0\}\,C\,\{Q\}$ 对所有终止执行有效。这个定理量化的是程序运行，不是“求解器没有找到反例”。

无循环片段可沿最弱自由前置条件逆向计算。赋值返回 $(Q[E/x],\varnothing)$ ；顺序 $C_1;C_2$ 先处理 $C_2$ ，再把得到的入口条件交给 $C_1$ ；条件分支若分别得到 $P_t,P_f$ ，入口为

(B\Rightarrow P_t)\land(\neg B\Rightarrow P_f).

对注解循环 while B invariant I do D，先求 $\operatorname{vcgen}(D,I)=(P_D,\mathcal V_D)$ ，再返回入口 $I$ ，并加入

I\land B\Rightarrow P_D, \qquad I\land\neg B\Rightarrow Q.

这正是循环不变式 Hoare 规则的有限证明义务； $\mathcal V_D$ 也必须保留。

直觉

生成器像一名沿控制流逆行的审稿人。它从“最终必须满足什么”出发，逐条询问前一条命令要提供什么；走到分叉处便分别审查两条路径，走到循环回边则用程序员给出的不变式封住无限展开。产物不是另一个程序，而是一组可以交给人、SMT 求解器或证明助理检查的纯逻辑问题。

循环说明了生成与求解的分工。不变式太弱时，退出公式推不出后置；太强时，初始化或保持公式失败。生成器可以忠实暴露这种失败，却不能仅凭语法凭空发现最合适的不变式。即使所有公式都被证明，仍须有一次关于生成算法的结构归纳，说明每条规则确实覆盖语言语义中的全部路径。

例子与边界

在数学整数语义下考虑

text

i := 0
while i < n invariant 0 <= i and i <= n do
    i := i + 1

目标后置为 $i=n$ ，调用者承诺 $n\ge 0$ 。生成器产生三项核心义务：初始化

n\ge0\Rightarrow 0\le0\le n,

保持

0\le i\le n\land i<n \Rightarrow 0\le i+1\le n,

以及退出

0\le i\le n\land\neg(i<n)\Rightarrow i=n.

三者都可在整数线性算术中直接验证。若把更新改成 i := i + 2，状态 $i=n-1$ 满足保持式左侧，却使新值超过 $n$ ；模型给出的这个赋值是归纳义务反例，未必是一条从指定初态可达的真实故障，但足以否定当前不变式证明。

边界首先来自语言语义。除零、数组越界、异常、固定宽度溢出和未定义行为若可能发生，就必须生成相应安全或异常出口条件。break、continue 与过程调用也各有控制流边；漏掉一条边会得到看似漂亮却不可靠的公式集。这里的循环规则只证明部分正确性；总正确性还要生成循环体终止以及良基变式严格下降的义务。

推论与应用

验证条件把程序验证拆成两个可分别审查的接口：前端负责从源码和注解生成公式，后端负责判定公式。基于 SMT 的软件验证常查询每个义务之否定是否可满足；SAT 模型帮助定位失败状态，UNSAT 则只在所选理论与编码下证明该项义务。

模块化验证可把函数契约当作调用处摘要：调用者证明被调函数前置，生成器随后假设其后置与 frame condition。摘要若遗漏副作用，错误发生在 VC 生成之前，求解器再可靠也无法补救。可信工具链因此通常同时记录源语义、生成规则、背景理论和未解决义务，而不把“本次求解成功”误写成没有条件的程序正确性。

参考资料

Robert W. Floyd, “Assigning Meanings to Programs,” in Mathematical Aspects of Computer Science, AMS, 1967, pp. 19–32。
C. A. R. Hoare, “An Axiomatic Basis for Computer Programming,” Communications of the ACM 12(10), 1969, pp. 576–580, 583。
K. Rustan M. Leino, This is Boogie 2, Microsoft Research, 2008。
Krzysztof R. Apt, Frank S. de Boer, and Ernst-Rüdiger Olderog, Verification of Sequential and Concurrent Programs, 3rd ed., Springer, 2009。

形式陈述 ​

反向链接

形式陈述