形状图理论定理证明及其在指针程序验证中应用论文

《形状图理论定理证明及其在指针程序验证中应用论文》由会员上传分享，免费在线阅读，更多相关内容在学术论文-天天文库。

1、㈣㈣㈣㈣㈣Y2354§§葺UniversityofScienceandTechnologyofChinaAdissertationformaster’SdegreeAutomaticTheoremProvingforShapeGraphLogicAnd‘■■。o●I■一APP¨cationInPoInterProgramVerificationAuthor’SName：Speciality：Supervisor：Finishedtime：YanhuiSongComputerSottwareandTheoryProf．YiyunChenApr22也，2013中国科学技术大学学

2、位论文原创性声明本人声明所呈交的学位论文。是本人在导师指导下进行研究工作所取得的成果·除己特别加以标注和致谢的地方外，论文中不包含任何他人已经发表或撰写过的研究成果。与我一同工作的同志对本研究所做的贡献均已在论文中作了明确的说明。作者签名：弛中国科学技术大学学位论文授权使用声明作为申请学位的条件之一，学位论文著作权拥有者授权中国科学技术大学拥有学位论文的部分使用权，即：学校有权按有关规定向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借阅，可以将学位论文编入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。本人提交的电子文档的内容和纸质

3、论文的内容相一致。保密的学位论文在解密后也遵守此规定。，窗公开口保密(——年)作者繇龇导师虢：隘受!堂签字日期：塑』；：!：!!签字日期：2△【；．5：z1．摘要随着信息时代的到来和深入，计算机技术已经在各行各业中得到了广泛地应用。但随着计算机软件系统的普及和规模的不断增大，其安全性问题也越来越突出。提高软件可靠程度的方法有很多，形式程序验证是其中一个重要的方法。。基于逻辑推理是程序验证中最严格也最可靠的，它根据特定的程序逻辑通过形式化的数学推导演算，并利用定理证明工具来证明。但由于自动推断循环不变式困难、断言语言表达力弱以及自动定理证明能力有限等诸多原因，形式程序验证尚未

4、在工业界得到应用。本文的工作建立在一个基于形状图逻辑的自动程序验证原型系统上，主要用于指针程序的验证。该验证过程主要分成两个阶段：第一阶段是对指针程序进行形状分析，第二阶段是利用形状分析得到的结果进行程序验证。其中，形状分析阶段使用形状图逻辑和形状系统，实现了循环不变形状图的自动推断，并且对于非递归函数可以推断出函数前后形状图。本文主要的研究工作是形状图理论的定理证明及其在指针程序验证中的应用。形状图理论主要包括形状图重写系统、形状图等价判定方法和形状图蕴涵判定方法；形状图理论在指针程序验证中的应用主要包括对循环不变形状图和递归函数前后形状图的推断。通过对系统原型做扩展之后

5、，系统能够验证带递归的指针程序。本文的主要贡献是：第一，设计并实现了形状图理论的判定方法。形状图及其等价变换规则和蕴涵变换规则可分别类比为代数项及其等式规则和重写规则，因而可像研究代数规范的理论那样来研究形状图理论。我们定义了形状图重写系统及其终止性、局部合流性和合流性等概念，最后得到基于形状图重写的形状图等价判定和蕴涵判定的方法。第二，设计并实现了指针类型递归函数前后形状图的自动推断方法。该自动推断方法源子一个通过迭代推断循环不变式的一般方法，并借助了上述形状图理论的判定方法。该方法的实现使得原型系统能够用于指针类型递归程序验证。通过上述方法的实现以及对系统原型其他地方的

6、完善，系统原型能够验证平衡二叉排序树和自顶向下伸展树等复杂的易变数据结构的程序。关键词：程序验证形状图逻辑形状分析自动定理证明不变式的自动推断I摘要IIAbstractWiththearrivalofinformationage，computertechnologyhasbeenwidelyusedinallaspectsoflife．Withthepopularityofcomputersoftwaresystemsandscaleofincreasing,itssecurityissuesbecomeincreasinglyprominent．Therealemanyw

7、aystoimprovesoftwarereliabilityandformalprogramverificationisoneofthemostimportantways．Basedonlogicalreasoning，programverificationisthemostdemandingandthemostreliable，accordingtoformalmathematicalcalculationsandtheoremprovingtools．Ⅵ／hileautomaticallyinferringl