可靠抽象转移函数

赋值的区间轨迹 ​

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

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

若机器整数在最大值处回绕，数学整数的 $[l+1,u+1]$ 公式可能漏掉负数结果。抽象变换必须匹配语言操作语义公理库操作语义Operational semantics以配置、推导规则和转移关系规定程序怎样执行及其可观察结果。中的位宽、溢出和异常规则。

guard 与分支过滤 ​

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

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

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

组合得到路径可靠性 ​

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

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

差分约束抽象域与 DBM公理库差分约束抽象域与 DBMDifference-bound matrix abstract domain · Zone abstract domain · DBM用差分约束矩阵保存变量关系，经最短路闭包、可靠转移与 raw widening，完整证明一个参数化整数循环的退出断言。把这条证明链落实为矩阵计算：差分 guard 做精确交集，平移赋值更新一行一列，闭矩阵 join 汇合分支，再以循环头归纳保持和退出闭包完成断言证明。

多面体抽象域公理库多面体抽象域Polyhedral abstract domain · Affine inequalities domain · Convex polyhedra domain以有限仿射不等式表示实数程序状态，经闭凸包汇合、guard 相交与旧变量消元，完整验证一次分支程序的关系断言。进一步允许任意有理系数的仿射关系：用旧变量改名和实数投影证明赋值精确，再以两个分支、闭凸包汇合、guard 与仿射赋值完成关系断言的证书。例中每次转移都精确，但汇合产生的伪状态仍然存留，具体展示了局部精确与全局可达精确的区别。

若任一语句处理漏掉一种边——异常、短路求值、别名写入或并发干扰——全局证明链就在该处断裂。后续 join 即使碰巧又覆盖了遗漏状态，也不能修复这一步缺失的局部可靠性证明。

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

若域有满足 $\gamma (\mathrm{\top })=\mathrm{\Sigma }$ 的顶元，$f^{\mathrm{\#}}(a)=\mathrm{\top }$ 就是平凡可靠变换，却几乎没有信息。若还给定 Galois 连接，才能进一步与最佳抽象 $\alpha f\gamma$ 按精度次序比较。

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

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

最佳性与完备性的区别 ​

在给定 Galois 连接时，最佳抽象变换 $\alpha f\gamma$ 是该域内最精确的可靠实现；它仍可能不满足后向完备（$\alpha$-completeness）等式

等式失败表示先抽象输入再变换比先做具体变换再抽象更粗。相对地，前向完备（$\gamma$-completeness）要求 $f\gamma =\gamma f^{\mathrm{\#}}$：抽象表示的具体集合经变换后仍能被输出精确表示。这两种完备性不同，也不由分析器沿 CFG 前向或后向运行来命名。完备性是“不因这次抽象时机额外损失信息”，比 soundness 强得多，也依赖具体操作与所选域。区间域对加法可能精确，对重复变量的非线性表达式却不完备，不能给整个分析器贴一个无条件“complete”标签。

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