八边形抽象域 | Codeboy's Blog

形式陈述

从差分约束到带符号坐标

固定 $n$ 个数学变量，取值域为 $\mathbb K=\mathbb Q$ 或 $\mathbb R$ ，所有约束非严格，所有端点运算精确。八边形约束允许 $\pm x_p\pm x_q\le c$ ，也允许单变量上下界。二维时这些不等式的边界只有水平、竖直和两种对角方向；交集至多有八个方向的边，名称由此而来，具体集合不必恰有八条边。

引入 $2n$ 个带符号坐标，使用从零开始的下标：

z_{2p}=x_{p+1},\qquad z_{2p+1}=-x_{p+1},\qquad \bar i=i\mathbin{\mathrm{xor}}1.

沿用差分约束抽象域与 DBM的方向， $M_{ij}\in\mathbb K\cup\{+\infty\}$ 是 $z_j-z_i$ 的上界。其具体含义是

\gamma_{\mathrm{oct}}(M)= \{x\in\mathbb K^n:\ \forall i,j,\ z_j(x)-z_i(x)\le M_{ij}\}.

坐标满足 $z_{\bar i}=-z_i$ ，因此同一个表达式有两种写法： $z_j-z_i=z_{\bar i}-z_{\bar j}$ 。矩阵称为相干（coherent），若

M_{ij}=M_{\bar j,\bar i}.

输入一条约束时，同时收紧这两个位置即可保持相干。以 $(z_0,z_1,z_2,z_3)=(x,-x,y,-y)$ 为例， $x+y\le c$ 存在 $(1,2)$ 与 $(3,0)$ ， $x-y\le c$ 存在 $(2,0)$ 与 $(1,3)$ 。一元界 $x\le u$ 写成 $z_0-z_1=2x\le2u$ ，所以无需再添加恒零坐标。

普通闭包后的加强公式

先对相干矩阵做普通最短路闭包，得到 $C$ 。初始化对角线时取原值与零的较小者，保留已有的负对角；若发现负环，结果为空。确认非空后，对角线为零，且

C_{ij}\le C_{ik}+C_{kj}.

闭包仍相干：每条 $i\to j$ 路径反向并对各下标取横线，得到一条同权的 $\bar j\to\bar i$ 路径。然而，普通路径相加尚未用足带符号坐标的身份。由两条一元约束

-2z_i=z_{\bar i}-z_i\le C_{i,\bar i},\qquad 2z_j=z_j-z_{\bar j}\le C_{\bar j,j}

相加并除以二，还能推出 $z_j-z_i$ 的界。于是定义一次加强：

S_{ij}=\min\left(C_{ij},\frac{C_{i,\bar i}+C_{\bar j,j}}2\right).

相干矩阵若具有零对角、满足所有三角不等式，并且满足

S_{ij}\le\frac{S_{i,\bar i}+S_{\bar j,j}}2,

就称为强闭合。在上述有理数或实数模型下，先普通闭包、再一次加强，即得到与原输入具有相同具体含义的强闭合矩阵；不需要交替重复这两步。下面分别解释可行性与“一次就够”的原因。

直觉

为什么负环检查仍然有效

普通 DBM 算法暂时把 $2n$ 个坐标当成独立势能。若它有一个解 $v$ ，相干性保证 $w_i=-v_{\bar i}$ 也是解，因为

w_j-w_i=v_{\bar i}-v_{\bar j}\le C_{\bar j,\bar i}=C_{ij}.

差分约束的解集是凸的，因此中点 $u=(v+w)/2$ 仍满足全部约束，并且 $u_{\bar i}=-u_i$ 。取 $x_{p+1}=u_{2p}$ ，便得到真正的程序状态。反过来，任何程序状态显然给出一个独立势能解。故在 $\mathbb Q$ 或 $\mathbb R$ 上，普通 DBM 可行性与带符号约束可行性等价；加强只显化逻辑后果，不会删除合法状态。

这里的中点是模型中真正需要的运算。整数势能的中点可能是半整数，所以整数八边形不能直接沿用这一可行性结论。

为什么加强不会破坏路径闭包

写成 $a_i=C_{i,\bar i}/2$ 、 $b_i=C_{\bar i,i}/2$ ，加强公式就是 $S_{ij}=\min(C_{ij},a_i+b_j)$ 。闭包与相干性给出

2a_i=C_{i,\bar i} \le C_{ik}+C_{k,\bar k}+C_{\bar k,\bar i} =2C_{ik}+2a_k,

即 $a_i\le C_{ik}+a_k$ 。同理 $b_j\le b_k+C_{kj}$ ；无负环还保证 $a_k+b_k\ge0$ 。

现在展开 $S_{ik}+S_{kj}$ 中两个最小值，共有四种候选和。每一种都不小于 $S_{ij}$ ：

\begin{aligned} C_{ik}+C_{kj}&\ge C_{ij}\ge S_{ij},\\ C_{ik}+a_k+b_j&\ge a_i+b_j\ge S_{ij},\\ a_i+b_k+C_{kj}&\ge a_i+b_j\ge S_{ij},\\ a_i+b_k+a_k+b_j&\ge a_i+b_j\ge S_{ij}. \end{aligned}

所以它们的最小值仍满足 $S_{ik}+S_{kj}\ge S_{ij}$ ，三角不等式得以保留。公式也保持相干； $a_i+b_i\ge0$ 保证 $S_{ii}=0$ 。最后，一元位置不变：因 $b_{\bar i}=a_i$ ，有 $S_{i,\bar i}=\min(C_{i,\bar i},2a_i)=C_{i,\bar i}$ 。因此加强右侧的一元界并未继续变化，所得 $S$ 已满足强闭合的全部条件。允许 $+\infty$ 时这些比较仍成立，因为全过程没有 $-\infty$ 。

例子与边界

一张完整的四阶矩阵证书

设初始集合为

P=\{(x,y):0\le x\le2,\ 0\le y\le3,\ x-y\le1\}.

仍按 $(x,-x,y,-y)$ 排列行列。直接写入约束、普通闭包、加强，分别得到

M=\begin{pmatrix} 0&0&\infty&\infty\\ 4&0&\infty&1\\ 1&\infty&0&0\\ \infty&\infty&6&0 \end{pmatrix},\qquad C=\begin{pmatrix} 0&0&7&1\\ 4&0&7&1\\ 1&1&0&0\\ 7&7&6&0 \end{pmatrix},

S=\begin{pmatrix} 0&0&3&0\\ 4&0&5&1\\ 1&0&0&0\\ 5&3&6&0 \end{pmatrix}.

例如普通闭包沿 $1\to3\to2$ 得到 $C_{12}=1+6=7$ ；加强利用 $C_{10}=4$ 与 $C_{32}=6$ ，将它收紧为 $S_{12}=(4+6)/2=5$ ，即 $x+y\le5$ 。同理 $S_{03}=0$ 表示 $x+y\ge0$ 。

矩阵其余项也可直接核验。 $P$ 的顶点是 $(0,0),(1,0),(2,1),(2,3),(0,3)$ ，所有 $z_j-z_i$ 都是线性函数，在这些顶点上取最大值便得到整张 $S$ 。其非对角信息归结为

0\le x\le2,\quad0\le y\le3,\quad -3\le x-y\le1,\quad0\le x+y\le5.

上下界分别都由列出的顶点达到。这既检查了十六个元素，也说明这次加强没有改变 $P$ 。初始的和界 $5$ 本就能由两个变量的上界相加得到；此处展示的是带符号 DBM 如何显化它，域的表达能力差异要看接下来的过滤。

一条和式 guard 改变了能够证明的断言

考虑程序：

text

assume 0 <= x <= 2 and 0 <= y <= 3 and x-y <= 1
assume x+y <= 4
x := x+1
assert x+y <= 5

第二行把相干位置 $(1,2),(3,0)$ 的界同时改为 $4$ 。本例所得 $G$ 已强闭合。赋值对应带符号位移 $\delta=(1,-1,0,0)$ ，精确更新为 $T_{ij}=G_{ij}+\delta_j-\delta_i$ ，所以

G=\begin{pmatrix} 0&0&3&0\\ 4&0&4&1\\ 1&0&0&0\\ 4&3&6&0 \end{pmatrix},\qquad T=\begin{pmatrix} 0&-2&2&-1\\ 6&0&5&2\\ 2&-1&0&0\\ 5&2&6&0 \end{pmatrix}.

该公式是赋值前后的差直接代换： $z'_j-z'_i=(z_j-z_i)+\delta_j-\delta_i$ ，逆平移给出反向包含，故不是仅仅可靠的外近似。读 $T_{12}=5$ 或相干的 $T_{30}=5$ ，即得到全部执行都满足的 $x+y\le5$ 。

guard 后的多边形顶点是 $(0,0),(1,0),(2,1),(2,2),(1,3),(0,3)$ 。它仍具有与 $P$ 相同的各变量上下界、 $x-y$ 上界 $1$ 及下界 $-3$ ，因此它的最佳 zone 外近似仍是 $P$ ，其中包含已被 guard 排除的点 $(2,3)$ 。平移后这个伪状态变成 $(3,3)$ ，违反待证断言。独立区间抽象域也保留这一伪状态；即便区间端点完全精确，仍无法保存 $x+y\le4$ 。

相同坐标系中，区间矩形包含点 A=(2,0)，差分 zone 排除 A 却保留 B=(2,3)，加入 x+y≤4 的八边形约束又排除 B；三个区域展示逐步保留的变量关系 — 从区间与差分约束到和式 guard

整数与任意斜率的边界

整数模型还要利用整性。例如 $2x\le3$ 在整数上应收紧为 $2x\le2$ 。更明显地， $2x\le1$ 与 $-2x\le-1$ 在实数上允许 $x=1/2$ ，在整数上却不可满足：普通负环检查并不能发现这个整数矛盾。整数八边形需要紧闭包，将一元界的偶数性与关系传播一起处理；只在加强公式中向下取整，并未给出完整的紧规范化算法。

八边形也不能精确表示整个直线 $y=2x$ 。它只有系数为 $\pm1$ 的双变量约束及一元约束；在这条无界直线上，每个非零的允许线性表达式都向上无界，因此任何有限的此类界都会误删真实点。任意线性多面体可用两个不等式 $y-2x\le0$ 、 $2x-y\le0$ 表示该直线，表达能力因此更强。

推论与应用

关系精度对应哪些计算代价

对 $n$ 个程序变量，矩阵有 $2n$ 行列，空间为 $O(n^2)$ 。普通 Floyd 闭包耗时 $O(n^3)$ ，随后加强扫描全部元素，耗时 $O(n^2)$ ，完整规范化仍为 $O(n^3)$ 。一条二元 guard 只需先写两个相干位置，写入成本为 $O(1)$ ，之后通常要重新规范化；不能把写入成本当作整个过滤操作的成本。

单变量平移只影响该变量两个带符号坐标的行列，更新成本为 $O(n)$ 。它保持相干、三角不等式和加强关系：位移在三角式中相消，且 $\delta_{\bar i}=-\delta_i$ 使加强式两侧得到相同的位移。因此从强闭合输入出发，本例的平移无需重新做立方成本的闭包。

从表示到验证，这一页完成了同一条链：用相干性记录符号配对，用中点论证可行性，用一次加强补全一元界之间的推论，再以和式 guard 与平移保留断言需要的关系。它适合差与和共同出现的数值不变量；选择此域的收益，正是像例子中那样保住 zone 会丢失的斜向边界。

参考资料

Antoine Miné, “The Octagon Abstract Domain”, Higher-Order and Symbolic Computation 19, 2006, pp. 31–100。此处参照 2006-04-13 的 90 页作者版，§§3.1、3.3–3.5、Theorems 2–6 与 Appendix B，讨论带符号表示、相干性、强闭包及其语义性质。
Antoine Miné, “Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation”, 2017，§5.4.5，印刷页 137–140，式 (5.19)–(5.21)。给出普通闭包后加强的算法与整数情形的区别。
Aziem Chawdhary, Ed Robbins and Andy King, “Incrementally Closing Octagons”, Formal Methods in System Design，§5.1、Theorem 5.1 证明闭合相干矩阵经加强即强闭合，§6 单独处理整数紧闭包。

区间抽象域

“八边形抽象域进一步保存 $x+y\le4$ 这样的和式关系：即使 guard 不改变任何单变量端点，它仍能排除区间外近似中的伪状态，并在后续平移后证明求和断言。”

差分约束抽象域与 DBM

“DBM 适合差值有界、计数器同步增长、索引相对偏移等性质，但不能精确表示一般的 $x+y\le c$ 或 $y=2x$。八边形抽象域扩展到 $\pm x\pm y\le c$，通过带符号坐标…”

形式陈述 ​

从差分约束到带符号坐标 ​

普通闭包后的加强公式 ​

为什么负环检查仍然有效 ​

为什么加强不会破坏路径闭包 ​

一张完整的四阶矩阵证书 ​

一条和式 guard 改变了能够证明的断言 ​

整数与任意斜率的边界 ​

关系精度对应哪些计算代价 ​

反向链接