形状图逻辑扩展的实现

《形状图逻辑扩展的实现》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、陈专絮———————————————————————————————————————————————————————乏；坼暨．)广中国科学技术夫学硕士学位论形状图逻辑扩展的实现作者姓名：学科专业：导师姓名：完成时间：韩亚慧计算机软件与理论陈意云教授二。一四年五月文UniverSitVOfSCienCeand-r_eChnOIOgVOfChinaUnIVerSltVOTSCIenCeanaIeCnnOIOgVOTUnInaAdiSSertatiOnfbrmaSter’SdegreetheImpIementa

2、tiOnOfExpanSiOnfOrShapeGraphLogicAu恤or’sName：Yj也uiHanSpecial埘：Supervisor：”o’1』’fm1Snedtlme：ConlputerSof叭areandTheoryPro￡YiyunChenMay，2014中国科学技术大学学位论文原创性声明本人声明所呈交的学位论文，是本人在导师指导下进行研究工作所取得的成果。除已特别加以标注和致谢的地方外，论文中不包含任何他人已经发表或撰写过的研究成果。与我一同工作的同志对本研究所做的贡献均已在论文中作了

3、明确的说明。作者签名：叠里堇签字日期：垫!生!篁!驾中国科学技术大学学位论文授权使用声明作为申请学位的条件之一，学位论文著作权拥有者授权中国科学技术大学拥有学位论文的部分使用权，即：学校有权按有关规定向国家有关部门或机构送交论文的复印件和电子版，允许论文被查阅和借阅，可以将学位论文编入有关数据库进行检索，可以采用影印、缩印或扫描等复制手段保存、汇编学位论文。本人提交的电子文档的内容和纸质论文的内容相一致。位论文在解密后也遵守此规定。口保密(——年)作者签名：塾垒鐾聊弛噬主堂导师签名：l■!＆兰签字日期：塑

4、!±：竺：兰l签字日期：221擎jc：当F摘要信息时代的发展，引领计算机软件应用深入到千家万户，各行各业。随着软件的应用领域迅速加大，规模急速扩张，软件安全性的要求也逐步提升，软件调试和维护的成本越来越高，软件的安全形势日渐严峻。基于逻辑推理的形式验证是提高软件可信程度的一种重要方法。进入21世纪来，国际国内对该方法的推广和工业应用进行了大量的研究与开发，本实验室(中科大一耶鲁高可信软件联合研究中心)在并行程序的验证方法和串行程序的验证工具的研发工作也相当活跃。本文工作基于一个类c小语言Pointe妃的程

5、序验证器原型。它是研究操作易变数据结构的指针程序的验证的试验性工具。本文对此验证器进行了两方面扩展，一是使验证器可以更好地用于一维数组程序的验证。二是使验证器能用于操作带附加单链表的数据结构的程序的验证。本文的主要贡献如下：第一，设计并实现了对一维数组元素进行赋值的语句的推理规则，并将此规则延伸应用到全称量词的约束变元出现在访问路径的上角标中的情况。原型系统虽然主要是针对指针程序设计的，但同时也考虑了操作其他数据类型的程序的验证，比如操作数组的程序的验证。操作一维数组的程序中，数组的很多性质需要使用量化断

6、言(如全称断言)来描述。这样在遇到数组元素的赋值语句时，在运行赋值公理时需要使用本文设计的规则对量化断言进行展开。同理，此规则也适用在验证包含带上角标表达式的全称量词的程序中。第二，设计并实现了一种操作带附加链表的数据结构的程序的验证方法。在形状分析时，若想让附加链表指针指在主数据结构的节点上，则不可能进行精确的指针分析，导致基于精确指针分析的形状图逻辑不能使用。本文设计的解决方法是，将附加链表从主数据结构的形状图中分离出来，建立分离的虚拟附加链表。通过上述对原型系统中形状图逻辑的扩展，使得系统原型能够验

7、证复杂的一维数组程序和包含带上角标表达式的全称量词的程序，并能验证操作带附加单链表的数据结构的程序，扩展了原型系统的验证范围。关键词：形式验证形状图逻辑推理规则全称量词附加单链表摘要IIAbs仃actAbStradThedeVelopmentoft11ei耐．onnationageleadssoRwareapplicationstoevery缸1ilya11da11worksof1ife．Wi廿ltllerapidexpallsionofme啪gea11dscaleofsoRwareapplication

8、s，t11erequireInemforsoRwarese阢血tyisimpro啊ng．TheincreasingofmecostforsofhⅣaretestingandmaintenaIlcemademeso凤rafesecuritymore油portant．ThefomlalverijEicationbaSedonlo垂cal协f．erenceisanimportantmethodtoimproVemesoRwarere