形状图理论的定理证明

《形状图理论的定理证明》由会员上传分享，免费在线阅读，更多相关内容在工程资料-天天文库。

1、第３９卷第１２期计算机学报Ｖｏｌ．３９Ｎｏ．１２２０１６年１２月ＣＨＩＮＥＳＥＪＯＵＲＮＡＬＯＦＣＯＭＰＵＴＥＲＳＤｅｃ．２０１６形状图理论的定理证明张昱陈意云李兆鹏（中国科学技术大学计算机科学与技术学院合肥２３００２６）（中国科学技术大学苏州研究院软件安全实验室江苏苏州２１５１２３）摘要验证操作易变数据结构的指针程序仍面临很多挑战．数据结构中严重的指针别名显著地复杂化对操作这些结构的程序的推理．为分析和验证操作易变数据结构的指针程序，文中提出了形状图逻辑．形状图是描述程序中静态声明的堆指针变量和动态分

2、配的结构体中指针域变量的指向的一种有向图，能准确表达指针的有效性和指针之间的相等性，可用于判断两个访问表达式是否是别名．形状图逻辑是Ｈｏａｒｅ逻辑的一种扩展，是一种直接将形状图作为程序中指针断言集的程序逻辑．该文研究形状图的等价理论和蕴含理论以及它们的判定方法和应用．首先，把形状图及其等价规则和蕴含规则分别类比为代数项及其等式规则和重写规则，像研究代数规范的理论那样来研究形状图理论．该文定义了形状图的语法理论和语义理论，定义了形状图重写系统及其终止性、局部合流性和合流性，然后得到基于形状图重写的形状图等

3、价判定和蕴含判定的方法．其次，提出循环不变形状图和递归函数前后形状图的自动推断方法．借助形状图理论的判定方法，该文把一个基于抽象解释的推断循环不变式的一般方法改编成推断循环不变形状图的方法．由于计算终止的递归函数总有非递归的出口，可以先通过非递归路径得到函数的后形状图的初值，然后再在递归路径上迭代求解．从而，可以像推断循环不变形状图那样来推断递归函数的前后形状图．第三，参照ＮｅｌｓｏｎＯｐｐｅｎ框架，提出形状图理论和整数理论组合的一种判定方法．对易变数据结构，除了关心数据结构各节点是否连成预定的形状外

4、，往往还关心数据在这些节点间的排列等特性，它们不能脱离易变数据结构的形状特征而单独验证．为此，所提出的组合判定方法针对这类程序的验证条件的特点，利用程序分析阶段得到的形状图对验证条件的前件中的符号断言按形状图的节点分组；然后运用整数理论为各节点推导出尽可能多的性质；最后才交由定理证明器Ｚ３去自动验证．这种方式有效地避免验证条件证明过程的不终止．基于形状图逻辑以及文中的工作，我们所开发的程序验证系统原型减轻了自动定理证明器的负担，并且能验证易变数据结构上较为复杂的程序，如有序循环双向链表、二叉排序树、伸展

5、树、树堆、二叉平衡树和ＡＡ树的插入和删除函数．关键词形状图逻辑；形状分析；程序验证；自动定理证明；循环不变式的推断中图法分类号ＴＰ３１１犇犗犐号１０．１１８９７／ＳＰ．Ｊ．１０１６．２０１６．０２４６０犜犺犲狅狉犲犿犘狉狅狏犻狀犵犳狅狉犪犜犺犲狅狉狔狅犳犛犺犪狆犲犌狉犪狆犺狊ＺＨＡＮＧＹｕＣＨＥＮＹｉＹｕｎＬＩＺｈａｏＰｅｎｇ（犛犮犺狅狅犾狅犳犆狅犿狆狌狋犲狉犛犮犻犲狀犮犲犪狀犱犜犲犮犺狀狅犾狅犵狔，犝狀犻狏犲狉狊犻狋狔狅犳犛犮犻犲狀犮犲犪狀犱犜犲犮犺狀狅犾狅犵狔狅犳犆犺犻狀犪，犎犲犳犲犻２３００２

6、６）（犛狅犳狋狑犪狉犲犛犲犮狌狉犻狋狔犔犪犫狅狉犪狋狅狉狔，犛狌狕犺狅狌犐狀狊狋犻狋狌狋犲犳狅狉犃犱狏犪狀犮犲犱犛狋狌犱狔，犝狀犻狏犲狉狊犻狋狔狅犳犛犮犻犲狀犮犲犪狀犱犜犲犮犺狀狅犾狅犵狔狅犳犆犺犻狀犪，犛狌狕犺狅狌，犑犻犪狀犵狊狌２１５１２３）犃犫狊狋狉犪犮狋Ｐｒｏｇｒａｍｓｍａｎｉｐｕｌａｔｉｎｇｍｕｔａｂｌｅｄａｔａｓｔｒｕｃｔｕｒｅｓｐｒｅｓｅｎｔａｃｈａｌｌｅｎｇｅｆｏｒｖｅｒｉｆｉｃａｔｉｏｎ．Ｄｅｅｐａｌｉａｓｉｎｇｉｎｓｉｄｅｄａｔａｓｔｒｕｃｔｕｒｅｓｄｒａｍａｔｉｃａｌｌｙｃｏｍｐｌ

7、ｉｃａｔｅｓｒｅａｓｏｎｉｎｇｓｔａｔｅｍｅｎｔｓｍａｎｉｐｕｌａｔｉｎｇｔｈｅｓｅｓｔｒｕｃｔｕｒｅｓ．Ｔｏａｎａｌｙｚｅａｎｄｖｅｒｉｆｙｐｒｏｇｒａｍｓｍａｎｉｐｕｌａｔｉｎｇｍｕｔａｂｌｅｄａｔａｓｔｒｕｃｔｕｒｅｓ，ｗｅｐｒｏｐｏｓｅｄｔｈｅｓｈａｐｅｇｒａｐｈｌｏｇｉｃ．Ｓｈａｐｅｇｒａｐｈｓｄｅｓｃｒｉｂｅｐｏｉｎｔｔｏｒｅｌａｔｉｏｎｓｏｆｓｔａｔｉｃａｌｌｙｄｅｃｌａｒｅｄｈｅａｐｐｏｉｎｔｅｒｖａｒｉａｂｌｅｓａｎｄｐｏｉｎｔｅｒｆｉｅｌｄｓｏｆｈｅａｐｏｂｊｅｃｔｓ．Ｔｈｅｙｐｒ

8、ｅｃｉｓｅｌｙｅｘｐｒｅｓｓｔｈｅｖａｌｉｄｉｔｙｏｆｐｏｉｎｔｅｒｓａｎｄｔｈｅｅｑｕａｌｉｔｉｅｓｂｅｔｗｅｅｎｐｏｉｎｔｅｒｓ，ａｎｄｃａｎｂｅｕｓｅｄｔｏｊｕｄｇｅｗｈｅｔｈｅｒｔｗｏａｃｃｅｓｓｅｘｐｒｅｓｓｉｏｎｓ收稿日期：２０１４１１１４；在线出版日期：２０１５０５２９．本课题得到国家“八六三”高技术研究发展计划项目基金（２０１２ＡＡ０１０９０１）、国家自然科学基金（６１１７００１８，６１２２９２０１）资助．张昱，女，