为了利用条件中可用的信息，我们将扩展语言以包含一个人工语句，即${assert(E)}$，其中E是一个布尔表达式。如果E为false，这个语句将在运行时中止执行，否则不产生任何影响，然而，我们只会将它插入到E被保证为true的地方。在区间分析中，这些新语句的约束将通过利用条件中的信息来缩小各个变量的区间。

    对于示例程序，条件语句的含义可以通过以下程序转换来编码：

x = input;
y = 0;
z = 0;
while (x > 0) {
  assert(x > 0);
  z = z+x;
  if (17 > y) { assert(17 > y); y = y+1; }
  x = x-1;
}
assert(!(x > 0));

在这里，我们还使用了一个一元取反操作符”!”来扩展了TIP。忽略assert语句总是安全的，这等于采用了这个简单的约束规则：

$$ [[assert(E)]] = JOIN(v) $$

采用这个约束规则并不会获得额外的精度。为了对断言定义非平凡且正确的约束，需要深入了解具体的静态分析。

    对于区间分析，从一般条件或谓词（例如E1 > E2或E1 == E2）中提取相对于格元素的信息是复杂的，本身是一个被广泛研究的领域。为简单起见，让我们只考虑两种类型的条件，即X > E和E > X。前一种类型的断言可以通过以下约束规则处理：

否定条件以类似的方式处理，而所有其他条件默认都采用平凡的约束。

    由于该分析现在考虑了分支条件中的信息，这种类型的分析被称为控制敏感分析（或分支敏感分析）。控制敏感性的另一种方法，不涉及assert语句，是使用两个约束变量而不是一个来模拟CFG中的每个分支节点，对应于分支条件评估的两种不同结果。另一种方法是将数据流约束与CFG的边相关联，而不是与节点相关联。这些方法的技术细节与本文所采用的方法将有所不同，但总体思路是相同的。