谓词抽象

计数器关系例子 ​

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

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

加入

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

有效，因此相等块对循环闭合，可证明 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)$，再判断当前谓词组合是否蕴含它、蕴含其否定，或两者都不能确定。此处每个输入恰有一个正常后继，才可把两种后态真值这样对分。

若都不能确定，抽象转移必须保留两种后态真值。对非确定、可能阻塞或发散的语句，应回到转移关系，分别查询当前块与 $T(s,s^{\prime })\wedge {\pi }_i(s^{\prime })$、$T(s,s^{\prime })\wedge \mathrm{\neg }{\pi }_i(s^{\prime })$ 是否可满足，保留所有有见证的正常后继。不能从 $\mathrm{\neg }wp(C,{\pi }_i)$ 推出全部后继满足 $\mathrm{\neg }{\pi }_i$：例如 $C$ 可任选赋值 $x:=0$ 或 $x:=1$ 时，$wp(C,x=0)$ 为假，却仍可能得到 $x=0$。猜一个更常见结果会漏掉具体行为。

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

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

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

边界与应用 ​

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

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

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

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

CEGAR完整算例公理库反例引导的抽象精化 CEGARCounterexample-guided abstraction refinement · CEGAR完整枚举整数循环的粗细谓词图，以路径UNSAT和共享状态插值精化，并交出封闭可达集安全证书。逐项列出两非负谓词的粗图与加入相等谓词后的精图，检查一轮路径的UNSAT和切口插值，并交出只含循环头111与检查点111的封闭可达集。每张表同时给出可满足边的见证和其余边不可满足的理由。