区间抽象域

区间格与环境 ​

单变量区间域包含空元素 $\mathrm{\perp }$ 和端点位于 $\mathbb{Z}\cup \{-\mathrm{\infty },+\mathrm{\infty }\}$ 的区间 $[l,u]$。concretization 为

按集合包含诱导精度次序：

所以更窄区间更精确，$[-\mathrm{\infty },+\mathrm{\infty }]=\mathrm{\top }$。join 是最小区间外壳

多变量抽象状态是环境 ${\rho }^{\mathrm{\#}}:Var\to Interval$，次序和 join 逐变量计算。这是非关系抽象域公理库抽象域Abstract domain · Domain of abstract properties用带精度次序和合流运算的抽象元素表示具体状态集合，为可靠静态近似提供语义空间。。

transfer 与分支过滤 ​

赋值 x := y + z 使用区间算术公理库验证数值计算与区间算术Verified numerics · Validated numerics · Interval arithmetic用向外舍入的区间运算构造包含真实结果的可检查外包络，并分辨可靠包含与界的紧致程度。：

其他变量不变。对机器浮点程序，端点需向外舍入；对数学整数程序，则需处理无穷端点和语言溢出语义。

条件 x < c 的真分支可与 $[-\mathrm{\infty },c-1]$ 相交，假分支与 $[c,+\mathrm{\infty }]$ 相交。若交为空，该分支不可达；只传播原区间仍可靠但更粗。

乘法、除法和非线性函数要分别给 inclusion transformer。除数区间包含零时，返回一个普通有限商区间会漏行为；可返回 $\mathrm{\top }$、分裂状态或建模异常分支。

完整循环轨迹 ​

分析程序：

x := 0
while x < 10:
    x := x + 1
assert x == 10

循环头普通迭代依次得到

这次有限常量界使迭代最终停止，但若条件或上界未知，链可无限增长。使用区间 widening 时，首次上界增长可跳到 $[0,+\mathrm{\infty }]$。

真分支 guard 把它收紧到 $[0,9]$，执行加一得到 $[1,10]$，回到头部仍包含在 widened 结果内。退出分支以 $x\ge 10$ 过滤 $[0,+\mathrm{\infty }]$，得到 $[10,+\mathrm{\infty }]$；一次 narrowing 利用循环方程和 guard 可把头部恢复到 $[0,10]$，退出得到 $[10,10]$，从而证明断言。

每一步分别展示 join、guard、transfer、widening 与 narrowing，不能只报最终区间而隐藏为何可靠、何处损失精度。

相关性丢失的假警报 ​

若程序先令 y := x，区间环境只记录 $x,y\in [0,1]$，不记录 $x=y$。检查 assert x-y==0 时，自然区间减法得到

无法证明结果恒零。真实执行没有错误，警报来自变量相关性丢失。

把区间换成更高精度浮点端点不会恢复 $x=y$；需要等式、octagon、polyhedra 或 symbolic relation 等关系域。算术外包络的 tightness 与抽象域表达能力是两种误差来源。

分支拆分可以局部恢复精度，但路径数可能指数增长。区间域的价值正是低成本合流，不能同时承诺保留全部路径关系。

两层可靠性 ​

底层区间算术要证明每次机器端点运算向外包含精确数学结果。上层静态分析还要证明变量环境、guard、赋值、join 与循环求解覆盖所有语言执行。

底层可靠不代表上层自动可靠：若分析把有符号溢出当数学整数，仍会漏状态。上层 transfer 正确也不代表端点实现可靠：最近舍入可能把真实边界舍到区间内。

区间分析给出范围不变量，不证明程序终止、数组索引语义正确或模型与部署环境一致。每个结论应写出整数/浮点模型与异常规则。