为了能够让6.1节的区间分析能够收敛,我们需要使用一种叫做widening的技术(翻译为放宽)。这项技术通常适用于如何“可以使用单调方程系统表达的分析“,但它通常用于具有无限高度格子的流敏感分析。

    令函数$f:L \\rightarrow L$ 表示4.4节中不动点理论与朴素不动点算法的计算函数。一个典型的、在实践中足以适用的widening方法,是引入一个函数$\\omega:~L \\rightarrow L$,那么计算的顺序

$$ (\omega~\circ~f)^i~(\bot)~ \text{for} ~ i = 0,1,\dots $$

则能够确保保证会收敛到一个大于或者等于朴素不动点算法中每个近似$f^i(\bot)$的不动点结果。因此widening之后的结果,是关于程序的sound的结果。为了确保这一性质,只需要
$\omega$ 是单调且广义的(参见练习4.18),以及 $\omega(L) = \{ \omega(x) | x \in L\}$ 具有有限高度。不动点算法,可以很容易的扩展到使用widening技术,只需要在每次迭代中使用 $\omega$ 加宽(widening)。

    加宽函数 $\\omega$ 在直观上将信息放宽到足够程度以确保终止。对于我们的区间分析,$\\omega$ 被点对点地定义为单个区间。放宽操作的对象是结合$B$,该集合由一组有限整数以及 $\\infty$ 和 $-\\infty$ 组成。通常,B由程序中出现的所有整数常量以及无穷来构成;其他的启发式的构成也可以。对于单个区间,我们定义放宽函数 $\\omega':~Intervals \\rightarrow Intervals$如下:

Untitled

这样就能找到能够满足条件的最优的区间结果。

    如6.1节所描述,朴素的不动点算法中区间分析的格为$L = States^n = (Vars \\rightarrow Intervals) ^ n$ ;其中n是程序控制流图G的所有节点的个数。对于放宽函数 $\\omega: ~ L \\rightarrow L$,那么一个简单的应用具体的 $\\omega'$ 到具体抽象状态的区间结果则为:

Untitled

    放宽不仅对于具有无限高度的格有用;它还可以当做一种加速技术,在可以容忍精度损失的分析中,适用于具有有限高度格,但收敛速度过慢的情况。

    放宽通常会超过目标,但后续的一种称为收缩(narrowing)的技术可能会改进结果。收缩只是计算 $f(f_\\omega)$,其中$f_\\omega$是使用加宽进行分析的结果。根据练习6.5,$lfp(f) \\sqsubseteq f_w$,换句话说$f(f_\\omega)$ 至少同 $f_\\omega$ 一样精确。此外,根据单调性f(f(fw) ≤ f(fw),所以f(fw)是一个不动点。换句话说,$f(f_\\omega)$ 是lfp(f)的一个安全的近似结果。这个收缩技术可能需要无数次迭代。

    放宽和收缩的一个例子如下:
y = 0; x = 7; x = x+1;
while (input) {
	x = 7;
	x = x+1;
	y = y+1;
}

如果没有widening技术,对于while-loop之后的程序点,朴素的不动点算法会产生如下发散的近似结果:

Untitled

如果我们采用放宽技术,根据(程序有的常量以及无穷)集合$B = \{ -\infty,0,1,7,\infty \}$,我们可以得到收敛的序列:注意这里x是7到无穷,因为存在widening,两边都要变化

Untitled

然而这个结果中,x的值令人不满意。但是在采用收缩技术之后,几个迭代之后就能够快速的提升结果为

Untitled

    这个分析结果是这个例子的理想结果。因此,继续做narrowing没有效果。然而,通常情况下,降序