4.2.3 理论分析
区间是抽象解释中的一个经典概念,它是基于计算机系统语义模型对变量取值范围的近似表示,它被广泛地用于实际工程中分析变量的值范围。以下给出对区间的详细介绍。
定义4-6 给定a,b∈R∪{-∞,+∞},则[a,b]={x|x∈R∪{-∞,+∞},a≤x≤b}是一个有界闭区间,简称区间。a是区间[a,b]的下确界,b是上确界。如果a＞b,那么[a,b]是一个空区间,记为⊥i,[-∞,+∞]是最大的区间,记作⊥i。
一个区间实际上是一些取值范围的集合。例如,如果x是一个从-3到6的整数,且它不能为0,那么x的区间可以表示为[-3,-1]∪[1,6],它实际是两个取值范围的集合。所有区间的集合记作I tvs。
定义4-7 对于两个区间I 1=[a,b]和I 2=[c,d],定义偏序⊆i为I 1⊆
,当且仅当c≤a≤b≤d且[a,b]=⊥i。
定义4-8 对于两个区间I 1=[a,b]和I 2=[c,d],分别定义它们的交集和并集为式(4-4)和式(4-5)。(https://www.daowen.com)
上述定义是在实数域上的,如果将R替换为Z则上述定义也适用于整数。在计算机中,实数变量的表示实际上是离散的。如果用步长λ(λ＞0)来代表最小精度,那么对于整数,λ等于1。而对于浮点变量,λ是变化的。根据不同计算机的限制,开区间(a,b)可以被表示为一个闭区间[a+λ1,b-λ2]。对于整数来说,λ1和λ2都等于1,而对于浮点数来说,λ1和λ2是变化的。可以很容易地验证＜I tvs,⊆i,∪i,∩i,⊥i,⊥i＞是一个完全格,而图4-12是整数域的哈斯图。区间的运算遵循格的计算规则。
图4-12 整数域的哈斯图
如果将从路径入口(将所有变量的区间集记作D in)到出口(将所有变量的区间集记作D out)的区间运算看作一个函数,那么根据克纳斯特-塔斯基定理,这个函数将会迭代收敛至其不动点,这对于总是计算出比实际要大很多的区间运算来说是一个很大的优化。
