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客机的开发上，已经用形式验证取代了部分安 件和循环不变式，系统对程序采用某种正向或逆向ａｒｅａｌｉａｓｅｓｏｒｎｏｔ．ＴｈｅｓｈａｐｅｇｒａｐｈｌｏｇｉｃｉｓａｎｅｘｔｅｎｓｉｏｎｔｏＨｏａｒｅｌｏｇｉｃ，ｗｈｉｃｈｄｉｒｅｃｔｌｙｕｓｅｓｓｈａｐｅ ｇｒａｐｈｓａｓｐｏｉｎｔｅｒａｓｓｅｒｔｉｏｎｓ．Ｔｈｉｓｐａｐｅｒｓｔｕｄｉｅｓｔｈｅｅｑｕｉｖａｌｅｎｃｅｔｈｅｏｒｙａｎｄｉｍｐｌｉｃａｔｉｏｎｔｈｅｏｒｙｏｆ ｓｈａｐｅｇｒａｐｈｓ，ａｓｗｅｌｌａｓｔｈｅｉｒｄｅｃｉｓｉｏｎｐｒｏｃｅｄｕｒｅｓａｎｄａｐｐｌｉｃａｔｉｏｎｓ．Ｆｉｒｓｔ，ｗｅｉｎｖｅｓｔｉｇａｔｅｔｈｅ ｓｈａｐｅｇｒａｐｈｔｈｅｏｒｙｕｓｉｎｇａｎａｌｏｇｏｕｓｍｅｔｈｏｄｓｔｏｔｈｏｓｅｉｎｓｔｕｄｙｉｎｇｔｈｅｔｈｅｏｒｙｏｆａｌｇｅｂｒａｉｃｓｐｅｃｉｆｉｃａｔｉｏｎ， ｗｈｅｒｅｓｈａｐｅｇｒａｐｈｓａｎｄｔｈｅｉｒｅｑｕｉｖａｌｅｎｃｅｒｕｌｅｓａｎｄｉｍｐｌｉｃａｔｉｏｎｒｕｌｅｓａｒｅａｎａｌｏｇｏｕｓｔｏａｌｇｅｂｒａｉｃ ｔｅｒｍｓａｎｄｔｈｅｉｒｅｑｕａｌｉｔｙｒｕｌｅｓａｎｄｒｅｗｒｉｔｉｎｇｒｕｌｅｓ，ｒｅｓｐｅｃｔｉｖｅｌｙ．Ａｎａｌｏｇｏｕｓｌｙ，ｗｅｄｅｆｉｎｅｔｈｅ ｓｙｎｔａｃｔｉｃｔｈｅｏｒｙａｎｄｓｅｍａｎｔｉｃｔｈｅｏｒｙｏｆｓｈａｐｅｇｒａｐｈｓ，ａｎｄｔｈｅｎｄｅｆｉｎｅｔｈｅｓｈａｐｅｇｒａｐｈｒｅｗｒｉｔｉｎｇ ｓｙｓｔｅｍａｓｗｅｌｌａｓｉｔｓｔｅｒｍｉｎａｔｉｏｎ，ｌｏｃａｌｃｏｎｆｌｕｅｎｃｅａｎｄｃｏｎｆｌｕｅｎｃｅ．Ｂａｓｅｄｏｎｔｈｅｓｅｄｅｆｉｎｉｔｉｏｎｓ，ｗｅ ｐｒｅｓｅｎｔｄｅｃｉｓｉｏｎｍｅｔｈｏｄｓｏｎｄｅｃｉｄｉｎｇｔｈｅｅｑｕａｌｉｔｙａｎｄｉｍｐｌｉｃａｔｉｏｎｏｆｓｈａｐｅｇｒａｐｈｓｂｙｒｅｗｒｉｔｉｎｇ ｓｈａｐｅｇｒａｐｈｓ．Ｓｅｃｏｎｄｌｙ，ｗｅｐｒｏｐｏｓｅｍｅｔｈｏｄｓｆｏｒａｕｔｏｍａｔｉｃａｌｌｙｉｎｆｅｒｒｉｎｇｌｏｏｐｉｎｖａｒｉａｎｔｓｈａｐｅ ｇｒａｐｈｓａｓｗｅｌｌａｓｔｈｅｐｒｅａｎｄｐｏｓｔｓｈａｐｅｇｒａｐｈｓｏｆｒｅｃｕｒｓｉｖｅｆｕｎｃｔｉｏｎｓ．Ｗｉｔｈｔｈｅｈｅｌｐｏｆｔｈｅ ｄｅｃｉｓｉｏｎｐｒｏｃｅｄｕｒｅｓｆｏｒｔｈｅｓｈａｐｅｇｒａｐｈｔｈｅｏｒｙ，ｔｈｅｐｒｏｐｏｓｅｄｍｅｔｈｏｄｆｏｒｉｎｆｅｒｒｉｎｇｌｏｏｐｉｎｖａｒｉａｎｔ ｓｈａｐｅｇｒａｐｈｓｈａｓｂｅｅｎａｄａｐｔｅｄｆｒｏｍａｇｅｎｅｒａｌｍｅｔｈｏｄｆｏｒｉｎｆｅｒｒｉｎｇｌｏｏｐｉｎｖａｒｉａｎｔｓｂａｓｅｄｏｎ ａｂｓｔｒａｃｔｉｎｔｅｒｐｒｅｔａｔｉｏｎ．Ｓｉｎｃｅａｔｅｒｍｉｎａｌｒｅｃｕｒｓｉｖｅｆｕｎｃｔｉｏｎｈａｓａｔｌｅａｓｔｏｎｅｎｏｎｒｅｃｕｒｓｉｖｅｅｘｉｔ，ｔｈｅ ｉｎｉｔｉａｌｐｏｓｔｓｈａｐｅｇｒａｐｈｓｏｆｔｈｅｆｕｎｃｔｉｏｎｃａｎｂｅｉｎｆｅｒｒｅｄａｌｏｎｇｔｈｅｎｏｎｒｅｃｕｒｓｉｖｅｐａｔｈ，ａｎｄｔｈｅｎ ｐｏｓｔｓｈａｐｅｇｒａｐｈｓｃａｎｂｅｉｔｅｒａｔｉｖｅｌｙｉｎｆｅｒｒｅｄａｌｏｎｇｔｈｅｒｅｃｕｒｓｉｖｅｐａｔｈｓ．Ａｃｃｏｒｄｉｎｇｌｙ，ｔｈｅｐｒｅａｎｄ ｐｏｓｔｓｈａｐｅｇｒａｐｈｓｏｆｒｅｃｕｒｓｉｖｅｆｕｎｃｔｉｏｎｓｃａｎｂｅｉｎｆｅｒｒｅｄｌｉｋｅｔｈｅｍｅｔｈｏｄｉｎｆｅｒｒｉｎｇｌｏｏｐｉｎｖａｒｉａｎｔ ｓｈａｐｅｇｒａｐｈｓ．Ｔｈｉｒｄｌｙ，ｂｙｒｅｆｅｒｅｎｃｉｎｇｔｈｅＮｅｌｓｏｎＯｐｐｅｎｃｏｍｂｉｎａｔｉｏｎｍｅｔｈｏｄ，ｗｅｐｒｏｐｏｓｅａ ｄｅｃｉｓｉｏｎｍｅｔｈｏｄｆｏｒｔｈｅｃｏｍｂｉｎａｔｉｏｎｏｆｔｈｅｔｈｅｏｒｙｏｆｓｈａｐｅｇｒａｐｈｓａｎｄｉｎｔｅｇｅｒｔｈｅｏｒｙ．Ｆｏｒ ｍｕｔａｂｌｅｄａｔａｓｔｒｕｃｔｕｒｅｓ，ｉｎａｄｄｉｔｉｏｎｔｏｃａｒｉｎｇａｂｏｕｔｗｈｅｔｈｅｒｎｏｄｅｓｏｆａｄａｔａｓｔｒｕｃｔｕｒｅｆｏｒｍｔｈｅ ｐｒｅｄｅｔｅｒｍｉｎｅｄｓｈａｐｅ，ｆｅａｔｕｒｅｓｓｕｃｈａｓｄａｔａａｒｒａｎｇｅｍｅｎｔｂｅｔｗｅｅｎｎｏｄｅｓａｒｅａｌｓｏｃａｒｅｄ．Ｓｕｃｈ ｆｅａｔｕｒｅｓｃａｎｎｏｔｂｅｄｉｖｏｒｃｅｄｆｒｏｍｔｈｅｓｈａｐｅｆｅａｔｕｒｅｏｆｍｕｔａｂｌｅｄａｔａｓｔｒｕｃｔｕｒｅｓ，ａｎｄｃａｎｎｏｔｂｅ ｖｅｒｉｆｉｅｄａｌｏｎｅ．Ｔｈｅｒｅｆｏｒｅ，ａｃｃｏｒｄｉｎｇｔｏｔｈｅｃｈａｒａｃｔｅｒｉｓｔｉｃｓｏｆｖｅｒｉｆｉｃａｔｉｏｎｃｏｎｄｉｔｉｏｎｓｇｅｎｅｒａｔｅｄ ｆｒｏｍｓｕｃｈｐｒｏｇｒａｍｓ，ｔｈｅｐｒｏｐｏｓｅｄｃｏｍｂｉｎａｔｉｏｎｍｅｔｈｏｄｕｓｅｓｓｈａｐｅｇｒａｐｈｓｏｂｔａｉｎｅｄｆｒｏｍｐｒｏｇｒａｍ ａｎａｌｙｓｉｓｔｏｇｒｏｕｐｓｙｍｂｏｌｉｃａｓｓｅｒｔｉｏｎｓｂｙｓｈａｐｅｇｒａｐｈｎｏｄｅｓ；ｔｈｅｎｕｓｅｓｉｎｔｅｇｅｒｔｈｅｏｒｙｔｏｉｎｆｅｒａｓ ｍａｎｙｐｒｏｐｅｒｔｉｅｓａｓｐｏｓｓｉｂｌｅｆｏｒｔｈｅｎｏｄｅｓ；ａｎｄｆｉｎａｌｌｙｐａｓｓｅｓｔｈｅｇｒｏｕｐｅｄａｓｓｅｒｔｉｏｎｓａｎｄｐｒｏｐｅｒｔｉｅｓｔｏ ｔｈｅＺ３ｔｈｅｏｒｅｍｐｒｏｖｅｒｆｏｒａｕｔｏｍａｔｉｃｖｅｒｉｆｉｃａｔｉｏｎ．Ｔｈｉｓｍｅｔｈｏｄｃａｎｅｆｆｅｃｔｉｖｅｌｙａｖｏｉｄｆａｉｌｕｒｅｓｔｏ ｐｒｏｖｅｖｅｒｉｆｉｃａｔｉｏｎｃｏｎｄｉｔｉｏｎｓ．Ｂａｓｅｄｏｎｔｈｅｓｈａｐｅｇｒａｐｈｔｈｅｏｒｙａｎｄｔｈｅｗｏｒｋｏｆｔｈｉｓｐａｐｅｒ，ｏｕｒ ｐｒｏｔｏｔｙｐｅｏｆｐｒｏｇｒａｍｖｅｒｉｆｉｃａｔｉｏｎｓｙｓｔｅｍａｌｌｅｖｉａｔｅｓｔｈｅｂｕｒｄｅｎｏｆａｕｔｏｍａｔｅｄｔｈｅｏｒｅｍｐｒｏｖｅｒｓ，ａｎｄ ｃａｎｖｅｒｉｆｙｐｒｏｇｒａｍｓｍａｎｉｐｕｌａｔｉｎｇｍｏｒｅｃｏｍｐｌｅｘｍｕｔａｂｌｅｄａｔａｓｔｒｕｃｔｕｒｅｓ，ｓｕｃｈａｓｉｎｓｅｒｔｆｕｎｃｔｉｏｎｓ ａｎｄｄｅｌｅｔｅｆｕｎｃｔｉｏｎｓｏｆｓｏｒｔｅｄｃｉｒｃｕｌａｒｄｏｕｂｌｙｌｉｎｋｅｄｌｉｓｔ，ｂｉｎａｒｙｓｅａｒｃｈｔｒｅｅ，ｓｐｌａｙｔｒｅｅ，ｔｒｅａｐ， ｂａｌａｎｃｅｄｂｉｎａｒｙｔｒｅｅａｎｄＡＡｔｒｅｅ． 犓犲狔狑狅狉犱狊ｓｈａｐｅｇｒａｐｈｌｏｇｉｃ；ｓｈａｐｅａｎａｌｙｓｉｓ；ｐｒｏｇｒａｍｖｅｒｉｆｉｃａｔｉｏｎ；ａｕｔｏｍａｔｅｄｔｈｅｏｒｅｍｐｒｏｖｉｎｇ； ｌｏｏｐｉｎｖａｒｉａｎｔｉｎｆｅｒｅｎｃｅ １引言 形式验证（包括抽象解释、模型检测和演绎验证 等途径）是提高软件可信程度的重要方法，并在工业 界已经逐步得到应用，尤其是抽象解释和模型检测． 例如，空客公司在Ａ４００Ｍ军用运输机以及Ａ３８０和 Ａ３５０客机的开发上，已经用形式验证取代了部分安 全攸关嵌入式软件的测试．和单元测试相比，单元证 明降低了投入，主要是因为它方便了维护［１］．演绎验 证在工业界的应用虽有限但也在拓展，达索航空公 司在健壮性的形式验证方面，已有约１５％的断言是 用演绎验证方式证明的［１］． 在演绎验证方法中，有关自动程序验证的大部 分研究按这样的途径开展：程序员提供函数前后条 件和循环不变式，系统对程序采用某种正向或逆向 １２期 张昱等：形状图理论的定理证明 ２４６１