逻辑表达式型似然不变量的分析与检测

论文摘要

迄今为止,计算机软件系统虽然仅仅只有短短的几十年历史,但是已经成为最广泛、最重要的应用系统之一。从而软件的质量成为人们目前广泛关注、高度重视的热点问题之一。众所周知,基于合约的程序设计是提高软件质量的一种重要的技术,但是合约的形式化制定是一项比较艰巨的任务。然而经过研究发现,程序不变量的动态生成技术是解决合约形式化制定的一项有效方法。利用程序不变量动态生成技术,可以进行程序不变量的动态检测,分析程序各变量之间的关联属性,从而有助于设计高质量的程序架构以及规范程序代码。本文通过分析得到了逻辑表达式型似然不变量的类型,提出了一种程序不变量动态检测方法。针对程序不变量动态生成理论、方法和技术进行了阐述;重点对逻辑表达式型似然不变量进行了分析,提出了逻辑表达式型似然不变量的表现形式,基于数据库的理论提出了一种新的逻辑表达式型似然不变量动态检测的技术和检测方法。本文的不变量检测技术通过数据库中提供的SQL条件查询功能,灵活多变地检测各种逻辑表达式型似然不变量,并且可以根据用户的实际需要随时指定新的程序不变量查询条件。最后,本文分析和设计了一个逻辑表达式型似然不变量原型系统。该系统具有两大特色:第一,基于关系数据库技术,具有良好的可扩展性;第二,使用SQL条件查询功能实现逻辑表达式似然不变量检测,检测方法具有很好的灵活性。

论文目录

• 摘要
• ABSTRACT
• 插图索引
• 附表索引
• 第一章 绪论
• 1.1 研究背景
• 1.2 程序不变量动态发现的相关研究
• 1.3 论文的研究目标、主要内容以及研究意义
• 1.4 论文组织结构
• 第二章 基于合约的程序设计
• 2.1 引言
• 2.2 合约式程序设计
• 2.3 程序不变量发现技术
• 2.3.1 程序不变量类型
• 2.3.2 程序不变量检测流程
• 2.3.3 程序不变量动态生成技术理论模型
• 2.4 小结
• 第三章 逻辑表达式型似然不变量分析
• 3.1 逻辑表达式型似然不变量的表现形式
• 3.2 逻辑表达式型似然不变量表达式发现
• 3.2.1 具体表达式的发现
• 3.2.2 具体表达式发现的分析
• 3.2.3 不变量表达式发现实验
• 3.3 小结
• 第四章 逻辑表达式型似然不变量检测
• 4.1 轨迹文件
• 4.2 逻辑表达式型似然不变量检测流程
• 4.3 小结
• 第五章 原型系统分析与设计
• 5.1 系统功能分析
• 5.2 系统设计
• 5.3 不变量检测详细流程
• 5.4 小结
• 第六章 总结与展望
• 6.1 工作总结
• 6.2 工作展望
• 参考文献
• 成果目录
• 致谢