一个基于两区间八边形约束的抽象域

　　抽象解释静态程序分析技术用来发现运行时错误，保证程序正确性，已经被成功应用到工业界。抽象域是抽象解释理论中的一个重要方面，然而大部分已存在的数值抽象域无法表示程序的非凸性质，抽象域的这种凸性限制很多时候会影响数值分析的精度，甚至带来更多误报。基于两区间八边形约束，提出了一个新的数值抽象域，其约束形式为z±y∈［a，b］U［c，d］，其中z和y表示变量取值，a，6，c，d∈R。该抽象域的域元素是用两区间八边形约束表示，因此可以表达某类非凸性质，表达能力强于经典的八边形抽象域，并且相对于八边形抽象域，域操作的计算复杂度并没有提高太多。