谓词抽象

从具体状态到布尔向量 ​

选择谓词集合

$$\mathrm{\Pi }=\{{\pi }_1(s),\dots ,{\pi }_m(s)\}.$$

具体状态 $s$ 的抽象为布尔公理库命题逻辑Propositional logic · Propositional calculus研究命题如何通过逻辑联结词组合以及公式在真值赋值下何时成立。向量

$$\alpha (s)=({\pi }_1(s),\dots ,{\pi }_m(s))\in \{0,1{\}}^m.$$

抽象状态 $b$ 的 concretization 是满足对应谓词及否定的全部具体状态：

$$\gamma (b)=\{s:\mathrm{\forall }i,{\pi }_i(s)=b_i\}.$$

有限 $m$ 给出至多 $2^m$ 个抽象状态，即使具体变量是无界整数或堆。谓词选择决定能表达哪些关系。

对具体状态集合 $X$，最精确 Boolean predicate abstraction 可以写成所有由 $X$ 中状态产生的真值向量集合，而 Cartesian abstraction 只分别统计每个谓词是否恒真、恒假或不确定。前者保留谓词间组合，后者把组合信息投影掉。

若谓词本身逻辑相关，例如 $x>1$ 蕴含 $x>0$，某些布尔向量 concretization 为空。抽象状态生成应通过 SMT 排除空块，否则会增加永远没有具体见证的伪路径。

抽象转移的存在量词 ​

具体转移关系为 $T(s,s^{\prime })$。抽象边 $b{\to }^{\mathrm{\#}}{b}^{\prime }$ 在最粗可靠定义下存在，当且仅当

$$\mathrm{\exists }s,s^{\prime }.{\gamma }_b(s)\wedge T(s,s^{\prime })\wedge {\gamma }_{b^{\prime }}(s^{\prime }).$$

SAT 见证说明至少有一对具体状态实现该边。逐边存在不保证一串抽象边有同一条具体路径，因为中间抽象块可在不同边使用不同具体见证。

这正是 over-approximation：全部具体转移都被覆盖，额外拼接的抽象路径可能形成伪反例。抽象解释公理库抽象解释Abstract interpretation · Theory of sound static approximation以具体与抽象语义、可靠转移和不动点逼近统一组织静态程序分析的数学框架。提供其可靠性方向。

may transition 用存在量词，适合保守发现可能行为。must transition 则要求抽象块中的每个具体状态都能执行到目标块或满足相应覆盖条件，适合某些必然性质；二者量词不同，不能用同一 SAT 查询实现。

构造整张 $2^m\times 2^m$ 转移矩阵通常不可行。工具可按需从当前抽象块求后继，或用谓词当前/下一真值变量构造符号关系；无论哪种表示，都要保持具体每一步有抽象边。

计数器关系例子 ​

程序维护 $x,y$ 并每轮同时加一。只选

$${\pi }_1:x\ge 0,{\pi }_2:y\ge 0$$

时，抽象能证明非负，却不能证明 $x=y$。抽象块 (true,true) 同时包含 $(0,0)$、$(0,1)$ 和 $(100,3)$。

加入

$${\pi }_3:x=y$$

后，初态落在 ${\pi }_3=true$，转移义务

$$x=y\wedge x^{\prime }=x+1\wedge y^{\prime }=y+1\Rightarrow x^{\prime }=y^{\prime }$$

有效，因此相等块对循环闭合，可证明 assert x==y。

把谓词换成 $x=7$ 只能排除某个表面反例常数，下一轮可能出现 $x=8$。有效精化应捕捉关系根因。

若程序使用机器整数，谓词 $x+1>x$ 在最大值处为假；以数学整数证明它恒真会让抽象 transition 删除溢出分支。谓词语义必须与具体 theory 同步。

路径上 $x=y$ 可能只在某个控制位置成立。全局谓词在所有位置跟踪会增加状态，location-specific predicate 只在相关程序点启用；离开作用域时如何忘记、重新进入时如何恢复需要精确 transfer。

Cartesian 与 Boolean 抽象 ​

Cartesian predicate abstraction 为每个谓词独立记录 true、false 或 unknown，成本较低，却不保留谓词间任意布尔关系。Boolean abstraction 可表示谓词真值的任意公式，更精确但可能指数增长。

例如谓词 $x=0$ 与 $x\ne 0$ 逻辑互补。独立 unknown 状态可能包含二者同时真假不明的冗余组合；SMT 可用 consistency constraints 删除不可满足布尔状态。

Boolean abstraction 中，一个抽象状态本身可用布尔公式表示，而不必枚举 valuation。BDD/SAT 可操作这些集合，但公式共享并不消除最坏指数：某些谓词组合仍需巨大表示。

reduced product 可让区间域证明 $x\ge 0$，再把结果反馈给谓词真值；reduction 必须只删除 concretization 为空的组合，不能根据启发式“看起来不可能”删状态。

谓词越多不保证分析单调更快。状态空间按 $2^m$ 增长，transition relation 查询也会变复杂；应通过 property relevance 和反例原因选择。

weakest precondition 接口 ​

对赋值或语句 $C$，可计算每个后态谓词的 weakest precondition $wp(C,{\pi }_i)$，再判断当前谓词组合是否蕴含它、蕴含其否定，或两者都不能确定。

若都不能确定，抽象转移必须保留两种后态真值。猜一个更常见结果会漏掉具体行为。

对 assume/guard，谓词抽象可以增加条件后重新求一致真值；对 havoc，所有涉及被修改变量且无法由其他谓词推出的真值都要忘记。把 havoc 当保持会得到最危险的欠近似。

函数调用摘要可直接规定谓词关系，但局部形式参数映射到全局实参时要处理 alias；两个实参实际同址，会让分别推导的谓词更新互相影响。

量词消除或 SMT unknown 会限制精度。unknown 通常需保守地当作可能可满足，而不是当作不可达。

边界与应用 ​

谓词抽象特别适合控制性质和少量关键数据关系，不擅长自动表达大规模数值范围。可与区间等域组合，让数值域产生候选谓词或协助可行性检查。

谓词抽象只相对于建模转移 sound。指针别名、溢出、异常或并发干扰若漏编码，有限布尔模型再完整也不能覆盖真实程序。

CEGAR 用伪反例自动补谓词，但循环不保证收敛。若每次只生成路径特定常数，布尔维数持续增长；插值或 unsat core 需要概括导致不可行的共享关系。

安全证明应交付最终谓词集合和抽象不变式，使读者能检查哪些具体状态被覆盖，而不只是报告“模型检查通过”。

参考资料

• Susanne Graf and Hassen Saïdi, “Construction of Abstract State Graphs with PVS,” CAV, 1997, pp. 72–83。
• Thomas Ball et al., “Automatic Predicate Abstraction of C Programs,” PLDI, 2001, pp. 203–213。
• Edmund Clarke et al., “Counterexample-Guided Abstraction Refinement,” CAV, 2000, pp. 154–169。