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

发布时间：2022-09-17 19:19

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

【文章页数】：55 页

【学位级别】：硕士

【文章目录】：
摘要
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 工作展望
参考文献
成果目录
致谢


【参考文献】：
期刊论文
[1]数据流分析方法[J]. 李慧贤,刘坚.  计算机工程与应用. 2003(13)
[2]程序形式化验证中的两个基本问题[J]. 杨淑群,章仕昌.  上饶师范学院学报(自然科学版). 2002(06)
[3]上下文敏感的过程间指针分析[J]. 黄波,臧斌宇,韦俊银,朱传琪.  计算机学报. 2000(05)
[4]谓词逻辑在程序正确性证明中的应用[J]. 黄万徽.  高等函授学报(自然科学版). 1997(06)
[5]一个过程间数据流分析的框架[J]. 郁卫江,朱根江,谢立.  软件学报. 1997(09)
[6]过程间的数据流分析技术[J]. 刘磊,叶晓煜.  计算机研究与发展. 1997(04)
[7]软件测试是软件质量保证的重要手段[J]. 牟光灿.  计算机应用研究. 1997(02)

博士论文
[1]具有可适应性的程序分析技术[D]. 连瑞琦.中国科学院研究生院（计算技术研究所） 2000



本文编号：3679798