单元赋值语句型循环不变式的开发方法研究

《单元赋值语句型循环不变式的开发方法研究》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、万方数据独创性声明本人声明所呈交的学位论文是本人在导师指导下进行的研究工作及取得的研究成果。据我所知，除了文中特别加以标注和致谢的地方外，论文中不包含其他人已经发表或撰写过的研究成果，也不包含为获得或其他教育机构的学位或证书而使用过的材料。与我一同工作的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表示谢意。学位论文作者签名：签字日期：年月日学位论文版权使用授权书本学位论文作者完全了解江西师范大学研究生院有关保留、使用学位论文的规定，有权保留并向国家有关部门或机构送交论文的复印件和磁盘，允许论文被查阅和借阅。本人授权江

2、西师范大学研究生院可以将学位论文的全部或部分内容编入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。(保密的学位论文在解密后适用本授权书)学位论文作者签名：签字日期：年月日导师签名：签字日期：年月日万方数据摘要“软件危机"的出现，对于软件的可靠性和生产效率提出了更高的要求，形式化开发软件是一个很好的解决办法。而形式化开发软件就是要保证能对算法程序进行正确的推导和证明。而循环不变式是算法程序进行推导和证明的基石。任何一个循环程序都存在一个循环不变式，它在循环执行前和每次迭代后都能成立，当达到循环退出条件

3、时，它产生了循环的最后结果。然而循环不变式无论是手工开发，还是自动构造一直都是一个巨大的挑战。本团队承担了国家自然科学基金重大国际合作项目：若干软件新技术及其在PAR平台中的实验研究。其中研究方向之一就是循环不变式的构造和自动探测。本文首先分析了国内外对循环不变式的定义及其开发方法的研究现状。然后介绍了本团队基于问题求解序列递推关系的循环不变式开发方法。接着介绍单元赋值语句型循环不变式的开发方法：按照PAR方法中的循环不变式开发策略，首先开发出抽象的单元赋值语句型循环程序的循环不变式，即抽象的单元赋值语句型循环不变式，并用Di

4、jkstra最弱前置谓词方法进行了形式化的证明，然后对于具体的单元赋值语句型循环程序，将其对应的抽象的单元赋值语句型循环不变式进行参数实例化即可得到所需的单元赋值语句型循环不变式。最后在本研究团队已有循环不变式自动生成系统中实现了单元赋值语句型循环不变式的自动生成。本文的创新点有如下3个方面：1．对单元赋值语句和单元赋值语句型循环程序进行了抽象，使得该方法具有一定的普遍性和典型性。2．运用Dijkstra最弱前置谓词方法对开发出的抽象的单元赋值语句型循环不变式进行了形式化证明。3．在本研究团队已有的循环不变式自动生成系统上扩充

5、实现了单元赋值语句型循环不变式的自动生成。关键词：循环不变式；PAR方法；单元赋值语句；Dijkstra最弱前置谓词方法万方数据AbstractAsme”So脚arecrisis”appears，itputsforwardhigherrequirementsforthereliabilityandproductivity．Formalsoftwaredevdopmemisagoodsolution·Ihef0如试softwaredevelopmentistoderivateandprovealgorithmicprogramp

6、roperly·The100piIlv￡匝antisthecornerstoneofthederivationandproofofalgorithmicDro阻锄．Attheheartofeveryloop，andhenceofallalgorithms，liesaloopinvariant：apropertyensuredbytheinitializationandmaintainedbyeveryiteration，soⅡlat，Whencombinedwiththeexitcondition，ityieldstheloo

7、p’sfinaleffect．HoWever，itisalwaysahugechallengetogetloopinvariantseithermanuallyora_utomatically．OurteamundertooktheNationalNaturalScienceFoundationofmajorinternationalcooperationprojects：ResearchOnSeveralNewSo凰艘Tecl血quesaIldTheirExperimentinPARPlatform，oneofwhichis

8、constructionandautomaticdetecionofloopinvariants．Thispaperanalyzestheresearchstatusonthedefinitionandmethodsofdevelopingloopinvariantsatho