循环不变式自动探测

《循环不变式自动探测》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、分类号：密级：学校代码：10414学号：2014160004硕士研究生学位论文循环不变式自动探测theAutomaticDetectionofLoopInvariant院所：计算机信息工程学院导师姓名：钟林辉薛锦云学科专业：计算机技术研究方向：软件形式化与自动化二〇一七年六月万方数据独创性声明本人声明所呈交的学位论文是本人在导师指导下进行的研究工作及取得的研究成果。据我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发表或撰写过的研究成果，也不包含为获得或其他教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中

2、作了明确的说明并表示谢意。学位论文作者签名：签字日期：年月日学位论文版权使用授权书本学位论文作者完全了解江西师范大学研究生院有关保留、使用学位论文的规定，有权保留并向国家有关部门或机构送交论文的电子版和纸质版，允许论文被查阅和借阅。本人授权江西师范大学研究生院可以将学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。（保密的学位论文在解密后适用本授权书）学位论文作者签名：导师签名：签字日期：年月日签字日期：年月日万方数据摘要保障软件的可靠性一直以来都是软件开发的热点问题，而采用形式化方法来开发软件是保障软件可靠性

3、的有效方法，其中形式化开发软件的关键是对算法程序中循环语句的分析与验证。而要很好的理解循环程序，其重点是要能正确的写出该循环程序的循环不变式。循环不变式无论是手工开发，还是自动构造一直都是算法程序设计领域中最具挑战性、最富有创造性、也是最困难的问题之一。本文是国家自然科学基金面上项目“新概念循环不变式及其自动探测技术研究”的研究方向之一。本文首先分析循环不变式现有定义及其开发技术的国内外研究现状。之后介绍PAR方法中关于循环不变式的新定义及新的开发策略，也是本文构造循环不变式的指导思想。接着介绍单元赋值语句型循环不变式的概念，并在本团队已有的循环不变式生成系统的

4、基础上，分析单元赋值语句的算法程序的循环不变式的构造过程，发现有一类单元赋值语句型的算法程序，在分划过程中其分划后的子问题与原问题的结构不相同。对于此类单元赋值语句型的算法程序，提出一种使用全称量词的方式来刻画此类单元赋值语句分划过程中的不变性，进而构造循环不变式。最后使用Java语言实现单元赋值语句型循环不变式自动探测，并用Isabelle定理证明器对自动构造的循环不变式进行机械的证明，相对于传统的手工验证，具有更高的可靠性。主要创新点包括以下3个方面：（1）对于一类单元赋值语句型的算法程序在分划过程中其分划后的子问题与原问题的结构不相同的情况，提出一种使用全

5、称量词的方式来刻画其分划过程中的不变性，进而构造其循环不变式。（2）使用Java语言实现循环不变式的自动探测系统，并且增加了while循环程序的自动探测。（3）运用定理证明器Isabelle对开发出的单元赋值语句型循环不变式进行形式化正确性证明。关键词：PAR方法；循环不变式；单元赋值语句；IsabelleI万方数据AbstractThereliabilityofthesoftwarehasalwaysbeenahotissueinsoftwaredevelopment,andtheuseofformalmethodstodevelopsoftwareisane

6、ffectivewaytoprotectthereliabilityofsoftware,inwhichthekeytothedevelopmentofsoftwareistheanalysisofthecirculatorystatementsinthealgorithmverification.Andagoodunderstandingofthecycleoftheprogram,thefocusistobeabletocorrectlywritethecycleofthecycleoftheinvariant.Itisoneofthemostchallen

7、ging,themostcreativeandthemostdifficultproblemsinthefieldofalgorithmprogramming,whetheritismanualdevelopmentorautomaticconstruction.Thispaperisoneoftheresearchdirectionsofthe"NewConceptCirculationInvariantandItsAutomaticDetectionTechnology"projectoftheNationalNaturalScienceFoundation

8、.Inthispaper