论文研究-基于抽象域和数值熵协同的数值程序分析.pdf

在软件日益丰富的信息时代，程序的正确性验证问题需要深入地研究。提出了基于抽象解释和数值熵协同的数值程序正确性分析方法。利用抽象解释理论框架对数值程序进行抽象解释分析，提取不变量的抽象域区间；在抽象域区间上进行数值熵运算；运行程序获取数值变量的实际取值，计算数值熵；将抽象域区间数值熵和实际数值熵信息进行对比分析，准确地判断程序的正确性等性质。单纯的抽象解释分析只可以近似得到数值变量的取值范围，而引入数值熵算法，在取值范围的基础上对程序静态分析的准确性进一步检验，同时也做到了对程序的正确性验证。通过C语言程序实例，对抽象解释基础上的熵值分析方法进行了验证，证明了该分析方法的可行性和正确性。