差分约束抽象域与 DBM

形式陈述

矩阵方向与具体含义

固定数学整数变量 $x_1,\ldots,x_d$ ，另加恒为零的 $x_0$ 。差分约束矩阵（difference-bound matrix，DBM） $M$ 的元素属于 $\mathbb Z\cup\{+\infty\}$ ，本文始终采用

M_{ab}\text{ 是 }x_b-x_a\text{ 的上界},\qquad \gamma(M)=\{x\in\mathbb Z^{d+1}:x_0=0,\ \forall a,b,\ x_b-x_a\le M_{ab}\}.

因此第零行存变量上界，第零列存下界的相反数： $M_{0i}=u$ 表示 $x_i\le u$ ， $M_{i0}=-l$ 表示 $x_i\ge l$ 。 $+\infty$ 表示该项不施加约束；独立的 $\bot$ 表示空集。矩阵所表示的集合称为 zone，允许同时约束两个变量，因而能保存独立区间无法记录的 $y-i=2$ 。

按具体集合包含比较精度。同一集合可能有许多矩阵表示；逐项 $M_{ab}\le N_{ab}$ 总能推出 $\gamma(M)\subseteq\gamma(N)$ ，反向判定则应先规范化。以下操作的任务都是满足可靠抽象转移函数的集合包含要求；精确性另行说明。

闭包、空集与合流

把每个有限元素看成有向边 $a\to b$ ，权重为 $M_{ab}$ 。路径上的不等式相加，得到端点差的上界；最短路给出所有路径中最紧的界。使用Floyd–Warshall 算法计算

M_{ab}\gets\min(M_{ab},M_{ak}+M_{kb}) \quad(k=0,\ldots,d).

初始化时对角线取原值与零的较小者，不能先抹去已有负对角。出现负环等价于约束不可满足，返回 $\bot$ ；确认非空后才把规范矩阵的对角统一为零。非空结果记作 $\operatorname{cl}(M)$ ，满足

\gamma(\operatorname{cl}(M))=\gamma(M),\qquad \operatorname{cl}(M)_{ab}\le M_{ab}.

整数边权的差分约束具有整数可行性：不存在负环时，最短路势能可取整数。因此这里无需额外舍入。闭包只显化已有约束的逻辑后果，不删去具体状态；时间复杂度为 $O(d^3)$ ，矩阵空间为 $O(d^2)$ 。

交集由逐项最小值再闭包精确计算。对两个非空闭矩阵，join 则是

(M\sqcup N)_{ab}=\max(M_{ab},N_{ab}).

这是包含 $\gamma(M)\cup\gamma(N)$ 的最小 zone，结果仍闭合，但通常不是集合并本身。例如一维集合 $\{0\}$ 与 $\{2\}$ 的 join 还含整数 $1$ 。必须先闭合两个输入：未显化的隐含界可能在逐项取最大值时被丢掉。 $\bot\sqcup M=M$ ，与 $\bot$ 相交仍为 $\bot$ 。

Guard 与赋值

差分 guard $x_b-x_a\le c$ 将 $M_{ab}$ 改为 $\min(M_{ab},c)$ ，再闭包，得到精确交集。数学整数上的严格条件 $x_b-x_a<c$ （ $c\in\mathbb Z$ ）可改写为 $x_b-x_a\le c-1$ 。

平移赋值 $x_k:=x_k+c$ （ $k\ne0$ ）精确更新涉及 $k$ 的一行一列：

M'_{ak}=M_{ak}+c\ (a\ne k),\qquad M'_{kb}=M_{kb}-c\ (b\ne k),\qquad M'_{kk}=0,

其余元素不变，且 $\infty+c=\infty$ 。这是把赋值前后的变量差直接代入约束，并非对每个变量各自估计范围。

对于拷贝平移 $x_k:=x_j+c$ （ $j\ne k$ ），先闭合输入，再 forget 旧 $x_k$ ：把该行列的非对角项设为无穷，保留其他变量之间已推导出的界。随后加入 $x_k-x_j\le c$ 与 $x_j-x_k\le-c$ ，再闭包。先闭合才遗忘保证经由旧 $x_k$ 推导出的其他变量关系不丢失；此操作在本整数模型下也是精确的。取 $j=0$ 即常量赋值。一般乘法或多变量线性表达式未必落在差分约束类内，需另外构造可靠近似。

直觉

一条边不是一个变量的范围

约束 $i\le n$ 与 $y=i+2$ 可拆成 $i-n\le0$ 、 $y-i\le2$ 、 $i-y\le-2$ 。沿 $n\to i\to y$ 相加立即得到 $y-n\le2$ ，即使 $n,i,y$ 的上界都未知，这条关系仍然有用。闭包完成的正是这种传播。

DBM 的信息单位是“两个变量最多相差多少”。它比区间更能保存程序中共同变化的量，又比任意线性不等式组成的多面体约束更受限。矩阵让这一表达能力对应到具体的图算法、包含判定和程序转移。

Widening 保存不再移动的关系

即使使用规范矩阵，普通 join 迭代仍可能产生无限上升链。逐项 widening 定义为

(M\nabla N)_{ab}= \begin{cases} M_{ab},&N_{ab}\le M_{ab},\\ +\infty,&N_{ab}>M_{ab}. \end{cases}

每个保留的旧界也被新矩阵满足，每个被删除的界变为无约束，故结果覆盖两个输入。这给出widening所需的上界性。终止证明依赖一个实现细节：左侧历史矩阵必须保持 raw。每个有限元素在历史中最多变成无穷一次，不再变回有限，因此有限多个元素最终全部停止变化。

可以闭合新右参数，也可以闭合历史矩阵的副本来计算 transfer、join 或检查性质；不能把该副本回写为下一轮的左历史。闭包可能通过其他路径重建已被 widening 删除的界，这会破坏“每项只删除一次”的终止论证。语义等价的表示变换，并不自动保持一个依赖表示的加速策略。

一种可核验的调度是保存 $R_k$ ，用 $C_k=\operatorname{cl}(R_k)$ 算出新候选 $N_k=H_0\sqcup\operatorname{body}(C_k\cap G)$ ，然后仅令 $R_{k+1}=R_k\nabla N_k$ 。若 raw 矩阵不再改变，上界性保证候选已包含在它之内，于是得到了循环头后不动点。各算子遇到 $\bot$ 时按不可达状态处理，初始 $\bot\nabla N=N$ 。

例子与边界

参数化循环：从三个矩阵到断言

下面所有变量都是无溢出的数学整数，输入 $n$ 可任意大，但循环不修改它：

text

n := input_integer(); assume n >= 0
i := 0; y := 2
while i < n:
    i := i + 1
    y := y + 1
assert y == n + 2

按变量顺序 $(0,n,i,y)$ ，初始化后的闭矩阵是

H_0= \begin{pmatrix} 0&\infty&0&2\\ 0&0&0&2\\ 0&\infty&0&2\\ -2&\infty&-2&0 \end{pmatrix}.

第零行给出 $i\le0,y\le2$ ，第零列给出 $n\ge0,i\ge0,y\ge2$ ，故它恰好表示初始化。第二行还写出 $i-n\le0,y-n\le2$ ；第三、四行的 $2,-2$ 记录 $y-i=2$ 。三个指向 $n$ 的非对角元素为无穷，因为 $n$ 无上界，其余有限界都由这些初始化条件推出。

真 guard 是 $i-n\le-1$ ，即收紧 $M_{n,i}$ 。在 $H_0$ 上过滤后有 $n\ge1$ ；执行两次赋值得到 $i=1,y=3$ 。与 $H_0$ 合流，闭矩阵逐项取最大值，得到第一轮普通候选

H_1= \begin{pmatrix} 0&\infty&1&3\\ 0&0&0&2\\ 0&\infty&0&2\\ -2&\infty&-2&0 \end{pmatrix}.

只有 $M_{0,i}$ 从 $0$ 增至 $1$ 、 $M_{0,y}$ 从 $2$ 增至 $3$ ； $i\le n$ 与 $y-i=2$ 没变。于是首次 widening 是

W=H_0\nabla H_1= \begin{pmatrix} 0&\infty&\infty&\infty\\ 0&0&0&2\\ 0&\infty&0&2\\ -2&\infty&-2&0 \end{pmatrix}.

这一次只删除两个增长中的绝对上界。读第零列得到 $n\ge0,i\ge0,y\ge2$ ；读 $M_{n,i}=0$ 与 $M_{i,y}=2,M_{y,i}=-2$ 得到 $i\le n,y=i+2$ 。因此

\gamma(W)=\{(n,i,y):n\ge0,\ 0\le i\le n,\ y=i+2\}.

其余有限项都被右侧条件蕴含，例如 $y-n\le2$ 。反过来，上述关键矩阵项也已推出右侧所有条件，所以这里是相等而不仅是包含。

归纳保持与退出闭包

先证明 $W$ 是归纳不变量。初始化显然包含于 $W$ 。设一次循环开始满足 $W$ 且 guard 为真，则整数性给出 $i\le n-1$ 。执行 i := i+1 后有 $1\le i\le n$ ，而尚未更新的 $y$ 满足 $y-i=1$ ；执行 y := y+1 后重新得到 $y-i=2$ 。 $n$ 始终不变，故

\gamma(H_0)\cup\operatorname{body}(\gamma(W)\cap\{i-n\le-1\}) \subseteq\gamma(W).

这里 guard 与两个平移都是精确变换，join 是最佳 zone 上界，因此抽象候选也不超出 $W$ 。本例的 $W$ 恰好已经闭合，下一轮 raw widening 保持 $W$ ，无需 narrowing 即告稳定。证明依赖上面的保持关系，而不只是观察某次运行停止变化。

退出时 guard 为假，即 $n-i\le0$ ，收紧元素 $M_{i,n}$ 为零。与已有 $i-n\le0$ 合在一起得 $i=n$ 。闭包沿两条路径推导

y-n=(y-i)+(i-n)\le2+0=2, \qquad n-y=(n-i)+(i-y)\le0-2=-2.

两侧夹住 $y-n$ ，所以所有退出状态都满足 $y=n+2$ 。 $n=0$ 时循环执行零次，初始 $i=0,y=2$ 也直接满足结论。

退出约束补上从 i 到 n 的零权边，配合循环不变量的差分边，经两条路径分别得到 y−n≤2 和 n−y≤−2，从而证明 y=n+2 — DBM 的退出闭包证书

区间为何无法完成同一个证明

逐变量区间 widening 可得到 $n,i\in[0,\infty]$ 、 $y\in[2,\infty]$ 。即使退出过滤保留 $i\ge n$ ，独立范围仍允许伪状态 $(n,i,y)=(1,1,2)$ ，它违反断言。真实退出集合的三个精确投影也分别是 $[0,\infty]$ 、 $[0,\infty]$ 、 $[2,\infty]$ ；所以仅把区间求解得更精确，仍不能恢复 $y=n+2$ 。这里缺少的是关系表达能力。

整数假设同样是证明的一部分。如果允许有理输入 $n=1/2$ ，程序一次循环后以 $i=1,y=3$ 退出，却有 $n+2=5/2$ 。此时严格 guard 不能改成 $i-n\le-1$ ，原来的保持证明不再成立。实数时钟的严格界通常要在 DBM 中另存开闭标记，不能套用此页的整数转换。

推论与应用

从可计算接口到能力边界

本例展示一个完整验证链：初始化确定 $H_0$ ，guard 与赋值产生 $H_1$ ，raw widening 产生并稳定于 $W$ ，归纳保持覆盖全部循环头状态，退出闭包最后推出断言。对这个循环，还可另用自然数变式 $n-i$ 证明终止：真 guard 下它至少为一，每轮严格减一。安全性证书与终止证明承担不同任务。

DBM 适合差值有界、计数器同步增长、索引相对偏移等性质，但不能精确表示一般的 $x+y\le c$ 或 $y=2x$ 。八边形抽象域扩展到 $\pm x\pm y\le c$ ，通过带符号坐标与强闭包保存和式关系，并给出 $x+y\le4$ 的 guard 后执行平移、证明断言的完整矩阵例子；整数八边形还涉及紧闭包。多面体域允许任意线性系数，表达力更强，代价与实现接口也随之改变。它们不是把 DBM 的同一闭包公式原样复用即可得到的扩展。

若把矩阵常数改成有理数，有限差分约束的闭包与这些精确 transfer 仍可讨论，但不能据此断言有理端点域自动对所有具体集合存在最佳抽象。例如有理数集合中趋近某个无理上界的序列，没有最小的有理上界。本文的整数端点选择避开了这一任意上确界问题。

参考资料

Antoine Miné, “A New Numerical Abstract Domain Based on Difference-Bound Matrices”, 2001；此处采用 arXiv cs/0703073v2，2007-03-16 上传版。§§2–3、Theorems 1–4 给出表示与规范化；§4、Theorems 5–7、Definitions 12、14 给出域操作与转移；§5、Theorem 15 的完备性陈述须注意整数、实数与有理数端点的区别。论文把一般定理的详细证明指向另文；上文独立展开的是本例的集合包含与归纳证书。
Antoine Miné, “Tutorial on Static Inference of Numeric Invariants by Abstract Interpretation”, Foundations and Trends in Programming Languages 4(3–4), 2017，作者版印刷页 125–139，§§5.4.1–5.4.5、Theorem 5.2、Example 5.18。重点参照闭包、最佳 zone join、精确赋值和 widening 历史不可随意规范化的条件。