一元多项式不等式似然不变量检测方法研究

摘要

计算机技术发展至今，计算机软件系统虽然只经历了短短的几十年历史，但其在社会各个行业得到了极其广泛的应用，如医疗卫生、航空航天、核电站控制等等。同时，人们对软件的质量和安全有了更为广泛和热切的关注。如何提高软件质量，成为人们研究的热点，并取得了一定的成绩。基于合约的程序设计是提高软件质量的一种重要技术，且得到了非常广泛的发展和应用。合约描述了程序内部的基本属性，运行的先决条件以及期望的运行结果。从不同的层面合约可分为语法合约、数据合约、行为合约和服务合约。程序不变量一般包含类不变量、前置条件和后置条件，它是一种基本的合约。程序不变量对于程序演进与重构、程序测试与排错、辅助定理证明、构件升级替换都有重要作用。通过分析关键点上的不变量，可以检测到程序运行中的异常。程序不变量的动态生成技术是解决合约形式化制定的一种有效方法。程序不变量动态生成技术，可以进行程序不变量的动态检测，分析程序各变量之间的关联属性，是提高程序质量和规范程序代码的关键。
　　本文重点研究了如何使用动态检测技术发现程序中的一元多项式不等式似然不变量。论文首先介绍了基于合约的程序设计，由此引出了程序似然不变量动态检测技术。接着重点介绍了程序似然不变量动态检测技术及其主要的实现工具Daikon,并分析了Daikon在不变量检测方法上存在的不足之处。然后针对现存不变量检测工具的缺陷，提出了一元多项式不等式似然不变量发现规则和检测算法，用实验验证了检测算法对于一元多项式不等式似然不变量检测的有效性，并与Daikon不变量检测工具进行了比较，实验结果表明本文检测算法明显优于Daikon。文章的最后设计并实现了一个不变量检测工具，该检测工具具有易用、灵活等特点。用户可以根据自己的需要定义要观测的变量。

目录

封面

声明

目录

中文摘要

英文摘要

插图索引

附表索引

第一章 绪论

1.1 研究背景

1.2 程序不变量动态发现的相关研究

1.3 论文的研究目标、主要内容及意义

1.4 论文组织结构

第二章 基于合约的程序设计

2.1 引言

2.2 程序分析技术

2.3 JAVA建模语言

2.4 合约式程序设计

2.5 小结

第三章 程序似然不变量动态检测技术

3.1 程序似然不变量检测技术

3.2 Daikon

3.3 相关工作

3.4 小结

第四章 一元多项式不等式似然不变量检测

4.1 引言

4.2 一元多项式不等式似然不变量性质分析

4.3 一元多项式不等式似然不变量检测

4.4不变量检测实验

4.5多元多项式不等式似然不变量检测

4.6 小结

第五章 原型系统设计与实现

5.1不变量检测原型设计

5.2 原型系统实现

5.3 小结

第六章 总结与展望

6.1 工作总结

6.2 工作展望

参考文献

成果目录

致谢