可靠抽象转移函数

局部可靠性不等式 ​

设具体域 $C=\mathcal{P}(\mathrm{\Sigma })$，抽象域 $A$ 与 concretization $\gamma :A\to C$ 已给定。具体语句的集合变换为 $f:C\to C$，实现的抽象变换为 $f^{\mathrm{\#}}:A\to A$。

$f^{\mathrm{\#}}$ 可靠，若

$$\mathrm{\forall }a\in A,f(\gamma (a))\subseteq \gamma (f^{\mathrm{\#}}(a)).$$

左侧收集所有由 $a$ 代表状态执行一步可能得到的结果；右侧必须全部包住它们。可靠性是“不漏掉具体行为”，不是“只产生真实行为”。

若有Galois 连接公理库抽象解释中的 Galois 连接Galois connection for abstract interpretation · Abstraction-concretization adjunction以 abstraction 与 concretization 的伴随关系刻画可靠表示、闭包以及具体变换的最佳抽象。 $(\alpha ,\gamma )$，等价地可要求

$$\alpha \circ f{\le }_A{f}^{\mathrm{\#}}\circ \alpha .$$

交换图不必严格相等；不等式方向允许抽象变换比最佳结果更粗。

赋值的区间轨迹 ​

考虑整数赋值 x := x + 1，抽象状态给出 $x\in [2,5]$。具体像是

$$\{x+1:x\in [2,5]\cap \mathbb{Z}\}=\{3,4,5,6\}.$$

抽象变换返回 $[3,6]$，其 concretization 恰好包含具体像，因此可靠。返回 $[3,5]$ 会漏掉输入 $x=5$ 的后继 $6$，即使对其他三个测试值都正确，也不可靠。

若机器整数在最大值处回绕，数学整数的 $[l+1,u+1]$ 公式可能漏掉负数结果。抽象变换必须匹配语言操作语义公理库操作语义Operational semantics用执行判断、转移规则或抽象机定义程序如何运行。中的位宽、溢出和异常规则。

guard 与分支过滤 ​

对条件 x < 0 的真分支，具体变换是集合交

$$f_{true}(X)=\{\sigma \in X:\sigma (x)<0\}.$$

输入区间 $[-2,3]$ 可收紧为 $[-2,-1]$（整数语义）。假分支则收紧为 $[0,3]$。若分析器懒惰地两边都返回原区间，仍然可靠但较不精确。

若浮点语义允许 NaN，条件 x < 0 为假不等价于 $x\ge 0$；NaN 会走假分支。用实数全序过滤会漏掉状态，说明 soundness 必须相对精确语言模型陈述。

组合得到路径可靠性 ​

若 $f^{\mathrm{\#}}$ 对 $f$ 可靠、$g^{\mathrm{\#}}$ 对 $g$ 可靠，且二者单调，则组合 $g^{\mathrm{\#}}\circ f^{\mathrm{\#}}$ 对 $g\circ f$ 可靠。证明把第一步包含关系代入第二步，再用单调性扩大输入。

控制流汇合还需要抽象 join 覆盖各前驱。由局部 transfer、可靠 join 与不动点迭代，可归纳证明每个程序点的抽象状态覆盖其收集语义。

若任一语句处理漏掉一种边——异常、短路求值、别名写入或并发干扰——全局证明链就在该处断裂。后续再宽的 join 不能恢复已经漏掉的具体后继。

可靠不等于精确、终止或无警报 ​

$f^{\mathrm{\#}}(a)=\mathrm{\top }$ 对每个语句都是平凡可靠变换，却几乎没有信息。精确度要比较它与最佳抽象 $\alpha f\gamma$ 的距离或次序。

每个局部变换可靠也不保证迭代终止；无限上升链仍可能持续产生新抽象值。widening 解决终止，需另证 widening 结果仍是上界。

可靠分析报告可能含假警报，因为抽象状态包括不可达行为。它保证真实错误不会因该抽象步骤被漏掉；端到端“不漏报”还依赖前端建模、所有转移和求解器实现均在可信边界内。

最佳性与完备性的区别 ​

最佳抽象变换 $\alpha f\gamma$ 是给定域内最精确的可靠实现；它仍可能不满足前向完备等式

$$\alpha f=f^{\mathrm{\#}}\alpha .$$

等式失败表示先抽象输入再变换比先做具体变换再抽象更粗。完备性是“不因这次抽象时机额外损失信息”，比 soundness 强得多，也依赖具体操作与所选域。区间域对加法可能精确，对重复变量的非线性表达式却不完备，不能给整个分析器贴一个无条件“complete”标签。

检查实现时还要覆盖 $\mathrm{\perp }$：不可达输入经过任何具体语句仍不可达，合理 transfer 应返回 $\mathrm{\perp }$ 或至少其可靠上界。若异常地从 $\mathrm{\perp }$ 生成普通状态，虽可能仍 sound，却会把不可达区域污染到后续全图。

参考资料

• Patrick Cousot and Radhia Cousot, “Abstract Interpretation: A Unified Lattice Model for Static Analysis,” POPL, 1977, pp. 238–252。
• Xavier Rival and Kwangkeun Yi, Introduction to Static Analysis, MIT Press, 2020, Chs. 6–8。
• Antoine Miné, “The Octagon Abstract Domain,” Higher-Order and Symbolic Computation 19, 2006, pp. 31–100。