区间分析（interval analysis）目标是计算每个整数类型的变量所有可能值的上界和下届。区间分析的结果很有用，因为sound的结果可以用于代码优化、缺陷检测，例如：数组越界，值溢出，或者整数表示。

    区间分析的格是无限高度，因此我们必须采取一些特殊的技术确保分析的结果趋向于不动点。

用于描述一个抽象值的格定义如下（叫做区间 interval）：

$$ Intervals = lift(\{ [l,h]~|~l,h \in N \wedge l \leq h \}) $$

其中，N是无穷的整数集合；并且区间的偏序关系定义如下：

$$ [l_1,h_1] \sqsubseteq [l_2,h_2] \Longleftrightarrow l_2 \leq l_1 \wedge h_1 \leq h_2 $$

因此，格看起来如下图：

这个格具有无限的高度，因为它可以包含如下无限长度的偏序关系链：

$$ [0,0] \sqsubseteq [0,1] \sqsubseteq [0,2] \sqsubseteq [0,3] \sqsubseteq [0,4] \sqsubseteq [0,5] \sqsubseteq ... $$

基于以上的定义，我们可以给出抽象状态的格：

$$ States = Vars \rightarrow Intervals $$

    在我们定义约束规则之前，我们先定义一个eval函数，这是一个辅助函数，用于对表达式在抽象域的计算：

二元表达式的抽象计算符号定义如下：

例如，（两个区间的加法）$\hat{+}([1,10],~[-5,7]) = [1-5,10+7] = [-4, 17]$

    在第12章，我们将提供对soundness和精度更加形式化的描述。区间分析的JOIN函数与前向分析一致：

$$ JOIN(v)=\bigsqcup_{w \in pred(v)} ~ [[w]] $$

我们可以定义赋值语句的约束规则：