抽象解释

从具体语义到抽象方程 ​

设具体性质格为 $C$，程序语义由单调算子 $F:C\to C$ 给出，具体可达语义是最小不动点

选定抽象域 $A$、concretization $\gamma :A\to C$ 和抽象算子 $F^{\mathrm{\#}}:A\to A$。局部可靠性要求

若分析求得抽象后不动点 $a^{\star }$ 满足

则由可靠抽象转移公理库可靠抽象转移函数Sound abstract transformer · Sound abstract transfer function以具体变换与抽象变换的交换不等式保证每个具体后继都被抽象结果覆盖。和不动点归纳得到

这条包含关系是抽象解释的安全证书：分析结果覆盖所有具体行为。

不动点证明责任 ​

Knaster–Tarski 定理公理库Knaster–Tarski 不动点定理Knaster-Tarski fixed-point theorem · Tarski fixed-point theorem完备格上的单调自映射之全部不动点构成完备格，并具有规范的最小与最大不动点。保证完备格上的单调算子存在最小不动点，也给出它是全部前不动点的下确界。它负责语义存在与归纳原则，不负责算法有限终止。

若抽象格有限高度，worklist 从 $\mathrm{\perp }$ 上升会稳定在最小抽象不动点。无限高度数值域可产生

需要widening公理库Widening 与 NarrowingWidening and narrowing · Widening operator · Narrowing operator以 widening 强制抽象迭代有限稳定，再用 narrowing 在可靠上界内恢复部分精度。跳到可靠上界，再用 narrowing 恢复精度。

最终结果可能只是后不动点，不等于 $\mu F^{\mathrm{\#}}$，更不等于具体最小不动点的最佳抽象。终止、可靠和最优精度是三个独立性质。

符号分析的完整轨迹 ​

考虑程序：

x := input
if x >= 0:
    y := x + 1
else:
    y := 0
assert y >= 0

用符号域分析。入口 $x=\mathrm{\top }$；真分支 guard 收紧为 $x=nonneg$，赋值 x+1 得 $y=pos$；假分支令 $y=zero$。汇合 join 得 $y=nonneg$，足以证明断言。

每个步骤都有独立责任：guard 不漏掉满足条件的状态，赋值覆盖所有算术结果，join 覆盖两分支，断言检查确认抽象集合与坏集合交为空。

若分析器不做 guard refinement，真分支会从 $x=\mathrm{\top }$ 得 $y=\mathrm{\top }$，汇合仍为 $\mathrm{\top }$，无法证明断言。结果更粗但仍可靠，说明“证明失败”不等于程序有错误。

正确告警与假警报 ​

可靠抽象若报告 bad 可能可达，真实含义是抽象状态与坏区域相交。交点可能由不同路径或变量独立组合制造，并无对应具体执行。

例如 y:=x; assert x-y==0 在逐变量区间域中会丢失等式关系，得到差值跨零的宽区间。换关系域、路径拆分或谓词精化可以排除假警报。

相反，若抽象结果证明坏区域不可交，则具体行为也不可达；这正是 over-approximation 的单向力量。用 under-approximation 找到具体测试路径有助于 bug finding，却不能承担同样的全称安全证明。

框架而非抽象执行比喻 ​

把运算符换成区间、符号或常量传播版本，是一种实现直觉；只有给出 concrete semantics、concretization 和交换不等式后，才成为形式抽象解释。

框架也不指定唯一域。区间、octagon、polyhedra、形状图和字符串自动机分别保留不同性质；域的 reduced product 可以交换信息，但组合 transfer 和 reduction 仍需证明可靠。

分析可以是前向或后向、may 或 must、flow-sensitive 或 context-sensitive。它们共享抽象语义结构，不是同一个算法的参数别名。

实现与语言边界 ​

前端必须建模整数溢出、浮点 NaN、异常、别名、未定义行为和并发干扰。抽象域数学再精细，若具体语义漏了一类真实步骤，端到端 soundness 仍失败。

外部库可用摘要替代代码；摘要前置条件若不满足或副作用漏写，会污染所有调用点。可信报告应列出未建模特性和使用的假设，而不是无条件声称“静态分析不会漏报”。