抽象解释

符号分析的完整轨迹 ​

考虑程序：

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 仍失败。

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