论文部分内容阅读
浮点变量在程序中的取值范围对浮点程序中相关性质的分析及运行时错误的检查具有重要意义。浮点运算的不精确性使得浮点变量的值范围分析具有挑战性。抽象解释理论为程序变量的值范围分析提供了一个通用的框架。在抽象解释的框架下，提出了一个新的数值抽象域——区间幂集抽象域，即使用有限个区间的析取来刻画变量的取值范围。该抽象域的表达能力强于经典的区间抽象域，能够较好地刻画大部分已有抽象域不能表达的非凸性质，从而有效提高分析精度。在此基础上，给出了区间幂集抽象域的可靠浮点实现方法，阐述了如何应用基于该抽象域的浮点实现对浮点程