第39卷第12期 计 算机 学报 Vol.39 No.12 2016年12月 CHINESE JOURNAL OF COMPUTERS Dec,2016 形状图理论的定理证明 张昱陈意云李兆鹏 (中国科学技术大学计算机科学与技术学院合肥230026) (中国科学技术大学苏州研究院软件安全实验室江苏苏州215123) 摘要验证操作易变数据结构的指针程序仍面临很多挑战.数据结构中严重的指针别名显著地复杂化对操作这 些结构的程序的推理.为分析和验证操作易变数据结构的指针程序，文中提出了形状图逻辑.形状图是描述程序中 静态声明的堆指针变量和动态分配的结构体中指针域变量的指向的一种有向图，能准确表达指针的有效性和指针 之间的相等性，可用于判断两个访问表达式是否是别名.形状图逻辑是Hoa©逻辑的一种扩展，是一种直接将形状 图作为程序中指针断言集的程序逻辑.该文研究形状图的等价理论和蕴含理论以及它们的判定方法和应用.首先， 把形状图及其等价规则和蕴含规则分别类比为代数项及其等式规则和重写规则，像研究代数规范的理论那样来研 究形状图理论.该文定义了形状图的语法理论和语义理论，定义了形状图重写系统及其终止性、局部合流性和合流 性，然后得到基于形状图重写的形状图等价判定和蕴含判定的方法.其次，提出循环不变形状图和递归函数前后形 状图的自动推断方法，借助形状图理论的判定方法，该文把一个基于抽象解释的推断循环不变式的一般方法改编 成推断循环不变形状图的方法，由于计算终止的递归函数总有非递归的出口，可以先通过非递归路径得到函数的 后形状图的初值，然后再在递归路径上迭代求解.从而，可以像推断循环不变形状图那样来推断递归函数的前后形 状图.第三，参照Nelson-Oppen框架，提出形状图理论和整数理论组合的一种判定方法.对易变数据结构，除了关 心数据结构各节点是否连成预定的形状外，往往还关心数据在这些节点间的排列等特性，它们不能脱离易变数据 结构的形状特征而单独验证.为此，所提出的组合判定方法针对这类程序的验证条件的特点，利用程序分析阶段得 到的形状图对验证条件的前件中的符号断言按形状图的节点分组：然后运用整数理论为各节点推导出尽可能多的 性质：最后才交由定理证明器Z3去自动验证.这种方式有效地避免验证条件证明过程的不终止.基于形状图逻辑 以及文中的工作，我们所开发的程序验证系统原型减轻了自动定理证明器的负担，并且能验证易变数据结构上较 为复杂的程序，如有序循环双向链表、二叉排序树、伸展树、树堆、二叉平衡树和AA树的插入和删除函数 关键词形状图逻辑；形状分析：程序验证：自动定理证明：循环不变式的推断 中图法分类号TP311 D0I号10.11897/SP.J.1016.2016.02460 Theorem Proving for a Theory of Shape Graphs ZHANG Yu CHEN Yi-Yun LI Zhao-Peng (School of Computer Science and Technology,University of Science and Technology of China.Hefei 230026) (Softuure Security Laboratory.Suzhou Institute for Adwanced Study.University of Science and Technology of China.Suzhou.Jiangsu 215123) Abstract Programs manipulating mutable data structures present a challenge for verification. Deep aliasing inside data structures dramatically complicates reasoning statements manipulating these structures.To analyze and verify programs manipulating mutable data structures,we proposed the shape graph logic.Shape graphs describe point-to relations of statically declared heap pointer variables and pointer fields of heap objects.They precisely express the validity of pointers and the equalities between pointers,and can be used to judge whether two access expressions 收稿日期：2014-11-14：在线出版日期：2015-05-29.本课题得到国家“八六三”高技术研究发展计划项目基金(2012AA010901)、国家自然 科学基金(61170018,61229201)资助.张昱，女，1972生，博士，副教授，中国计算机学会(CCF)高级会员，主要研究方向为程序设计语 言的理论和实现技术、程序验证、确定性并行编程模型与运行时系统.E-mail:yuzhangt@ustc.edu.cn.陈意云，男，l946年生，教授，博士 生导师，中国计算机学会(CC℉)高级会员，主要研究领域为程序设计语言的理论和实现技术，程序验证、软件安全等.李兆鹏，男，1978年 生，博士，副研究员，中国计算机学会(CC℉)会员，主要研究方向为程序语言、程序验证、出具证明的编译器、自动定理证明
书 第３９卷第１２期 ２０１６年１２月 计 算 机 学 报 ＣＨＩＮＥＳＥＪＯＵＲＮＡＬＯＦＣＯＭＰＵＴＥＲＳ Ｖｏｌ．３９Ｎｏ．１２ Ｄｅｃ．２０１６ 收稿日期：２０１４１１１４；在线出版日期：２０１５０５２９．本课题得到国家“八六三”高技术研究发展计划项目基金（２０１２ＡＡ０１０９０１）、国家自然 科学基金（６１１７００１８，６１２２９２０１）资助．张昱，女，１９７２生，博士，副教授，中国计算机学会（ＣＣＦ）高级会员，主要研究方向为程序设计语 言的理论和实现技术、程序验证、确定性并行编程模型与运行时系统．Ｅｍａｉｌ：ｙｕｚｈａｎｇ＠ｕｓｔｃ．ｅｄｕ．ｃｎ．陈意云，男，１９４６年生，教授，博士 生导师，中国计算机学会（ＣＣＦ）高级会员，主要研究领域为程序设计语言的理论和实现技术、程序验证、软件安全等．李兆鹏，男，１９７８年 生，博士，副研究员，中国计算机学会（ＣＣＦ）会员，主要研究方向为程序语言、程序验证、出具证明的编译器、自动定理证明． 形状图理论的定理证明 张昱陈意云李兆鹏 （中国科学技术大学计算机科学与技术学院合肥２３００２６） （中国科学技术大学苏州研究院软件安全实验室江苏苏州２１５１２３） 摘要验证操作易变数据结构的指针程序仍面临很多挑战．数据结构中严重的指针别名显著地复杂化对操作这 些结构的程序的推理．为分析和验证操作易变数据结构的指针程序，文中提出了形状图逻辑．形状图是描述程序中 静态声明的堆指针变量和动态分配的结构体中指针域变量的指向的一种有向图，能准确表达指针的有效性和指针 之间的相等性，可用于判断两个访问表达式是否是别名．形状图逻辑是Ｈｏａｒｅ逻辑的一种扩展，是一种直接将形状 图作为程序中指针断言集的程序逻辑．该文研究形状图的等价理论和蕴含理论以及它们的判定方法和应用．首先， 把形状图及其等价规则和蕴含规则分别类比为代数项及其等式规则和重写规则，像研究代数规范的理论那样来研 究形状图理论．该文定义了形状图的语法理论和语义理论，定义了形状图重写系统及其终止性、局部合流性和合流 性，然后得到基于形状图重写的形状图等价判定和蕴含判定的方法．其次，提出循环不变形状图和递归函数前后形 状图的自动推断方法．借助形状图理论的判定方法，该文把一个基于抽象解释的推断循环不变式的一般方法改编 成推断循环不变形状图的方法．由于计算终止的递归函数总有非递归的出口，可以先通过非递归路径得到函数的 后形状图的初值，然后再在递归路径上迭代求解．从而，可以像推断循环不变形状图那样来推断递归函数的前后形 状图．第三，参照ＮｅｌｓｏｎＯｐｐｅｎ框架，提出形状图理论和整数理论组合的一种判定方法．对易变数据结构，除了关 心数据结构各节点是否连成预定的形状外，往往还关心数据在这些节点间的排列等特性，它们不能脱离易变数据 结构的形状特征而单独验证．为此，所提出的组合判定方法针对这类程序的验证条件的特点，利用程序分析阶段得 到的形状图对验证条件的前件中的符号断言按形状图的节点分组；然后运用整数理论为各节点推导出尽可能多的 性质；最后才交由定理证明器Ｚ３去自动验证．这种方式有效地避免验证条件证明过程的不终止．基于形状图逻辑 以及文中的工作，我们所开发的程序验证系统原型减轻了自动定理证明器的负担，并且能验证易变数据结构上较 为复杂的程序，如有序循环双向链表、二叉排序树、伸展树、树堆、二叉平衡树和ＡＡ树的插入和删除函数． 关键词形状图逻辑；形状分析；程序验证；自动定理证明；循环不变式的推断 中图法分类号ＴＰ３１１ 犇犗犐号１０．１１８９７／ＳＰ．Ｊ．１０１６．２０１６．０２４６０ 犜犺犲狅狉犲犿犘狉狅狏犻狀犵犳狅狉犪犜犺犲狅狉狔狅犳犛犺犪狆犲犌狉犪狆犺狊 ＺＨＡＮＧＹｕＣＨＥＮＹｉＹｕｎＬＩＺｈａｏＰｅｎｇ （犛犮犺狅狅犾狅犳犆狅犿狆狌狋犲狉犛犮犻犲狀犮犲犪狀犱犜犲犮犺狀狅犾狅犵狔，犝狀犻狏犲狉狊犻狋狔狅犳犛犮犻犲狀犮犲犪狀犱犜犲犮犺狀狅犾狅犵狔狅犳犆犺犻狀犪，犎犲犳犲犻２３００２６） （犛狅犳狋狑犪狉犲犛犲犮狌狉犻狋狔犔犪犫狅狉犪狋狅狉狔，犛狌狕犺狅狌犐狀狊狋犻狋狌狋犲犳狅狉犃犱狏犪狀犮犲犱犛狋狌犱狔，犝狀犻狏犲狉狊犻狋狔狅犳犛犮犻犲狀犮犲犪狀犱犜犲犮犺狀狅犾狅犵狔狅犳犆犺犻狀犪，犛狌狕犺狅狌，犑犻犪狀犵狊狌２１５１２３） 犃犫狊狋狉犪犮狋Ｐｒｏｇｒａｍｓｍａｎｉｐｕｌａｔｉｎｇｍｕｔａｂｌｅｄａｔａｓｔｒｕｃｔｕｒｅｓｐｒｅｓｅｎｔａｃｈａｌｌｅｎｇｅｆｏｒｖｅｒｉｆｉｃａｔｉｏｎ． Ｄｅｅｐａｌｉａｓｉｎｇｉｎｓｉｄｅｄａｔａｓｔｒｕｃｔｕｒｅｓｄｒａｍａｔｉｃａｌｌｙｃｏｍｐｌｉｃａｔｅｓｒｅａｓｏｎｉｎｇｓｔａｔｅｍｅｎｔｓｍａｎｉｐｕｌａｔｉｎｇ ｔｈｅｓｅｓｔｒｕｃｔｕｒｅｓ．Ｔｏａｎａｌｙｚｅａｎｄｖｅｒｉｆｙｐｒｏｇｒａｍｓｍａｎｉｐｕｌａｔｉｎｇｍｕｔａｂｌｅｄａｔａｓｔｒｕｃｔｕｒｅｓ，ｗｅ ｐｒｏｐｏｓｅｄｔｈｅｓｈａｐｅｇｒａｐｈｌｏｇｉｃ．Ｓｈａｐｅｇｒａｐｈｓｄｅｓｃｒｉｂｅｐｏｉｎｔｔｏｒｅｌａｔｉｏｎｓｏｆｓｔａｔｉｃａｌｌｙｄｅｃｌａｒｅｄ ｈｅａｐｐｏｉｎｔｅｒｖａｒｉａｂｌｅｓａｎｄｐｏｉｎｔｅｒｆｉｅｌｄｓｏｆｈｅａｐｏｂｊｅｃｔｓ．Ｔｈｅｙｐｒｅｃｉｓｅｌｙｅｘｐｒｅｓｓｔｈｅｖａｌｉｄｉｔｙｏｆ ｐｏｉｎｔｅｒｓａｎｄｔｈｅｅｑｕａｌｉｔｉｅｓｂｅｔｗｅｅｎｐｏｉｎｔｅｒｓ，ａｎｄｃａｎｂｅｕｓｅｄｔｏｊｕｄｇｅｗｈｅｔｈｅｒｔｗｏａｃｃｅｓｓｅｘｐｒｅｓｓｉｏｎｓ
12期 张昱等：形状图理论的定理证明 2461 are aliases or not.The shape graph logic is an extension to Hoare logic,which directly uses shape graphs as pointer assertions.This paper studies the equivalence theory and implication theory of shape graphs,as well as their decision procedures and applications.First,we investigate the shape graph theory using analogous methods to those in studying the theory of algebraic specification, where shape graphs and their equivalence rules and implication rules are analogous to algebraic terms and their equality rules and rewriting rules,respectively.Analogously,we define the syntactic theory and semantic theory of shape graphs,and then define the shape graph rewriting system as well as its termination,local confluence and confluence.Based on these definitions,we present decision methods on deciding the equality and implication of shape graphs by rewriting shape graphs.Secondly,we propose methods for automatically inferring loop-invariant shape graphs as well as the pre-and post-shape graphs of recursive functions.With the help of the decision procedures for the shape graph theory,the proposed method for inferring loop-invariant shape graphs has been adapted from a general method for inferring loop invariants based on abstract interpretation.Since a terminal recursive function has at least one non-recursive exit,the initial post-shape graphs of the function can be inferred along the non-recursive path,and then post-shape graphs can be iteratively inferred along the recursive paths.Accordingly,the pre-and post-shape graphs of recursive functions can be inferred like the method inferring loop-invariant shape graphs.Thirdly,by referencing the Nelson-Oppen combination method,we propose a decision method for the combination of the theory of shape graphs and integer theory.For mutable data structures,in addition to caring about whether nodes of a data structure form the predetermined shape,features such as data arrangement between nodes are also cared.Such features cannot be divorced from the shape feature of mutable data structures,and cannot be verified alone.Therefore,according to the characteristics of verification conditions generated from such programs,the proposed combination method uses shape graphs obtained from program analysis to group symbolic assertions by shape graph nodes;then uses integer theory to infer as many properties as possible for the nodes;and finally passes the grouped assertions and properties to the Z3 theorem prover for automatic verification.This method can effectively avoid failures to prove verification conditions.Based on the shape graph theory and the work of this paper,our prototype of program verification system alleviates the burden of automated theorem provers,and can verify programs manipulating more complex mutable data structures,such as insert functions and delete functions of sorted circular doubly linked list,binary search tree,splay tree,treap, balanced binary tree and AA tree. Keywords shape graph logic;shape analysis;program verification;automated theorem proving; loop-invariant inference 全攸关嵌入式软件的测试.和单元测试相比，单元证 1 引 言 明降低了投入，主要是因为它方便了维护山.演绎验 证在工业界的应用虽有限但也在拓展，达索航空公 形式验证（包括抽象解释、模型检测和演绎验证 司在健壮性的形式验证方面，已有约15%的断言是 等途径)是提高软件可信程度的重要方法，并在工业 用演绎验证方式证明的叮 界已经逐步得到应用，尤其是抽象解释和模型检测. 在演绎验证方法中，有关自动程序验证的大部 例如，空客公司在A400M军用运输机以及A380和 分研究按这样的途径开展：程序员提供函数前后条 A350客机的开发上，已经用形式验证取代了部分安 件和循环不变式，系统对程序采用某种正向或逆向
ａｒｅａｌｉａｓｅｓｏｒｎｏｔ．ＴｈｅｓｈａｐｅｇｒａｐｈｌｏｇｉｃｉｓａｎｅｘｔｅｎｓｉｏｎｔｏＨｏａｒｅｌｏｇｉｃ，ｗｈｉｃｈｄｉｒｅｃｔｌｙｕｓｅｓｓｈａｐｅ ｇｒａｐｈｓａｓｐｏｉｎｔｅｒａｓｓｅｒｔｉｏｎｓ．Ｔｈｉｓｐａｐｅｒｓｔｕｄｉｅｓｔｈｅｅｑｕｉｖａｌｅｎｃｅｔｈｅｏｒｙａｎｄｉｍｐｌｉｃａｔｉｏｎｔｈｅｏｒｙｏｆ ｓｈａｐｅｇｒａｐｈｓ，ａｓｗｅｌｌａｓｔｈｅｉｒｄｅｃｉｓｉｏｎｐｒｏｃｅｄｕｒｅｓａｎｄａｐｐｌｉｃａｔｉｏｎｓ．Ｆｉｒｓｔ，ｗｅｉｎｖｅｓｔｉｇａｔｅｔｈｅ ｓｈａｐｅｇｒａｐｈｔｈｅｏｒｙｕｓｉｎｇａｎａｌｏｇｏｕｓｍｅｔｈｏｄｓｔｏｔｈｏｓｅｉｎｓｔｕｄｙｉｎｇｔｈｅｔｈｅｏｒｙｏｆａｌｇｅｂｒａｉｃｓｐｅｃｉｆｉｃａｔｉｏｎ， ｗｈｅｒｅｓｈａｐｅｇｒａｐｈｓａｎｄｔｈｅｉｒｅｑｕｉｖａｌｅｎｃｅｒｕｌｅｓａｎｄｉｍｐｌｉｃａｔｉｏｎｒｕｌｅｓａｒｅａｎａｌｏｇｏｕｓｔｏａｌｇｅｂｒａｉｃ ｔｅｒｍｓａｎｄｔｈｅｉｒｅｑｕａｌｉｔｙｒｕｌｅｓａｎｄｒｅｗｒｉｔｉｎｇｒｕｌｅｓ，ｒｅｓｐｅｃｔｉｖｅｌｙ．Ａｎａｌｏｇｏｕｓｌｙ，ｗｅｄｅｆｉｎｅｔｈｅ ｓｙｎｔａｃｔｉｃｔｈｅｏｒｙａｎｄｓｅｍａｎｔｉｃｔｈｅｏｒｙｏｆｓｈａｐｅｇｒａｐｈｓ，ａｎｄｔｈｅｎｄｅｆｉｎｅｔｈｅｓｈａｐｅｇｒａｐｈｒｅｗｒｉｔｉｎｇ ｓｙｓｔｅｍａｓｗｅｌｌａｓｉｔｓｔｅｒｍｉｎａｔｉｏｎ，ｌｏｃａｌｃｏｎｆｌｕｅｎｃｅａｎｄｃｏｎｆｌｕｅｎｃｅ．Ｂａｓｅｄｏｎｔｈｅｓｅｄｅｆｉｎｉｔｉｏｎｓ，ｗｅ ｐｒｅｓｅｎｔｄｅｃｉｓｉｏｎｍｅｔｈｏｄｓｏｎｄｅｃｉｄｉｎｇｔｈｅｅｑｕａｌｉｔｙａｎｄｉｍｐｌｉｃａｔｉｏｎｏｆｓｈａｐｅｇｒａｐｈｓｂｙｒｅｗｒｉｔｉｎｇ ｓｈａｐｅｇｒａｐｈｓ．Ｓｅｃｏｎｄｌｙ，ｗｅｐｒｏｐｏｓｅｍｅｔｈｏｄｓｆｏｒａｕｔｏｍａｔｉｃａｌｌｙｉｎｆｅｒｒｉｎｇｌｏｏｐｉｎｖａｒｉａｎｔｓｈａｐｅ ｇｒａｐｈｓａｓｗｅｌｌａｓｔｈｅｐｒｅａｎｄｐｏｓｔｓｈａｐｅｇｒａｐｈｓｏｆｒｅｃｕｒｓｉｖｅｆｕｎｃｔｉｏｎｓ．Ｗｉｔｈｔｈｅｈｅｌｐｏｆｔｈｅ ｄｅｃｉｓｉｏｎｐｒｏｃｅｄｕｒｅｓｆｏｒｔｈｅｓｈａｐｅｇｒａｐｈｔｈｅｏｒｙ，ｔｈｅｐｒｏｐｏｓｅｄｍｅｔｈｏｄｆｏｒｉｎｆｅｒｒｉｎｇｌｏｏｐｉｎｖａｒｉａｎｔ ｓｈａｐｅｇｒａｐｈｓｈａｓｂｅｅｎａｄａｐｔｅｄｆｒｏｍａｇｅｎｅｒａｌｍｅｔｈｏｄｆｏｒｉｎｆｅｒｒｉｎｇｌｏｏｐｉｎｖａｒｉａｎｔｓｂａｓｅｄｏｎ ａｂｓｔｒａｃｔｉｎｔｅｒｐｒｅｔａｔｉｏｎ．Ｓｉｎｃｅａｔｅｒｍｉｎａｌｒｅｃｕｒｓｉｖｅｆｕｎｃｔｉｏｎｈａｓａｔｌｅａｓｔｏｎｅｎｏｎｒｅｃｕｒｓｉｖｅｅｘｉｔ，ｔｈｅ ｉｎｉｔｉａｌｐｏｓｔｓｈａｐｅｇｒａｐｈｓｏｆｔｈｅｆｕｎｃｔｉｏｎｃａｎｂｅｉｎｆｅｒｒｅｄａｌｏｎｇｔｈｅｎｏｎｒｅｃｕｒｓｉｖｅｐａｔｈ，ａｎｄｔｈｅｎ ｐｏｓｔｓｈａｐｅｇｒａｐｈｓｃａｎｂｅｉｔｅｒａｔｉｖｅｌｙｉｎｆｅｒｒｅｄａｌｏｎｇｔｈｅｒｅｃｕｒｓｉｖｅｐａｔｈｓ．Ａｃｃｏｒｄｉｎｇｌｙ，ｔｈｅｐｒｅａｎｄ ｐｏｓｔｓｈａｐｅｇｒａｐｈｓｏｆｒｅｃｕｒｓｉｖｅｆｕｎｃｔｉｏｎｓｃａｎｂｅｉｎｆｅｒｒｅｄｌｉｋｅｔｈｅｍｅｔｈｏｄｉｎｆｅｒｒｉｎｇｌｏｏｐｉｎｖａｒｉａｎｔ ｓｈａｐｅｇｒａｐｈｓ．Ｔｈｉｒｄｌｙ，ｂｙｒｅｆｅｒｅｎｃｉｎｇｔｈｅＮｅｌｓｏｎＯｐｐｅｎｃｏｍｂｉｎａｔｉｏｎｍｅｔｈｏｄ，ｗｅｐｒｏｐｏｓｅａ ｄｅｃｉｓｉｏｎｍｅｔｈｏｄｆｏｒｔｈｅｃｏｍｂｉｎａｔｉｏｎｏｆｔｈｅｔｈｅｏｒｙｏｆｓｈａｐｅｇｒａｐｈｓａｎｄｉｎｔｅｇｅｒｔｈｅｏｒｙ．Ｆｏｒ ｍｕｔａｂｌｅｄａｔａｓｔｒｕｃｔｕｒｅｓ，ｉｎａｄｄｉｔｉｏｎｔｏｃａｒｉｎｇａｂｏｕｔｗｈｅｔｈｅｒｎｏｄｅｓｏｆａｄａｔａｓｔｒｕｃｔｕｒｅｆｏｒｍｔｈｅ ｐｒｅｄｅｔｅｒｍｉｎｅｄｓｈａｐｅ，ｆｅａｔｕｒｅｓｓｕｃｈａｓｄａｔａａｒｒａｎｇｅｍｅｎｔｂｅｔｗｅｅｎｎｏｄｅｓａｒｅａｌｓｏｃａｒｅｄ．Ｓｕｃｈ ｆｅａｔｕｒｅｓｃａｎｎｏｔｂｅｄｉｖｏｒｃｅｄｆｒｏｍｔｈｅｓｈａｐｅｆｅａｔｕｒｅｏｆｍｕｔａｂｌｅｄａｔａｓｔｒｕｃｔｕｒｅｓ，ａｎｄｃａｎｎｏｔｂｅ ｖｅｒｉｆｉｅｄａｌｏｎｅ．Ｔｈｅｒｅｆｏｒｅ，ａｃｃｏｒｄｉｎｇｔｏｔｈｅｃｈａｒａｃｔｅｒｉｓｔｉｃｓｏｆｖｅｒｉｆｉｃａｔｉｏｎｃｏｎｄｉｔｉｏｎｓｇｅｎｅｒａｔｅｄ ｆｒｏｍｓｕｃｈｐｒｏｇｒａｍｓ，ｔｈｅｐｒｏｐｏｓｅｄｃｏｍｂｉｎａｔｉｏｎｍｅｔｈｏｄｕｓｅｓｓｈａｐｅｇｒａｐｈｓｏｂｔａｉｎｅｄｆｒｏｍｐｒｏｇｒａｍ ａｎａｌｙｓｉｓｔｏｇｒｏｕｐｓｙｍｂｏｌｉｃａｓｓｅｒｔｉｏｎｓｂｙｓｈａｐｅｇｒａｐｈｎｏｄｅｓ；ｔｈｅｎｕｓｅｓｉｎｔｅｇｅｒｔｈｅｏｒｙｔｏｉｎｆｅｒａｓ ｍａｎｙｐｒｏｐｅｒｔｉｅｓａｓｐｏｓｓｉｂｌｅｆｏｒｔｈｅｎｏｄｅｓ；ａｎｄｆｉｎａｌｌｙｐａｓｓｅｓｔｈｅｇｒｏｕｐｅｄａｓｓｅｒｔｉｏｎｓａｎｄｐｒｏｐｅｒｔｉｅｓｔｏ ｔｈｅＺ３ｔｈｅｏｒｅｍｐｒｏｖｅｒｆｏｒａｕｔｏｍａｔｉｃｖｅｒｉｆｉｃａｔｉｏｎ．Ｔｈｉｓｍｅｔｈｏｄｃａｎｅｆｆｅｃｔｉｖｅｌｙａｖｏｉｄｆａｉｌｕｒｅｓｔｏ ｐｒｏｖｅｖｅｒｉｆｉｃａｔｉｏｎｃｏｎｄｉｔｉｏｎｓ．Ｂａｓｅｄｏｎｔｈｅｓｈａｐｅｇｒａｐｈｔｈｅｏｒｙａｎｄｔｈｅｗｏｒｋｏｆｔｈｉｓｐａｐｅｒ，ｏｕｒ ｐｒｏｔｏｔｙｐｅｏｆｐｒｏｇｒａｍｖｅｒｉｆｉｃａｔｉｏｎｓｙｓｔｅｍａｌｌｅｖｉａｔｅｓｔｈｅｂｕｒｄｅｎｏｆａｕｔｏｍａｔｅｄｔｈｅｏｒｅｍｐｒｏｖｅｒｓ，ａｎｄ ｃａｎｖｅｒｉｆｙｐｒｏｇｒａｍｓｍａｎｉｐｕｌａｔｉｎｇｍｏｒｅｃｏｍｐｌｅｘｍｕｔａｂｌｅｄａｔａｓｔｒｕｃｔｕｒｅｓ，ｓｕｃｈａｓｉｎｓｅｒｔｆｕｎｃｔｉｏｎｓ ａｎｄｄｅｌｅｔｅｆｕｎｃｔｉｏｎｓｏｆｓｏｒｔｅｄｃｉｒｃｕｌａｒｄｏｕｂｌｙｌｉｎｋｅｄｌｉｓｔ，ｂｉｎａｒｙｓｅａｒｃｈｔｒｅｅ，ｓｐｌａｙｔｒｅｅ，ｔｒｅａｐ， ｂａｌａｎｃｅｄｂｉｎａｒｙｔｒｅｅａｎｄＡＡｔｒｅｅ． 犓犲狔狑狅狉犱狊ｓｈａｐｅｇｒａｐｈｌｏｇｉｃ；ｓｈａｐｅａｎａｌｙｓｉｓ；ｐｒｏｇｒａｍｖｅｒｉｆｉｃａｔｉｏｎ；ａｕｔｏｍａｔｅｄｔｈｅｏｒｅｍｐｒｏｖｉｎｇ； ｌｏｏｐｉｎｖａｒｉａｎｔｉｎｆｅｒｅｎｃｅ １引言 形式验证（包括抽象解释、模型检测和演绎验证 等途径）是提高软件可信程度的重要方法，并在工业 界已经逐步得到应用，尤其是抽象解释和模型检测． 例如，空客公司在Ａ４００Ｍ军用运输机以及Ａ３８０和 Ａ３５０客机的开发上，已经用形式验证取代了部分安 全攸关嵌入式软件的测试．和单元测试相比，单元证 明降低了投入，主要是因为它方便了维护［１］．演绎验 证在工业界的应用虽有限但也在拓展，达索航空公 司在健壮性的形式验证方面，已有约１５％的断言是 用演绎验证方式证明的［１］． 在演绎验证方法中，有关自动程序验证的大部 分研究按这样的途径开展：程序员提供函数前后条 件和循环不变式，系统对程序采用某种正向或逆向 １２期 张昱等：形状图理论的定理证明 ２４６１
2462 计算 龙 学 报 2016年 的演算来产生验证条件（即把对程序满足某些性质 理论.例如，对于用根节点的中序前驱（其左子树中 的证明转化为对一些验证条件的证明)，然后用自动 最右下的节点)代替根节点的、删除二叉排序树根节 定理证明器来证明验证条件，如Ynot)、Spec#[ 点的函数，若要证明结果仍然是二叉排序树，则需要 和ESC/Java).有些研究依靠符号计算及其过程中 用到二叉排序树的两个性质：左子树中任何节点的 的定理证明来避免验证条件的生成，如smallfoot) 值一定小于右子树中各节点的值，左子树中最右下 和jStar6].无论用哪种策略，演绎验证方法都使用 节点的值大于左子树中其他节点的任何值.它们都 严谨的方式对软件系统进行数学推理，并且都借助 是二叉排序树的归纳性质，但是基于演绎推理的自 定理证明软件，如定理证明器Isabelle/HOL)、定 动定理证明器不可能从二叉排序树的归纳定义推导 理证明辅助工具Cog①、SMT(Satisfiability Modulo 出这些性质，因而无法证明依赖这些性质的验证 Theories)求解器Z3[s]. 条件 基于演绎推理的自动形式验证方法对自动定理 为验证操作易变数据结构的指针程序，我们提 证明器的能力有较高期待.首先，定理证明器在程序 出了形状图逻辑].形状图是描述程序所操作的静 验证过程中频繁使用.大到验证条件的证明和循环 态声明的指针型变量（简称声明指针）和动态分配的 不变式的推断，小到下标变量的别名判断和数组边 结构体中指针型域变量（简称域指针）的指向的一种 界检查，都需要或可以使用定理证明器.其次，需要 有向图.它准确表达了指针的有效性（指针有效是说 能够应对各种领域专用逻辑的定理证明.应用程序 该指针指向已分配且尚未释放的内存块)和指针的 的代码中可能涉及多种数据类型，操作系统的代码 相等性，因而可作为指针程序中指针有效性和相等 依赖于硬件特性，为完成对这些程序的验证，需要定 性的断言.形状图逻辑就是一种直接把形状图作为 理证明器能够覆盖这些领域专用逻辑的定理证明. 程序中指针断言集的程序逻辑.它是Hoare逻辑的 第三，需要定理证明器能处理各种理论的组合.例如 一种扩展，为指针操作语句设计了专门的推理规则， 面向数组类型的数组逻辑，它由下标逻辑和元素逻 这些规则用图形方式描述指针操作语句引起的形状 辑组成.对于操作数组的程序的验证，定理证明器要 图上被关注部分的变化.利用形状图还可以方便地 能证明这两种逻辑的相应理论（可能还包括等式理 消除访问路径别名，使易变数据结构上数据性质的 论和未解释函数理论)组合后形成的组合理论上的 验证仍可用Hoare逻辑的规则进行推理 定理.组合理论的问题复杂性在于：即使两个理论分 本文补足文献[10]所缺少的部分理论和算法 别可判定，其组合理论未必可判定[).数组理论就是 文献[10]主要围绕程序逻辑层面，提出把形状图作 这样的例子 为指针断言，并在此基础上设计了推理指针程序的 本文研究操作易变数据结构（包括单/双向链 形状图逻辑和检查形状合法性的形状系统.本文围 表、循环单/双向链表②和二叉链表示的二叉树)的 绕作为指针断言的形状图，研究形状图的等价理论 指针程序的自动验证中的一些定理证明问题.这类 和蕴涵理论以及它们的判定方法和应用.本文的贡 程序的验证非常困难.首先，难以给出表达程序性质 献有如下3点： 的函数前后条件，尤其是循环不变式.因为它们涉及 (1)提出形状图理论的一种判定方法。 所操作的数据结构的结构性质（常使用带量词的命 本文把形状图及其等价规则和蕴涵规则分别类 题和可达性谓词来表达)以及在数据结构中各节点 比为代数项及其等式规则和重写规则，像研究代数 内的数据的性质，而后者的描述可能紧密依赖于数 规范的理论那样来研究形状图理论，本文类似地定 据结构的结构性质，例如平衡二叉树节点的平衡因 义形状图的语法理论和语义理论，定义形状图重 子和AA树节点的level值.其次，难以证明这类程 写系统及其终止性、局部合流性和合流性，最后得到 序的验证条件，因为在验证条件中经常出现对数据 基于形状图重写的形状图等价判定和蕴涵判定的 结构所有节点的某种全称量化，这导致不能使用像 方法。 Nelson-(Oppen框架[]这样仅适用于无量词理论的 (2)提出循环不变形状图和递归函数前后形状 传统的理论组合.Z3虽然通过使用E-graph匹配技 术能够处理量化公式，但也难以适应复杂的量化公 D The Cog Development Team.The Cog proof assistant reference 式.除了要用量词刻画性质以及涉及的理论组合之 manual (Version 8.2),2009.URL http://cog.inria.fr ②本文用“单/双向链表”表示非循环的单/双向链表，用“（循 外，验证条件的证明可能还要用到数据结构的归纳 环)单/双向链表”表示循环和/或非循环的单/双向链表
的演算来产生验证条件（即把对程序满足某些性质 的证明转化为对一些验证条件的证明），然后用自动 定理证明器来证明验证条件，如Ｙｎｏｔ［２］、Ｓｐｅｃ＃［３］ 和ＥＳＣ／Ｊａｖａ［４］．有些研究依靠符号计算及其过程中 的定理证明来避免验证条件的生成，如ｓｍａｌｌｆｏｏｔ［５］ 和ｊＳｔａｒ［６］．无论用哪种策略，演绎验证方法都使用 严谨的方式对软件系统进行数学推理，并且都借助 定理证明软件，如定理证明器Ｉｓａｂｅｌｌｅ／ＨＯＬ［７］、定 理证明辅助工具Ｃｏｑ①、ＳＭＴ（ＳａｔｉｓｆｉａｂｉｌｉｔｙＭｏｄｕｌｏ Ｔｈｅｏｒｉｅｓ）求解器Ｚ３［８］． 基于演绎推理的自动形式验证方法对自动定理 证明器的能力有较高期待．首先，定理证明器在程序 验证过程中频繁使用．大到验证条件的证明和循环 不变式的推断，小到下标变量的别名判断和数组边 界检查，都需要或可以使用定理证明器．其次，需要 能够应对各种领域专用逻辑的定理证明．应用程序 的代码中可能涉及多种数据类型，操作系统的代码 依赖于硬件特性，为完成对这些程序的验证，需要定 理证明器能够覆盖这些领域专用逻辑的定理证明． 第三，需要定理证明器能处理各种理论的组合．例如 面向数组类型的数组逻辑，它由下标逻辑和元素逻 辑组成．对于操作数组的程序的验证，定理证明器要 能证明这两种逻辑的相应理论（可能还包括等式理 论和未解释函数理论）组合后形成的组合理论上的 定理．组合理论的问题复杂性在于：即使两个理论分 别可判定，其组合理论未必可判定［９］．数组理论就是 这样的例子． 本文研究操作易变数据结构（包括单／双向链 表、循环单／双向链表②和二叉链表示的二叉树）的 指针程序的自动验证中的一些定理证明问题．这类 程序的验证非常困难．首先，难以给出表达程序性质 的函数前后条件，尤其是循环不变式．因为它们涉及 所操作的数据结构的结构性质（常使用带量词的命 题和可达性谓词来表达）以及在数据结构中各节点 内的数据的性质，而后者的描述可能紧密依赖于数 据结构的结构性质，例如平衡二叉树节点的平衡因 子和ＡＡ树节点的ｌｅｖｅｌ值．其次，难以证明这类程 序的验证条件，因为在验证条件中经常出现对数据 结构所有节点的某种全称量化．这导致不能使用像 ＮｅｌｓｏｎＯｐｐｅｎ框架［９］这样仅适用于无量词理论的 传统的理论组合．Ｚ３虽然通过使用Ｅｇｒａｐｈ匹配技 术能够处理量化公式，但也难以适应复杂的量化公 式．除了要用量词刻画性质以及涉及的理论组合之 外，验证条件的证明可能还要用到数据结构的归纳 理论．例如，对于用根节点的中序前驱（其左子树中 最右下的节点）代替根节点的、删除二叉排序树根节 点的函数，若要证明结果仍然是二叉排序树，则需要 用到二叉排序树的两个性质：左子树中任何节点的 值一定小于右子树中各节点的值，左子树中最右下 节点的值大于左子树中其他节点的任何值．它们都 是二叉排序树的归纳性质，但是基于演绎推理的自 动定理证明器不可能从二叉排序树的归纳定义推导 出这些性质，因而无法证明依赖这些性质的验证 条件．为验证操作易变数据结构的指针程序，我们提 出了形状图逻辑［１０］．形状图是描述程序所操作的静 态声明的指针型变量（简称声明指针）和动态分配的 结构体中指针型域变量（简称域指针）的指向的一种 有向图．它准确表达了指针的有效性（指针有效是说 该指针指向已分配且尚未释放的内存块）和指针的 相等性，因而可作为指针程序中指针有效性和相等 性的断言．形状图逻辑就是一种直接把形状图作为 程序中指针断言集的程序逻辑．它是Ｈｏａｒｅ逻辑的 一种扩展，为指针操作语句设计了专门的推理规则， 这些规则用图形方式描述指针操作语句引起的形状 图上被关注部分的变化．利用形状图还可以方便地 消除访问路径别名，使易变数据结构上数据性质的 验证仍可用Ｈｏａｒｅ逻辑的规则进行推理． 本文补足文献［１０］所缺少的部分理论和算法． 文献［１０］主要围绕程序逻辑层面，提出把形状图作 为指针断言，并在此基础上设计了推理指针程序的 形状图逻辑和检查形状合法性的形状系统．本文围 绕作为指针断言的形状图，研究形状图的等价理论 和蕴涵理论以及它们的判定方法和应用．本文的贡 献有如下３点： （１）提出形状图理论的一种判定方法． 本文把形状图及其等价规则和蕴涵规则分别类 比为代数项及其等式规则和重写规则，像研究代数 规范的理论那样来研究形状图理论．本文类似地定 义形状图的语法理论和语义理论，定义形状图重 写系统及其终止性、局部合流性和合流性，最后得到 基于形状图重写的形状图等价判定和蕴涵判定的 方法．（２）提出循环不变形状图和递归函数前后形状 ２４６２ 计 算 机 学 报 ２０１６年 ① ② ＴｈｅＣｏｑＤｅｖｅｌｏｐｍｅｎｔＴｅａｍ．ＴｈｅＣｏｑｐｒｏｏｆａｓｓｉｓｔａｎｔｒｅｆｅｒｅｎｃｅ ｍａｎｕａｌ（Ｖｅｒｓｉｏｎ８．２），２００９．ＵＲＬｈｔｔｐ：／／ｃｏｑ．ｉｎｒｉａ．ｆｒ 本文用“单／双向链表”表示非循环的单／双向链表，用“（循 环）单／双向链表”表示循环和／或非循环的单／双向链表．
12期 张昱等：形状图理论的定理证明 2463 图的自动推断算法 还可能有与浓缩节点含义一致的表达式e和断言 借助形状图理论的判定方法，本文把一个通过 a.指向谓词节点的有向边以及该节点下侧的e和a 迭代推断循环不变式的一般方法]改编成一个推 是该节点所代表的谓词的变元，例如图2给出了几 断循环不变形状图的方法；进一步设计该方法的一 种用形状图定义的数据结构，以单链表为例，图中谓 个变种来迭代推断递归函数的前后形状图. 词节点的变元和左侧的符号谓词1ist(s,e,a)的变元 (3)提出形状图理论和整数理论组合的一种判 是一致的. 定方法 单链表 对易变数据结构，除了关心数据结构各节点是 list(s,e,a） 否连成预定的形状外，往往还关心数据在这些节点 list,e.a 0.3 间的排列特性，它们不能脱离易变数据结构的结构 双向链表 dlist(s.e,a) GG网 特点而单独验证.于是需要研究形状图理论和整数 dlist,e,a 上线性算术理论（假定节点数据是整型）组合的判定 a→(e==0) 问题.本文针对验证条件的特点，利用程序分析阶段 得到的形状图，参照Nelson-(Oppen框架，提出形状 图理论和整数上线性算术理论组合的一种判定方法 网 dlist.e. a→(e>= 本文第2节简要回顾文献[10]提出的形状图、 形状图变换规则和形状图逻辑；第3节介绍形状图 双向链表 dlist(s 理论的判定方法；第4节介绍循环不变形状图的推 dlist 断和递归函数前后形状图的推断：第5节介绍形状 图理论和整数理论组合的判定方法：第6节是验证 实例：第7节是和相关研究工作的比较：第8节是 ©89图 总结 二叉树 tree(s) 2 形状图和形状图逻辑 o o-B 2.1形状图 形状图是描述程序中静态声明指针和动态分配 图2形状谓词定义的一些例子 的结构体中域指针的指向关系的一种有向图， 形状图的顶点（也称节点）有6种，其图形化语 形状图中的有向边表示声明指针和域指针的指 法形式见图1.其中声明节点和结构节点分别表示 向，指向同一个节点（悬空节点除外）的指针相等.有 静态声明指针和动态分配的结构体.null节点和悬 向边及其连接的节点满足如下语法约束： 空节点的用意稍后会提到 (1)声明节点.只有唯一的出边，没有入边，出 边的标记就是声明指针名. D i (2)结构节点和浓缩节点.有入边和出边，其中 声明节点结构节点u节点悬空节点ea 浓缩节点 name,e,a 调词节点 出边的条数与结构节点所代表的结构体的域指针个 图1形状图的各种节点 数一致，各出边的标记分别是各域指针名。 浓缩节点是若干个结构节点和它们之间的有向 (3)ull节点、悬空节点和谓词节点.有入边，没 边的浓缩表示，其灰色矩形下侧的表达式e和断言 有出边.ul节点和悬空节点分别用来表示指向它 a分别表示被浓缩的结构节点的个数以及对e的取 们的有向边代表null指针和悬空指针. 值范围的约束，若灰色矩形下无e和a,称为无约束 形状图的定义：(1)节点和有向边满足上述语 浓缩节点，它表示被浓缩的结构节点个数任意，可以 法约束，各声明节点出边标记相异，且边被视为无向 是0个 时则连通的图形是形状图；(2)若形状图G1,G2,…, 谓词节点代表满足指定谓词的若干节点和它们 G.的声明节点出边标记集两两相交都为空，则由逻 之间的有向边，其矩形节点下侧标有谓词名name, 辑合取符号∧连接的G1∧G2∧…∧Gm也是形状图
图的自动推断算法． 借助形状图理论的判定方法，本文把一个通过 迭代推断循环不变式的一般方法［１１］改编成一个推 断循环不变形状图的方法；进一步设计该方法的一 个变种来迭代推断递归函数的前后形状图． （３）提出形状图理论和整数理论组合的一种判 定方法．对易变数据结构，除了关心数据结构各节点是 否连成预定的形状外，往往还关心数据在这些节点 间的排列特性，它们不能脱离易变数据结构的结构 特点而单独验证．于是需要研究形状图理论和整数 上线性算术理论（假定节点数据是整型）组合的判定 问题．本文针对验证条件的特点，利用程序分析阶段 得到的形状图，参照ＮｅｌｓｏｎＯｐｐｅｎ框架，提出形状 图理论和整数上线性算术理论组合的一种判定方法． 本文第２节简要回顾文献［１０］提出的形状图、 形状图变换规则和形状图逻辑；第３节介绍形状图 理论的判定方法；第４节介绍循环不变形状图的推 断和递归函数前后形状图的推断；第５节介绍形状 图理论和整数理论组合的判定方法；第６节是验证 实例；第７节是和相关研究工作的比较；第８节是 总结． ２形状图和形状图逻辑 ２１形状图 形状图是描述程序中静态声明指针和动态分配 的结构体中域指针的指向关系的一种有向图． 形状图的顶点（也称节点）有６种，其图形化语 法形式见图１．其中声明节点和结构节点分别表示 静态声明指针和动态分配的结构体．ｎｕｌｌ节点和悬 空节点的用意稍后会提到． 图１形状图的各种节点 浓缩节点是若干个结构节点和它们之间的有向 边的浓缩表示，其灰色矩形下侧的表达式ｅ和断言 ａ分别表示被浓缩的结构节点的个数以及对ｅ的取 值范围的约束．若灰色矩形下无ｅ和ａ，称为无约束 浓缩节点，它表示被浓缩的结构节点个数任意，可以 是０个．谓词节点代表满足指定谓词的若干节点和它们 之间的有向边，其矩形节点下侧标有谓词名ｎａｍｅ， 还可能有与浓缩节点含义一致的表达式ｅ和断言 ａ．指向谓词节点的有向边以及该节点下侧的ｅ和ａ 是该节点所代表的谓词的变元，例如图２给出了几 种用形状图定义的数据结构，以单链表为例，图中谓 词节点的变元和左侧的符号谓词ｌｉｓｔ（ｓ，ｅ，ａ）的变元 是一致的． 图２形状谓词定义的一些例子 形状图中的有向边表示声明指针和域指针的指 向，指向同一个节点（悬空节点除外）的指针相等．有 向边及其连接的节点满足如下语法约束： （１）声明节点．只有唯一的出边，没有入边，出 边的标记就是声明指针名． （２）结构节点和浓缩节点．有入边和出边，其中 出边的条数与结构节点所代表的结构体的域指针个 数一致，各出边的标记分别是各域指针名． （３）ｎｕｌｌ节点、悬空节点和谓词节点．有入边，没 有出边．ｎｕｌｌ节点和悬空节点分别用来表示指向它 们的有向边代表ｎｕｌｌ指针和悬空指针． 形状图的定义：（１）节点和有向边满足上述语 法约束，各声明节点出边标记相异，且边被视为无向 时则连通的图形是形状图；（２）若形状图犌１，犌２，…， 犌狀的声明节点出边标记集两两相交都为空，则由逻 辑合取符号∧连接的犌１∧犌２∧…∧犌狀也是形状图． １２期 张昱等：形状图理论的定理证明 ２４６３
2464 计算 学 报 2016年 其中，不含符号八的形状图G被称为形状子图； 一个形状图的某形状子图中用点划线方框标明 (3)若形状图G1,G2,…,Gn的声明节点出边标记集 并满足下面条件的部分称为窗口，窗口描述形状子 都相同，则逻辑析取符号V连接的G1VG2V…VGn 图上被关注的那部分，形状图的其余部分称为窗口 也是形状图」 的上下文 从文献[10]有关形状图的语义知道，一个不含 (1)形状图的各节点处于窗口内或上下文中， 析取符号并且没有浓缩节点和谓词节点的形状图是 不得与窗口的方框边界相交。 程序状态中指针型数据的图形表示，不含析取符号 (2)窗口内各节点之间的边都位于窗口中. 的一般形状图G则是程序状态集的图形表示.G1∧ (3)表达窗口中节点与上下文中节点联系的、 G2中的G和G2各代表程序状态的不同部分，G1V 穿越方框边界的边属于窗口，这些边的另一份副本 G2中的G和G2则代表不同的程序状态集.若无特 在上下文中。 别说明，符号G仅表示不含符号V的形状图， 窗口W和上下文G[]的匹配就是检查穿越W 图2给出基于形状图定义的单链表（域指针t 边界的边和G[]中的副本边能否重合，重合后得到 是下文next或nxt的简称，本文不区分这3个名称)、 的形状图用G[W]表示. 双向链表和二叉链表示的二叉树（系统还支持的循 在形状图变换规则中出现的窗口有如下的缩写 环单链表和循环双向链表的定义见文献[10]).在 约定：对窗口中的某节点而言，若要求从窗口外指向 图2中，定义式最左边的dlist(s,e,a)等符号表示是 该节点至少要有一条边（如图3的p:),则可能还有 为了便于在文中引用.可以看出，把dlist(s,e,a)的 的、指向该节点的其他边（可以是0条）用一条标记 2个定义中的e和a部分略去，再用符号V连接它 为p的边统一表示。 们，就得到dist(s)的定义.若用符号谓词表示，图2 窗口用来定义形状图的等价规则和蕴涵规则 的二叉树定义相当于tree(s)△s==NULLVs!= (见文献[10]的2.3节)及形状图逻辑的推理规则 NULL∧tree(s→r)∧tree(s→-l) (见文献[10]的3.1节) e,a (1) a→(e>=1) (2) (3) 图3（循环）单链表的等价规则的3个例子 2.2形状图的等价和蕴涵规则 e)八a)→az和(e2==e1)∧az)→a1.例如，从图4 等价规则是保持形状图语义等价的变换规则. 的每条等价规则都可得到两条蕴涵规则， 图3列出了在文献[10]的2.3节中定义的（循环）单 链表的部分等价规则.第3节还会列举一些等价 nt 规则. (1) 除了等价规则外，形状图还有蕴涵规则，蕴涵规 ((e==ea1)→a)A((e2==eMa2)→a1) 则是保持形状图语义蕴涵的变换规则.文献[10]中 2.3节定义的形状图蕴涵规则分成三部分. (1)从等价规则W台W:VWz可得W1→W和 Wz→W两条蕴涵规则.例如，从图3(3)的等价规则 (e==eAa1)=a)A((e==eAa2)=→a1】 可以得到两条蕴涵规则. (2)若等价规则W1台W2的副条件是((e1== 图4对浓缩节点的约束数据进行变换的部分等价规则 e2Aa1)→az)∧((e2==e1∧a2)→a1),则有蕴涵规 (3)将等价规则中有约束浓缩节点改成无约束 则W,→W2和W2→W1,其副条件分别是(e1== 浓缩节点而得到蕴涵规则.例如，图5中蕴涵规则
其中，不含符号∧的形状图犌被称为形状子图； （３）若形状图犌１，犌２，…，犌狀的声明节点出边标记集 都相同，则逻辑析取符号∨连接的犌１∨犌２∨…∨犌狀 也是形状图． 从文献［１０］有关形状图的语义知道，一个不含 析取符号并且没有浓缩节点和谓词节点的形状图是 程序状态中指针型数据的图形表示，不含析取符号 的一般形状图犌则是程序状态集的图形表示．犌１∧ 犌２中的犌１和犌２各代表程序状态的不同部分．犌１∨ 犌２中的犌１和犌２则代表不同的程序状态集．若无特 别说明，符号犌仅表示不含符号∨的形状图． 图２给出基于形状图定义的单链表（域指针ｎｔ 是下文ｎｅｘｔ或ｎｘｔ的简称，本文不区分这３个名称）、 双向链表和二叉链表示的二叉树（系统还支持的循 环单链表和循环双向链表的定义见文献［１０］）．在 图２中，定义式最左边的ｄｌｉｓｔ（ｓ，ｅ，ａ）等符号表示是 为了便于在文中引用．可以看出，把ｄｌｉｓｔ（ｓ，ｅ，ａ）的 ２个定义中的ｅ和ａ部分略去，再用符号∨连接它 们，就得到ｄｌｉｓｔ（ｓ）的定义．若用符号谓词表示，图２ 的二叉树定义相当于ｔｒｅｅ（ｓ）ｓ＝＝ＮＵＬＬ∨ｓ！＝ ＮＵＬＬ∧ｔｒｅｅ（ｓ→ｒ）∧ｔｒｅｅ（ｓ→ｌ）． 一个形状图的某形状子图中用点划线方框标明 并满足下面条件的部分称为窗口，窗口描述形状子 图上被关注的那部分，形状图的其余部分称为窗口 的上下文．（１）形状图的各节点处于窗口内或上下文中， 不得与窗口的方框边界相交． （２）窗口内各节点之间的边都位于窗口中． （３）表达窗口中节点与上下文中节点联系的、 穿越方框边界的边属于窗口，这些边的另一份副本 在上下文中． 窗口犠和上下文犌［］的匹配就是检查穿越犠 边界的边和犌［］中的副本边能否重合，重合后得到 的形状图用犌［犠］表示． 在形状图变换规则中出现的窗口有如下的缩写 约定：对窗口中的某节点而言，若要求从窗口外指向 该节点至少要有一条边（如图３的狆１），则可能还有 的、指向该节点的其他边（可以是０条）用一条标记 为狆犽的边统一表示． 窗口用来定义形状图的等价规则和蕴涵规则 （见文献［１０］的２．３节）及形状图逻辑的推理规则 （见文献［１０］的３．１节）． 图３（循环）单链表的等价规则的３个例子 ２２形状图的等价和蕴涵规则 等价规则是保持形状图语义等价的变换规则． 图３列出了在文献［１０］的２．３节中定义的（循环）单 链表的部分等价规则．第３节还会列举一些等价 规则．除了等价规则外，形状图还有蕴涵规则，蕴涵规 则是保持形状图语义蕴涵的变换规则．文献［１０］中 ２．３节定义的形状图蕴涵规则分成三部分． （１）从等价规则犠犠１∨犠２可得犠１犠和 犠２犠两条蕴涵规则．例如，从图３（３）的等价规则 可以得到两条蕴涵规则． （２）若等价规则犠１犠２的副条件是（（ｅ１＝＝ ｅ２∧ａ１）ａ２）∧（（ｅ２＝＝ｅ１∧ａ２）ａ１），则有蕴涵规 则犠１犠２和犠２犠１，其副条件分别是（（ｅ１＝＝ ｅ２）∧ａ１）ａ２和（（ｅ２＝＝ｅ１）∧ａ２）ａ１．例如，从图４ 的每条等价规则都可得到两条蕴涵规则． 图４对浓缩节点的约束数据进行变换的部分等价规则 （３）将等价规则中有约束浓缩节点改成无约束 浓缩节点而得到蕴涵规则．例如，图５中蕴涵规则 ２４６４ 计 算 机 学 报 ２０１６年