论文部分内容阅读
在高度依赖软件的信息时代，程序的正确性验证问题需要深入研究。文中提出了基于抽象解释和数值熵的数值程序正确性分析方法。抽象解释理论为程序静态分析提供了一个通用框架，在编译时能够自动地推导程序的动态性质。数值信息熵能够反映变量的值范围，通过熵值的大小可以判断变量取值是否在规定范围内。通过一个C程序对该方法进行了验证，该数值程序分析方法可以做到对程序正确性等的验证，并且较单纯地抽象解释近似分析，正确性、可靠性更高。