抽象域

抽象值代表具体状态集合 ​

设具体状态集合为 $\mathrm{\Sigma }$，具体语义公理库收集语义Collecting semantics · Reachability semantics at program points为每个程序点收集所有可达具体状态，作为静态分析需要可靠逼近的具体语义基准。位于幂集格

$$C=(\mathcal{P}(\mathrm{\Sigma }),\subseteq ).$$

抽象域由抽象元素集合 $A$、偏序 ${⊑}_A$ 以及解释抽象值的 concretization

$$\gamma :A\to \mathcal{P}(\mathrm{\Sigma })$$

组成。本文采用的方向是

$$a{⊑}_{A}b⟹\gamma (a)\subseteq \gamma (b),$$

所以较小元素更精确，较大元素覆盖更多具体状态。若文献采用“信息更多者更大”的反向次序，join、meet 与迭代方向也要一起翻转，不能只改符号。

用于不动点分析时，$A$ 通常组织成完备格公理库完备格Complete lattice · Complete ordered lattice任意子集都具有上确界和下确界，从而包含顶元、底元并支持任意族合流的格。或至少满足算法所需的有限合流与链上界。$\mathrm{\top }$ 表示完全未知，覆盖全部 $\mathrm{\Sigma }$；$\mathrm{\perp }$ 表示没有可能状态，通常解释为空集。

符号抽象域 ​

对一个整数变量 $x$，符号域可取

$$A_{sign}=\{\mathrm{\perp },\mathsf{neg},\mathsf{zero},\mathsf{pos},\mathsf{nonpos},\mathsf{nonneg},\mathrm{\top }\}.$$

其解释例如

$$\gamma (\mathsf{neg})=\{n\in \mathbb{Z}:n<0\},\gamma (\mathsf{nonneg})=\{n\in \mathbb{Z}:n\ge 0\}.$$

$\mathsf{neg}$ 与 $\mathsf{zero}$ 的最小共同上界是 $\mathsf{nonpos}$；$\mathsf{neg}$ 与 $\mathsf{pos}$ 的 join 若域中没有“非零”元素，只能是 $\mathrm{\top }$。join 的结果由域的表达能力决定，不是把两个标签字符串拼接起来。

若程序执行 x := x*x，任何输入的输出都非负，故抽象转移可把 $\mathrm{\top }$ 送到 $\mathsf{nonneg}$。若执行 x := x+1，neg 输入可能仍负、变零或变正，粗符号域只能返回 $\mathrm{\top }$；这不是语义不可靠，而是域无法表达“至少比原值大一”这类关系。

环境域与控制流合流 ​

多个变量的抽象环境可写作点态函数

$${\rho }^{\mathrm{\#}}:Var\to A_{sign}.$$

函数空间按变量逐点排序和 join。例如一条分支结束时得到 $x=\mathsf{neg}$，另一条得到 $x=\mathsf{zero}$，汇合后的最小可靠摘要为 $x=\mathsf{nonpos}$。

逐变量乘积是非关系域：它能分别记录 $x,y$ 的符号，却不能表达 $x=y$。若两条分支分别得到 $(x,y)=(0,0)$ 与 $(1,1)$，逐变量集合允许额外组合 $(0,1)$、$(1,0)$。关系域可保存等式或多面体约束，但通常付出更高计算成本。

抽象域因而同时规定可表达性质与精度上限。更丰富不总是更合适；分析目标若只需证明数组长度非负，完整多面体域可能增加成本而不改变结论。

可靠、精确与最佳表示 ​

抽象值 $a$ 对具体集合 $X$ 可靠，若

$$X\subseteq \gamma (a).$$

可靠允许额外状态，不能推出没有假警报。精确则是相对概念：在同一域内，$a⊑b$ 表示 $a$ 至少不比 $b$ 粗；跨域比较还需建立转换或共同具体语义。

某些具体集合在域中没有最精确表示。例如只含 even 和 odd 区别的事实无法由纯符号域表达。即使最精确抽象存在，计算它也可能昂贵；Galois 连接会形式化 abstraction $\alpha$、concretization $\gamma$ 与最佳抽象之间的伴随关系，本页不把它预设为所有抽象域定义的一部分。

meet 表示同时施加两个抽象约束，但其 concretization 可能只是交集的可靠近似；join 表示覆盖替代分支。把程序分支的“二选一”误用 meet 会漏掉行为，直接破坏 soundness。

区间、终止与分析边界 ​

区间是数值抽象域的典型实例：每个变量由上下界表示，能高效传播范围，却会丢失变量相关性。区间算术自身的向外舍入保证与静态分析的抽象转移可靠性属于两层证明，完整例子由后续区间抽象域页面承担。

完备格保证语义上的任意 join 存在，不保证朴素迭代有限步终止。无限上升链可以让分析不断产生更宽界；widening 会主动跳到更粗上界以换取终止，结果通常不是最小不动点。

抽象域也不等同于分类标签清单。若没有次序、$\mathrm{\top }/\mathrm{\perp }$、join 以及每个元素的具体含义，就无法判断合流是否可靠、分析结果谁更精确，也无法证明转移函数覆盖具体行为。

从域到完整分析 ​

仅选定 $A$ 还没有完成静态分析。还需为每条具体语句给出抽象转移，沿控制流建立方程，选择迭代与终止策略，并证明结果包含收集语义。可靠抽象转移函数承担局部交换不等式，抽象解释框架再把这些部件接成全局不动点。

这个分层避免把“域很精细”误写成“分析正确”。一个关系域若转移函数漏掉整数溢出仍不可靠；一个粗糙的符号域只要覆盖所有具体结果，依然可以给出可信但保守的证明。

参考资料

• Patrick Cousot and Radhia Cousot, “Abstract Interpretation: A Unified Lattice Model for Static Analysis,” POPL, 1977, pp. 238–252。
• Flemming Nielson, Hanne Riis Nielson, and Chris Hankin, Principles of Program Analysis, Springer, 1999, Chs. 2–4。
• Xavier Rival and Kwangkeun Yi, Introduction to Static Analysis, MIT Press, 2020, Chs. 5–7。
• Antoine Miné, “A Few Graph-Based Relational Numerical Abstract Domains,” SAS, Springer, 2002, pp. 117–132。