Houdini 不变式推断 | Codeboy's Blog

形式陈述

候选不是已经成立的事实

给定转移系统 $(S,I,T)$ 和有限候选表 $C=\{c_1,\ldots,c_m\}$ 。候选是状态谓词，可能为假。对当前保留集合 $A\subseteq C$ ，记

H_A(s)=\bigwedge_{c\in A}c(s),\qquad H_\varnothing=\top.

目标是在这张候选表内找到足够有用的归纳不变式。Houdini 从 $A=C$ 开始，每轮对每个 $c\in A$ 检查

I(s)\land\neg c(s),\tag{初始失败}

H_A(s)\land T(s,s')\land\neg c(s').\tag{保持失败}

可用SMT查询这些反例公式。某式 SAT 就删除对应候选，并保存见证；同轮所有查询采用同一个旧 $A$ ，之后批量删除，再开始下一轮。没有可删除项且所有剩余义务均 UNSAT 时返回 $H_A$ 。[1, §2]

unknown 不表示验证成功。可暂停并返回未完成；也可保守删去未知候选后继续，但后者可能损失本来可保留的事实，不再承诺下面的精确最大性。下载脚本在显式有限 $S,T$ 上穷尽查询，因此没有 unknown。

停机与可靠性

每个非终止轮至少删除一个候选，不会重新加入；至多 $m$ 轮删除后，再经一轮无删除检查即停止。最终逐项初始化合起来给 $I\Rightarrow H_A$ ，逐项保持合起来给 $H_A\land T\Rightarrow H_A'$ ，所以返回合取确为归纳不变式。

若目标是安全性质 $P$ ，还要单独证明 $H_A\Rightarrow P$ 。Houdini 返回真也满足初始和保持，但它通常不能排除坏状态；“候选筛选完成”不能代替安全证明。

最大性只相对于候选合取

假定查询精确。取任意 $B\subseteq C$ ，其合取 $H_B$ 已经是归纳不变式。算法始终保持 $B\subseteq A$ ：初始失败的候选不可能属于 $B$ ；若保持失败见证满足 $H_A(s)$ ，则在 $B\subseteq A$ 下也满足 $H_B(s)$ 。若被删候选 $c$ 属于 $B$ ，归纳性便强迫 $c(s')$ ，与见证矛盾。

因此任何有效候选子集都包含于最终 $A$ 。最终 $A$ 自身又有效，所以它是按候选包含关系最大的有效子集，其合取在这些子集合取中逻辑最强。候选越多、合取越强，允许状态反而越少；不能把最大候选集写成最大允许状态集。它也不等于所有可表达不变式中的最强者。

直觉

删除一个支点，别的候选可能失效

算法起初乐观地同时假设全部候选来检查一步保持，但这份乐观必须受独立初始化约束。某候选删去以后， $H_A$ 变弱，归纳步要考虑的源状态变多；此前通过的其他候选可能因此失效，必须重查。

反过来，不能强求每个候选单独归纳。若两个布尔量每步交换，初值都为0，候选 x=0 与 y=0 合起来可以保持；单独 x=0 却允许旧 y=1，交换后失败。合取中的事实可以相互支撑，前提是整个合取确实从初态建立并整体保持。

例子与边界

五个状态、三轮级联删除

取 $S=\{0,1,2,3,4\}$ ， $I=\{0\}$ ，全部转移为

0\to1,\quad1\to2,\quad2\to2,\quad3\to4,\quad4\to4.

实际可达集是 $\{0,1,2\}$ 。给出五个候选

p_0:s>0,\quad p_1:s\ne1,\quad p_2:s\ne2, \quad p_3:s\le2,\quad p_4:s\ne4.

轮次	本轮合取允许的源状态	删除与见证
0	空集	$p_0$ 在初态0失败；保持查询虽空真仍不能保留它
1	$\{0\}$	$0\to1$ 否定后态的 $p_1$
2	$\{0,1\}$	$1\to2$ 否定后态的 $p_2$
3	$\{0,1,2\}$	无删除，返回 $p_3\land p_4$

例如第1轮尚不能删除 $p_2$ ：源状态1仍被 $p_1$ 排除，而从0出发的新状态1满足 $s\ne2$ 。删除 $p_1$ 后才出现该反例。这就是只做一遍会漏掉的依赖。

最后证书为 $H(s)=(s\le2)\land(s\ne4)$ 。初态0满足它；三条从 $H$ 内出发的边分别落在1、2、2，仍满足它；它蕴涵目标 $s\ne4$ 。所有任意长度的可达执行因此安全。下载脚本另枚举全部 $2^5=32$ 个候选子集，验证每个归纳子集都包含于最终 $\{p_3,p_4\}$ ，与最大性证明对照。

三个红色删除见证逐步扩大归纳源集合，绿色最终区域对所有转移闭合；下半图区分从初态的base与任意状态的step — 候选剔除与归纳证书

真性质也可能被剔除

换成 $S=\{0,1,2,3\}$ ，初态0，边为 $0\to1,1\to1,2\to3,3\to3$ 。候选只有 $P(s)\equiv s\ne3$ 。它在全部可达状态0、1上为真，但保持查询发现不可达的 $2\to3$ ，所以被删除，结果为真。

这不证明程序有错，只证明当前候选表无法提供所需的一步归纳屏障。加入 $Q(s)\equiv s\le1$ 后， $Q\land P$ 排除源状态2，两候选都可保留，并推出安全。k归纳则从另一方向使用更长安全窗口处理某些这样的不可达干扰。

推论与应用

复杂度、候选语言与最终检查

每轮至多对 $m$ 个候选各查两式，总查询数不超过 $2m(m+1)$ 。这只是查询次数，不是多项式求解时间保证。 $m=0$ 时不需候选查询，立即得到真；仍须检查真是否蕴涵目标。

显式有限模型上，按下载脚本逐状态和逐边检查，且每个谓词求值按常数计，可用 $O((m+1)^2(|S|+|T|+1))$ 保守界住总工作；日志最多记录每项一次删除见证。若谓词本身复杂，另计其求值成本；若模型以公式隐式给出，则应报告实际求解费用。

Houdini 不生成候选之外的新谓词，也不自动组合任意析取。候选可来自模板、程序比较式或测试猜测，但最终可靠性来自初始化和一步保持的全称检查，不来自样本上暂时未见失败。候选中若已有一个析取公式，当然可以把它作为一个整体检查；受限的是候选间组合语言，而非谓词内部语法。

迁移练习：在五状态模型中添加边 $2\to3$ 。第3轮 $p_3$ 由该边否定；删除后源状态3进入合取允许范围， $3\to4$ 再否定 $p_4$ ，最终无候选。此时实际路径 $0,1,2,3,4$ 也确实违反安全目标；保存删除见证与实际可达反例，能分清“证明不够强”和“程序真的不安全”。

参考资料

[1] Cormac Flanagan、K. Rustan M. Leino，Houdini, an Annotation Assistant for ESC/Java，Compaq SRC Technical Note 2000-003，2000年12月31日；§2（正文3–4页）给候选检查与删除循环，§8说明只组合候选合取。会议版本发表于 FME 2001，500–517页。本文是单位置转移系统上的精确变体，最大性证明与有限算例在正文独立给出，不继承未建模的 Java 语义。

形式陈述 ​

候选不是已经成立的事实 ​

停机与可靠性 ​

最大性只相对于候选合取 ​

删除一个支点，别的候选可能失效 ​

五个状态、三轮级联删除 ​

真性质也可能被剔除 ​

复杂度、候选语言与最终检查 ​

反向链接