Widening 与 Narrowing | Codeboy's Blog

形式陈述

在抽象域 $(A,\sqsubseteq)$ 上，二元操作 $\nabla:A\times A\to A$ 是 widening，若至少满足上界性

x\sqsubseteq x\nabla y,\qquad y\sqsubseteq x\nabla y,

并且对任意上升链 $x_0\sqsubseteq x_1\sqsubseteq\cdots$ ，序列

y_0=x_0,\qquad y_{n+1}=y_n\nabla x_{n+1}

在有限步后稳定。不同教材给出等价或更一般的序列式定义，核心都是“结果保持可靠上界”和“加速序列最终稳定”。

Widening 通常不是格 join，不要求结合、交换、幂等或单调。擅自依赖这些代数律会让 worklist 次序变化时出现未经证明的结果。

直觉

经典区间 widening 对 $[l_0,u_0]$ 与新值 $[l_1,u_1]$ 定义

[l_0,u_0]\nabla[l_1,u_1]=[l',u'],

其中若 $l_1<l_0$ 则 $l'=-\infty$ ，否则 $l'=l_0$ ；若 $u_1>u_0$ 则 $u'=+\infty$ ，否则 $u'=u_0$ 。

循环 x:=0; while (...) x:=x+1 的普通 join 迭代产生

[0,0],[0,1],[0,2],\ldots

永不有限稳定。首次增长时 widening 可从 $[0,0]$ 与 $[0,1]$ 跳到 $[0,+\infty]$ ，下一轮保持不变。

这个结果可靠却很粗。它不是“猜测真实上界无穷”，而是主动放弃不断移动的有限上界，以保证分析终止。

例子与边界

不必在每个控制流节点都 widening。常见策略只在循环头或反馈边使用，使无环区域仍以精确 join 传播。选取覆盖每个循环的 widening points 是终止证明的一部分。

可以先做若干普通迭代，再启用 widening；或采用 thresholds，只允许边界跳到程序常量 $10,100$ 后再到无穷。它们常提高精度，却需证明任何无限增长最终仍会越过有限阈值并稳定。

迭代次序会影响结果。两个语义等价的 CFG 排序可能触发不同 widening 时机，因此工程报告应说明策略，不把输出当成唯一最小解。

表示规范化也会影响终止论证。DBM 的逐项 widening要求左侧历史矩阵保持 raw：闭包副本可用于转移和性质检查，却不能每轮回写历史，否则被丢到无穷的界可能经其他路径重新出现。“每个有限界只删除一次”的证明只适用于未被这种规范化改写的历史序列。

推论与应用

得到归纳上界 $y$ ，即 $F^\#(y)\sqsubseteq y$ 后，可用 narrowing $\triangle$ 生成下降序列

z_0=y,\qquad z_{n+1}=z_n\triangle F^\#(z_n),

一种标准充分条件是 $F^\#$ 单调，且当 $v\sqsubseteq u$ 时满足 $v\sqsubseteq u\triangle v\sqsubseteq u$ ，并保证这里生成的下降序列有限稳定。若 $F^\#(z_n)\sqsubseteq z_n$ ，则

F^\#(z_{n+1})\sqsubseteq F^\#(z_n)\sqsubseteq z_{n+1},

所以每一轮仍是归纳上界；局部转移可靠性再保证它覆盖具体最小解。区间 narrowing 常把无穷端点替换为 transfer 计算出的有限端点。

若循环实际条件是 x<100，widening 得 $[0,+\infty]$ 后，guard 与一次或数次 narrowing 可能收紧到 $[0,100]$ 。narrowing 不保证回到最小不动点，也不能恢复 widening 丢掉的所有关系信息。

没有可靠上界就开始下降可能漏状态。顺序必须先获得这样的归纳上界，再在保真条件下改进；把 narrowing 当任意“优化结果”的后处理没有证明依据。

若所谓 widening 只返回第二个参数 $y$ ，它在上升链上是上界，却可能沿 $[0,n]$ 永不稳定，因此不是 widening。若返回第一个参数 $x$ ，会稳定但未必覆盖新状态，也不可靠。

过早 widening 到 $\top$ 会让分析快速终止，却可能产生大量假警报；过度延迟又可能耗尽资源。比较策略时，应同时记录迭代次数和最终能证明的性质，例如是否仍能验证数组下标有界。

有限高度域上，普通单调迭代已保证有限终止，因此 widening 不是理论终止所必需的。但高度很大时，它仍可用来减少迭代次数，只是可能损失精度；不能把“无需它证明终止”理解为“使用它必然错误”。

对嵌套循环，外层和内层 widening point 的调度会互相影响。内层尚未稳定就把粗结果送到外层，可能触发不可逆的无穷边界；完全求稳内层又可能重复昂贵计算。局部 WTO 等策略用控制流的嵌套结构规定更新次序，但每种策略仍需证明所有反馈环最终经过 widening 点。

整数八边形给出具体反例链：闭包回写令两个变量的绝对界交替增长为(2,1)、(2,3)、(4,3)、(4,5)，而保存raw历史在两轮删除绝对界后稳定，只留下差值界。这把表示纪律与终止性质的联系落实到可复算矩阵。

参考资料

Patrick Cousot and Radhia Cousot, “Abstract Interpretation: A Unified Lattice Model for Static Analysis,” POPL, 1977, pp. 238–252。
Patrick Cousot and Radhia Cousot, “Comparing the Galois Connection and Widening/Narrowing Approaches,” PLILP, Springer, 1992, pp. 269–295。
Xavier Rival and Kwangkeun Yi, Introduction to Static Analysis, MIT Press, 2020, Ch. 10。