抽象域

符号抽象域 ​

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

其解释例如

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

若程序执行 x := x*x，任何整数输入的输出都非负，故抽象转移可把 $\mathrm{\top }$ 送到 $\mathsf{nonneg}$。对 x := x+1 则要用整数边界实际计算：$x<0$ 意味着 $x\le -1$，加一后至多为零，所以 neg 的最佳输出是 nonpos，不是 $\mathrm{\top }$。例如 $-3$ 变成 $-2$，$-1$ 变成 $0$，两种符号都必须覆盖。

同一语句若从 nonpos 出发，输出包含负数、零和正数 $1$，本域才只能返回 $\mathrm{\top }$。具体输出其实不超过 $1$，但符号标签无法保留这个数值上界。这里区分了转移计算错误与域本身的精度损失；换成实数变量时，负数 $-1/2$ 加一也能变正，前一个整数结论便不再适用。

环境域与控制流合流 ​

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

函数空间按变量逐点排序和 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$ 可靠，若

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

不能精确表示与不存在最佳近似是两回事。全体偶数在上述符号域中不能被精确表示，但仍有唯一最佳可靠近似 $\mathrm{\top }$：偶数同时包含负数、零和正数，其他元素都覆盖不全。反之，若某个域对集合 $X$ 只有两个互不可比的最小可靠上界，且没有共同的更小可靠上界，才是真的没有最佳近似。

若每个具体集合都有最佳近似，可用 $\alpha (X)$ 表示它，并以 Galois 连接刻画 $\alpha (X)⊑a⟺X\subseteq \gamma (a)$。这条等价式说明，$\alpha$ 选出的不是任意安全标签，而是所有安全标签中最精确者。最佳值的存在也不保证计算便宜；本页不把 Galois 连接预设为所有抽象域定义的一部分。

仅由 $\gamma$ 单调可知 $\gamma (a\sqcap b)\subseteq \gamma (a)\cap \gamma (b)$，不能据此把 meet 当成交集的可靠上近似。若 $\gamma$ 是 Galois 连接中的右伴随，它保持 meet，此时上述包含成为等号。join 则覆盖替代分支：$\gamma (a)\cup \gamma (b)\subseteq \gamma (a\bigsqcup b)$。把程序分支的“二选一”误用 meet，会把允许状态删掉，直接破坏可靠性。

区间、终止与分析边界 ​

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

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

抽象域也不等同于没有解释的分类标签清单。次序与 concretization 给出谁更精确、每个元素覆盖哪些状态，局部转移的可靠包含可以直接在这个接口上陈述。若所选求解器还使用 $\mathrm{\top }/\mathrm{\perp }$、join 或无限链上界，就必须另给这些对象及相应语义条件；它们不是所有抽象域一律具备的组成部分。

从域到完整分析 ​

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

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