3.2.1 基于抽象解释的区间迭代优化策略
1.问题的提出
区间运算对于分支限界非常重要。不管是路径可达性判断还是赋值的判断,都需要调用区间运算。而分支限界由于涉及对于路径约束的精确分析,比CTS组的其他模块需要功能更强大的区间运算。实际上,预处理和状态空间搜索阶段都会用到区间运算。下面用一个例子来说明为什么对区间运算进行优化。
例3-1 不等式组
很显然A和B的解区间集都是{a:[2,+inf],b:[1,inf]}。如果将A、B两个不等式组作为分支限界的被测函数的控制条件,那么它们分别对应如下程序的所有if真分支经过的路径:
A组和B组经过区间运算所得到的最终结果是不同的,A组为{a:[-inf,+inf],b=[1,inf]},B组为{a;[2,+inf],b:[1,+inf]}。可以看出B组的结果更加精确,这是由于区间运算是按照先后顺序求解的,而A、B组的区别就在于两个约束条件的先后顺序不同。A组在第2行出现了b＞0的约束,而区间运算是顺序分析的,这个约束无法作用于第1行的a＞b,从而导致a的取值区间不够精确。如果不进行优化,在求解A组时会在空间{a:[-inf,1],b:[1,inf]}上浪费时间。
2.优化策略
下面结合分支限界搜索和区间运算的特点考虑算法优化的策略。由于搜索树上的每个状态都对应一个所有变量的稳定区间集,这个稳定区间集是通过区间运算判定是否包含有效解的。从一个状态到下一个状态之间,即从一个稳定区间集到下一个稳定区间集之间,可以进行多次迭代,每一次迭代生成的中间结果是两次稳定区间集之间的临时区间集。临时区间集中有可能出现区间为空的变量,从而导致路径不可达,其原因就是在当前稳定区间集中所选取的当前变量的赋值不是一个有效解,需要从稳定区间集中选择其他的值。
从区间运算的角度来说,由于每一次运算的初始条件作为上一次迭代的结果,是符合前一次顺序处理的结果的,因此在此次运算中,初始条件作为包含上一次顺序处理的约束而存在。如果其中某一步的区间运算给出的结果超出初始条件的范围,即为不满足上一次的约束,此结果就会被“剪枝”。迭代达到稳定即是到达了两次状态之间的不动点。同时,迭代的区间运算策略可以在算法执行前进行路径可达性的预判,对于不可达路径可以避免后续测试用例生成的无用功。简单来说,在顺序得到的区间运算给出的初步取值区间之后,将这些变量的取值区间作为下一次区间运算的输入进行迭代运算,如此循环,直至最终的区间不再发生变化。
定义3-8 (D 1,D 2,…,D n)0是在分支限界中所有变量赋值前预处理得到的各变量的区间集。
定义3-9 (D 1,D 2,…,Dn)i(i=1,2,…,n)是在分支限界中第i个变量赋值前各变量对应的区间集。
(1)(D 1,D 2,…,Dn)0→(D 1,D 2,…,D n)1:对(D 1,D 2,…,D n)0进行迭代的区间运算过程
①如果迭代达到稳定,将得到的稳定的区间进行区间初始化后得到的(D 1,D 2,…,D n)1作为分支限界的输入。
以例3-1中的A为例,预处理得到的初始区间(Da,Db)0是{a:[-inf,+inf],b:[1,+inf]},将此区间代入路径进行计算。
第1次迭代:
开始:{a:[-inf,+inf], b:[1,+inf]}
处理: b＜a 结果:{a:[2,+inf], b:[1,+inf]}
处理: b＞0 结果:{a:[2,+inf], b:[1,+inf]}
注:加粗字体为处理一条语句后区间发生变化的情况。
此次迭代的结果为{a:[2,+inf],b:[1,+inf]},与输入{a:[-inf,+inf],b:[1,+inf]}不同,将此次结果作为下一次的输入继续迭代。
第2次迭代:
开始:{a:[2,+inf],b:[1,+inf]}
处理: b＜a 结果:{a:[2,+inf],b:[1,+inf]}
处理: b＞0 结果:{a:[2,+inf],b:[1,+inf]}
此次迭代的结果为{a:[2,+inf],b:[1,+inf]},与输入{a:[2,+inf],b:[1,+inf]}相同,返回此次的结果。
可见此结果与约束条件
的解空间{a:[2,+inf],b:[1,+inf]}一致,消除了区间运算顺序处理的不足。
②如果经过迭代发生矛盾,则说明给定的路径区间有问题,在预处理阶段就判断路径为不可达路径,无法生成测试用例,提前退出分支限界。(https://www.daowen.com)
例3-2 void f(int a,int b){
对所有if真分支生成测试用例。
第1次迭代:
开始:{a:[-inf,+inf],b:[-inf,+inf]}
处理: b＞a 结果:{a:[-inf,+inf],b:[-inf,+inf]}
处理: b＜-4 结果:{a:[-inf,+inf],b:[-inf,-5]}
处理: a＞0 结果:{a:[1,+inf],b:[-inf,-5]}
处理: …; 结果:{a:[1,+inf],b:[-inf,-5]}
注:加粗字体为处理一条语句后区间发生变化的情况。
优化前的区间运算会将结果{a:[1,+inf],b:[-inf,-5]}作为(Da,Db)1给出,作为变量的取值范围进行测试用例生成。但是可以很明显地看到,{a:[1,+inf],b:[-inf,-5]}与第一个约束条件b＞a是矛盾的,因此无论怎么选值都不符合这个约束要求。当对区间运算进行优化之后,由于第一次的结果与输入不相等,因此还需要进行迭代。
第2次迭代:
开始:{a:[1,+inf],b:[-inf,-5]}
处理: b＞a 结果:{a:∅,b:∅}发生矛盾!
在初始区间迭代过程发生矛盾,这说明此路径为不可达路径,无法得到(D a,Db)1,直接进入不可达路径的处理流程,不再生成测试用例,省去了大量的工作。
(2)(D 1,D 2,…,D n)i-1→(D 1,D 2,…,D n)i(i=2,3,…n):对(D 1,D 2,…,D n)i-1进行迭代的区间运算过程
由于搜索中的每一个状态都对应一个区间运算不产生矛盾的最简区间集,并且这个最简区间集中一定是包含有效解的。从第一个最简区间集(D 1,D 2,…,Dn)1到下一个最简区间(D 1,D 2,…,D n)2之间需要经过多次迭代,每一次迭代生成的中间结果看作两次最简区间集之间的临时区间集。临时区间集有可能不可达,不可达的原因就是在最简区间集(D 1,D 2,…,Dn)1中,当前变量(假设x 1)的赋值不是一个有效解,所以需要从(D 1,D 2,…,D n)1中选择其他的值再进行试探。当i为3,…,n时,处理流程类似。一次迭代区间运算(Iterative Interval Arithmetic,IIA)的流程如图3-7所示。使用区间迭代优化策略的分支限界算法流程如图3-8所示,其中加粗部分为涉及迭代区间运算的部分。
3.理论分析
在迭代区间运算过程中,变量区间集是单调缩小的。这是由于每一次的区间运算都由初始值来限制,初始条件作为上一次迭代的结果,是符合前一次顺序处理的结果的,因此在此次区间运算中,初始条件作为包含上一次顺序处理的约束而存在。如果其中某一步的区间运算给出的结果超出初始条件的范围,即为不满足上一次的约束,此结果就会被“剪枝”。最终达到新的稳定区间集(D 1,D 2,…,D n)i+1∈(D 1,D 2,…,Dn)i(i=1,2,…,n-1)。这个过程可以用抽象解释中的Narrowing算子解释。
命题3-2 在每次迭代的区间运算中,变量的区间是单调缩小的。
证明 L是一个高度有限的格。需要为单调函数F找到一个收敛的递减序列{bn}。其中,L为区间抽象域,F为一次从入口到出口的路径分析,x n为每次作为输入的变量区间集,bn为顺次递减的稳定变量区间集。NarrowingΔ:L×L→L满足以下条件。
①x≤y→x≤xΔy≤y。
②对于任何递减的序列{x n}n,“narrowed”后的序列y n收敛:
y 0=x 0 y n+1=y nΔx n+1
也就是说,任何严格递减的序列{y n}都是有限的。
将每两次稳定区间(D 1,D 2,…,Dn)i和(D 1,D 2,…,Dn)i+1之间的临时区间temp Dj(j=1,2,…,m,假设迭代m次达到稳定)看作一个递减的序列,则在进行一系列的迭代之后到达的稳定区间就是经过收敛的序列极限值,即
(D 1,D 2,…,Dn)1=temp D 1 (D 1,D 2,…,D n)i+1=(D 1,D 2,…,Dn)iΔtemp D m
(D 1,D 2,…,Dn)i+1就是经过迭代后得到的稳定区间。
图3-7 一次区间迭代运算流程图
