ISSN 1000-9825,CODEN RUXUEW E-mail:jos@iscas.ac.cn Journal of Sofnare,Vol.20,No.8,August 2009,pp.2037-2050 http://www.jos.org.cn doi:10.3724/SP.J.1001.2009.00572 Tel/Fax:+86-10-62562563 by Institute of Sofare,the Chinese Academy of Sciences.All rights reserved. 用于指针逻辑的自动定理证明器” 王振明片，陈意云}，王志芳之 '(中因科学技术大学计算机科学技术系，安徽合肥230026) (中国科学技术大学苏州研究院软件安全实验室，江苏苏州215123) Automated Theorem Prover for Pointer Logic WANG Zhen-Ming,CHEN Yi-Yun',WANG Zhi-Fang? (Department of Computer Science and Technology,University of Science and Technology of China,Hefei 230026,China) (Software Security Laboratory,Suzhou Institute for Advanced Study,University of Science and Technology of China,Suzhou 215123, China) Corresponding author:E-mail:zmwang4@mail.ustc.edu.cn,http://ssg.ustcsz.edu.cn/ Wang ZM,Chen YY,Wang ZF.Automated theorem prover for pointer logic.Journal of Software,2009,20(8): 2037-2050.http:/www.jos.org.cn/1000-9825/572.htm Abstract:This paper presents a technique for designing theorem prover which mainly based on transformation and substitution for Pointer Logic.The technique realized as a tool called APL is implemented.The APL theorem prover is fully automated with which proofs can be recorded and checked efficiently.The tool is tested on pointer programs mainly about singly-linked lists,doubly-linked lists and binary trees. Key words:pointer program;pointer logic;verification condition;automated theorem prover,proof checker 摘要：提出了一种为指针逻辑设计定理证明器的新技术，该项技术主要是基于变换和替代，己在APL的工具中 得以实现APL自动定理证明器是完全自动的，且其产生的证明可以被有效地记录和检验.已使用关于单链表、双链 表和二又树的指针程序测试了该自动定理证明器】 关键词：指针程序：指针逻辑：验证条件；自动定理证明器：证明检查器 中图法分类号：TP301 文献标识码：A 1 Introduction With increased complexity of missions,the need for high quality and safety-critical software has increased dramatically over the past few years.Formal methods have been used in the development of many safety-critical systems in the form of formal specification and formal proof of correctness.A wide variety of different logics have been developed for formal methods.Building theorem provers for each of these logics is a massive challenge Among all the existing popular theorem provers,PVS is a proprietary system for developing formal specifications,of which the PVS proof checker is one component.Isabelleis a generic theorem prover,allowing ·Supported by the National Natural Science Foundation of China under Grant Nos.60673126,90718026(国家自然科学基金) Received 2008-05-25;Revised 2008-08-28;Accepted 2008-10-09 ⊙中国科学院软件研究所htp/ww.j0s.org.cn
ISSN 1000-9825, CODEN RUXUEW E-mail: jos@iscas.ac.cn Journal of Software, Vol.20, No.8, August 2009, pp.2037−2050 http://www.jos.org.cn doi: 10.3724/SP.J.1001.2009.00572 Tel/Fax: +86-10-62562563 © by Institute of Software, the Chinese Academy of Sciences. All rights reserved. 用于指针逻辑的自动定理证明器∗ 王振明 1+, 陈意云 1 , 王志芳 2 1 (中国科学技术大学 计算机科学技术系,安徽 合肥 230026) 2 (中国科学技术大学 苏州研究院 软件安全实验室,江苏 苏州 215123) Automated Theorem Prover for Pointer Logic WANG Zhen-Ming1+, CHEN Yi-Yun1 , WANG Zhi-Fang2 1 (Department of Computer Science and Technology, University of Science and Technology of China, Hefei 230026, China) 2 (Software Security Laboratory, Suzhou Institute for Advanced Study, University of Science and Technology of China, Suzhou 215123, China) + Corresponding author: E-mail: zmwang4@mail.ustc.edu.cn, http://ssg.ustcsz.edu.cn/ Wang ZM, Chen YY, Wang ZF. Automated theorem prover for pointer logic. Journal of Software, 2009,20(8): 2037−2050. http://www.jos.org.cn/1000-9825/572.htm Abstract: This paper presents a technique for designing theorem prover which mainly based on transformation and substitution for Pointer Logic. The technique realized as a tool called APL is implemented. The APL theorem prover is fully automated with which proofs can be recorded and checked efficiently. The tool is tested on pointer programs mainly about singly-linked lists, doubly-linked lists and binary trees. Key words: pointer program; pointer logic; verification condition; automated theorem prover; proof checker 摘 要: 提出了一种为指针逻辑设计定理证明器的新技术,该项技术主要是基于变换和替代,已在 APL 的工具中 得以实现.APL 自动定理证明器是完全自动的,且其产生的证明可以被有效地记录和检验.已使用关于单链表、双链 表和二叉树的指针程序测试了该自动定理证明器. 关键词: 指针程序;指针逻辑;验证条件;自动定理证明器;证明检查器 中图法分类号: TP301 文献标识码: A 1 Introduction With increased complexity of missions, the need for high quality and safety-critical software has increased dramatically over the past few years. Formal methods have been used in the development of many safety-critical systems in the form of formal specification and formal proof of correctness. A wide variety of different logics have been developed for formal methods. Building theorem provers for each of these logics is a massive challenge. Among all the existing popular theorem provers, PVS[1] is a proprietary system for developing formal specifications, of which the PVS proof checker is one component. Isabelle[2,3] is a generic theorem prover, allowing ∗ Supported by the National Natural Science Foundation of China under Grant Nos.60673126, 90718026 (国家自然科学基金) Received 2008-05-25; Revised 2008-08-28; Accepted 2008-10-09
2038 Journal of Software软件学报Vol.20,No.8,August2009 different logics to be defined by users.Nuprll4l is an interactive proof system for constructive mathematics based on Martin-Lofs Type Theory.Coqls]is a proof assistant for the Calculus of Inductive Constructions and Coq uses the natural deduction proof style.ACL26]is a heavily automated,first order theorem prover specifically designed to support the specification and development of computing systems.As is well known,this area is characterized by its wide variety of proof methods,forms of automated deduction and applications. This paper concerns with automated theorem proving for Pointer Logic,which is an extension of Hoare logic and essentially is a pointer analysis tool.Pointer Logic is designed for PointerCls which is a C-like programming language.In Pointer Logic,pointers are classified into effective pointers (those point to objects)and ineffective pointers which contain null pointers and dangling pointers.Pointer Logic collects pointer information including whether a pointer is null,dangling or effective,the equality between effective pointers in a forward manner.And the collected information can then be used to prove that the program satisfies the requests of user-defined safety policies such as type safety and memory safety.To meet the safety requirements of software,some undecidable pointer operations have been restrained in PointerC.Thus we can obtain accurate pointer analysis instead of an imprecise one. In our earlier work,we designed a certifying compiler called PLCCl for PointerC.In our original implementation,not all the verification conditions (VCs)generated by the verification condition generator(VCG) could be proved automatically by the theorem prover embedded in the compiler and those VCs need to be proved interactively by programmers using the proof-assistant tool-Coq.Consequently it made the tool difficult to use by one who is not an expert in Coq.Besides,the early version of PLCC can handle only a few simple programs written in PointerC.This is because the programming language constructs such as pointers,structures and unions are not directly supported by the existing provers,and are often encoded imprecisely by using axioms and uninterrupted functionsl0.To solve those problems,we have developed a new powerful automated theorem prover called APL for the PLCC system. Our paper makes the following contributions: 1.We present a new technique for designing automated theorem prover which mainly proves proof obligations manipulating pointers; 2.A fully automated theorem prover using this technique has been implemented for Pointer Logic; 3.Machine checkable proofs could be generated,recorded and checked efficiently by this tool; 4.The realization of the automated theorem prover APL makes our earlier certifying compiler PLCC more powerful now. In this paper,we introduce Pointer Logic,and the design and implementation of our automated theorem prover. The rest of the paper is organized as follows.Section 2 describes Pointer Logic.In Section 3 we give an overview of the whole theorem prover and introduce the verification condition.We describe the verification condition checker, which checks if the verification condition to be proved violates the rules of Pointer Logic in Section 4.In Section 5, we explain how the proofs are generated and recorded.Proof checking is described in Section 6.Section 7 shows the experimental results.Section 8 compares our work with related work and Section 9 concludes the paper. 2 Pointer Logic Pointer Logic is an extension of Hoare logic and it essentially is a pointer analysis tool.The basic idea of Pointer Logic is to represent memory states by means of sets of pointers.Pointer Logic consists of an assertion language,a set of axioms and inference rules.The interested reader can find a detailed description of Pointer Logic in Refs.[7,9]. ⊙中国科学院软件研究所htp/ww.j0s.org.cn
2038 Journal of Software 软件学报 Vol.20, No.8, August 2009 different logics to be defined by users. Nuprl[4] is an interactive proof system for constructive mathematics based on Martin-Löf's Type Theory. Coq[5] is a proof assistant for the Calculus of Inductive Constructions and Coq uses the natural deduction proof style. ACL2[6] is a heavily automated, first order theorem prover specifically designed to support the specification and development of computing systems. As is well known, this area is characterized by its wide variety of proof methods, forms of automated deduction and applications. This paper concerns with automated theorem proving for Pointer Logic[7], which is an extension of Hoare logic and essentially is a pointer analysis tool. Pointer Logic is designed for PointerC[8] which is a C-like programming language. In Pointer Logic, pointers are classified into effective pointers (those point to objects) and ineffective pointers which contain null pointers and dangling pointers. Pointer Logic collects pointer information including whether a pointer is null, dangling or effective, the equality between effective pointers in a forward manner. And the collected information can then be used to prove that the program satisfies the requests of user-defined safety policies such as type safety and memory safety. To meet the safety requirements of software, some undecidable pointer operations have been restrained in PointerC. Thus we can obtain accurate pointer analysis instead of an imprecise one. In our earlier work, we designed a certifying compiler called PLCC[9] for PointerC. In our original implementation, not all the verification conditions (VCs) generated by the verification condition generator (VCG) could be proved automatically by the theorem prover embedded in the compiler and those VCs need to be proved interactively by programmers using the proof-assistant tool—Coq. Consequently it made the tool difficult to use by one who is not an expert in Coq. Besides, the early version of PLCC can handle only a few simple programs written in PointerC. This is because the programming language constructs such as pointers, structures and unions are not directly supported by the existing provers, and are often encoded imprecisely by using axioms and uninterrupted functions[10]. To solve those problems, we have developed a new powerful automated theorem prover called APL for the PLCC system. Our paper makes the following contributions: 1. We present a new technique for designing automated theorem prover which mainly proves proof obligations manipulating pointers; 2. A fully automated theorem prover using this technique has been implemented for Pointer Logic; 3. Machine checkable proofs could be generated, recorded and checked efficiently by this tool; 4. The realization of the automated theorem prover APL makes our earlier certifying compiler PLCC more powerful now. In this paper, we introduce Pointer Logic, and the design and implementation of our automated theorem prover. The rest of the paper is organized as follows. Section 2 describes Pointer Logic. In Section 3 we give an overview of the whole theorem prover and introduce the verification condition. We describe the verification condition checker, which checks if the verification condition to be proved violates the rules of Pointer Logic in Section 4. In Section 5, we explain how the proofs are generated and recorded. Proof checking is described in Section 6. Section 7 shows the experimental results. Section 8 compares our work with related work and Section 9 concludes the paper. 2 Pointer Logic Pointer Logic is an extension of Hoare logic and it essentially is a pointer analysis tool. The basic idea of Pointer Logic is to represent memory states by means of sets of pointers. Pointer Logic consists of an assertion language, a set of axioms and inference rules. The interested reader can find a detailed description of Pointer Logic in Refs.[7,9]
王振明等：用于指针逻辑的自动定理证明器 2039 Our certifying compiler PLCC supports a source language called PointerC which equipped with both a type system and a logic system.PointerC is a C-like imperative language,which excludes pointer arithmetic and the address-of operation.These restrictions are based on the premise of not affecting the functionality of PointerC and this makes checking more pointer programs statically possible.We use the logic system to help reason the side conditions in the typing rules and then support value-sensitive static checking.In the following,we will give a brief introduction to this logic system called Pointer Logic.Due to the limitation of space,we will not describe the axioms and inference rules of Pointer Logic in the following subsections. 2.1 Conventions and notations In Pointer Logic,we represent states by means of sets of pointers (or access paths,which are introduced later) and we classify pointers into three kinds:effective pointers(those point to dynamically allocated objects),null pointers and dangling pointers.At any program point,we use /7to denote set of effective pointers,use N to denote the set of null pointers;use D to denote the set of dangling pointers.The null pointers and dangling pointers are also called ineffective pointers.N and D are used for the purpose of detecting possible memory errors such as null dereference or using an ineffective pointer as actual parameter of function free.The elements of set N and set D are pointers while the elements of /7are sets of pointers when N,D,/7are not empty.We use S to denote the elements of /7 the suffix n represents the dimension of /7.Note that the order of S in /7 does not matter.For example,if p,q),(m,n,we let S=p,q,S2=(m,n),we call p,q,m,n all effective pointers,and p,q are equal pointers (but not aliases),m,n are equal pointers (but not aliases).According to Point Logic,p and g in S should not be equal to any other pointers in S2 and vice versa.Next,we introduce the concepts of equality and aliasing of pointers. We say that two pointers are equal if their r-values are equal.We say that two pointers are aliases if their I-values are equal. In our Logic,a heap is represented by a directed graph.Each dynamically allocated object is a vertex in a graph.The access paths maintain the topological structure by connecting vertices in the graph.Access paths are a special kind of strings that satisfies certain syntactical requirements.Thus we introduce the notation of prefix.For example,.p→next is a prefix of p-→next→nexl,and p is a prefix of p→next-→nexl.Pointer Logic concerns pointer aliasing which occurs when two or more access paths refer the same storage location at the same program point. Different access paths are assumed to bound to different storage locations,unless it can be proved that they are bound to the same location(those bound to the same location are aliases)therefore,equality information of effective pointers is needed to deduce the access paths that are bound to the same location. 2.2 Assertion language In the following figure we show the syntax of the assertion language,which is used to annotate the source program in PointerC.We omitted the definition of boolexp.Actually,it is a Boolean expression,and it can be value TRUE,FALSE,or conjunction,disjunction,negation,and so on.Here means null.The definition of /7 N and D is just the same form as we described above.And /val can be considered as the pointer or the access path we mentioned in Section 2.1.Let us take p(>next)'as an example to explain the meaning of /val(>id)ex.p(>nexr)is the abbreviation for p->next->next->next.And id is a string over the alphabet [0..9a..zA..Z].If the effective pointer set or the null pointer set or the dangling pointer set is empty,then {..or {...N or {...p will not appear in the assertion. @中国科学院软件研究所htp/W.j0s.org.cn
王振明 等:用于指针逻辑的自动定理证明器 2039 Our certifying compiler PLCC supports a source language called PointerC which equipped with both a type system and a logic system. PointerC is a C-like imperative language, which excludes pointer arithmetic and the address-of operation. These restrictions are based on the premise of not affecting the functionality of PointerC and this makes checking more pointer programs statically possible. We use the logic system to help reason the side conditions in the typing rules and then support value-sensitive static checking. In the following, we will give a brief introduction to this logic system called Pointer Logic. Due to the limitation of space, we will not describe the axioms and inference rules of Pointer Logic in the following subsections. 2.1 Conventions and notations In Pointer Logic, we represent states by means of sets of pointers (or access paths, which are introduced later) and we classify pointers into three kinds: effective pointers (those point to dynamically allocated objects), null pointers and dangling pointers. At any program point, we use Π to denote set of effective pointers; use N to denote the set of null pointers; use D to denote the set of dangling pointers. The null pointers and dangling pointers are also called ineffective pointers. N and D are used for the purpose of detecting possible memory errors such as null dereference or using an ineffective pointer as actual parameter of function free. The elements of set N and set D are pointers while the elements of Π are sets of pointers when N, D, Π are not empty. We use Sn to denote the elements of Π, the suffix n represents the dimension of Π. Note that the order of Sn in Π does not matter. For example, if Π={{p,q},{m,n}}, we let S1={p,q}, S2={m,n}, we call p, q, m, n all effective pointers, and p, q are equal pointers (but not aliases), m, n are equal pointers (but not aliases). According to Point Logic, p and q in S1 should not be equal to any other pointers in S2 and vice versa. Next, we introduce the concepts of equality and aliasing of pointers. We say that two pointers are equal if their r-values are equal. We say that two pointers are aliases if their l-values are equal. In our Logic, a heap is represented by a directed graph. Each dynamically allocated object is a vertex in a graph. The access paths maintain the topological structure by connecting vertices in the graph. Access paths are a special kind of strings that satisfies certain syntactical requirements. Thus we introduce the notation of prefix. For example, p→next is a prefix of p→next→next, and p is a prefix of p→next→next. Pointer Logic concerns pointer aliasing which occurs when two or more access paths refer the same storage location at the same program point. Different access paths are assumed to bound to different storage locations, unless it can be proved that they are bound to the same location (those bound to the same location are aliases) therefore, equality information of effective pointers is needed to deduce the access paths that are bound to the same location. 2.2 Assertion language In the following figure we show the syntax of the assertion language, which is used to annotate the source program in PointerC. We omitted the definition of boolexp. Actually, it is a Boolean expression, and it can be value TRUE, FALSE, or conjunction, disjunction, negation, and so on. Here ε means null. The definition of Π, N and D is just the same form as we described above. And lval can be considered as the pointer or the access path we mentioned in Section 2.1. Let us take p(→next) 3 as an example to explain the meaning of lval(→id) exp. p(→next) 3 is the abbreviation for p→next→next→next. And id is a string over the alphabet [0..9a..zA..Z]. If the effective pointer set or the null pointer set or the dangling pointer set is empty, then {…}Π or {…}N or {…}D will not appear in the assertion
2040 Journal of Software软件学报Vol.20,No.8,August2009 ass :boolexpass ass ass (ass)I ass vass ass=ass id(Ival)3id dom.ass Vid dom.ass dom:=s exp..exp Ⅱ：={ssin N :=(Isw D:={D ss :ss,set set ser:=(In lI :Il,Ival|lval hval=id lval-→id|hal(-→id)p exp num I NULL I exp+exp I exp-exp I exp*exp 1... mm=011|2l. Pointer Logic is designed to be fit to collect pointer information in a forward manner.This information includes whether a pointer is null,dangling or effective,equality relation between effective pointers.The information collected is recorded in sets.From all of the above,one may find that Pointer Logic is a little different from all the other existing logics devised to prove pointer programs,although itself is an extension of Hoare logic. Considering the fact that it is not quantifier free,the pointer information is stored in set and it needs to take many pointer aliasing problems into account,it is a challenging problem to design an automated theorem prover for Pointer Logic. 3 Overview of the APL Theorem Prover The basic interface that an ATP provides takes as input a formula and returns a Boolean ("true","false") answer.In addition to this basic interface,ATP may generate proofs witnessing the validity of input formulas,this basic capability is essential to techniques such as Proof-Carrying Code(PCC)where the ATP is an untrusted and potentially complicated program and the proof generated by the ATP can be checked efficiently by a simple program.And our implementation is not an exception. Figure 1 gives an overview of the overall system architecture. Verification condition (VC) VC checker ◆Invalid VC Valid VC Decision proceduresVC+ProofProof checker Yes/No Fig.1 Overall structure of the APL theorem prover The system takes as input the verification condition generated by a verification condition generator embedded in the front end of the PLCC compiler.The VC is first propagated to the VC checker,which checks if the VC satisfies the rules of Pointer Logic,if not,the invalid VC will not be handled further more by the APL system.The valid one is put to the decision procedures which will generate its corresponding proofs if existed.Then the VC and ⊙中国科学院软件研究所hp/ww.j0s.org.cn
2040 Journal of Software 软件学报 Vol.20, No.8, August 2009 Yes/No :: exp | | | | ( ) | | | ( )| : . | : . :: :: :: :: :: :: :: :: :: exp :: :: ass bool ass ass ass ass ass ass ass ass id lval id dom ass id dom ass dom N D ss set ll lval num Ψ ε Ψ Π = ¬ ∧ ∨ ⇒ ∃ ∀ = = = = = = = = = = = exp | exp..exp | | | | | | |... { } { } { } , | { } , | | |() | | exp exp | exp exp | exp exp N D ND N DND ND ss ls ls ss set set ll ll lval lval id lval id lval id num NULL Π Π ΠΠ Π ∧ ∧ ∧ ∧ ∧ → → + − ∗ |... 0 | 1 | 2 |... Pointer Logic is designed to be fit to collect pointer information in a forward manner. This information includes whether a pointer is null, dangling or effective, equality relation between effective pointers. The information collected is recorded in sets. From all of the above, one may find that Pointer Logic is a little different from all the other existing logics devised to prove pointer programs, although itself is an extension of Hoare logic. Considering the fact that it is not quantifier free, the pointer information is stored in set and it needs to take many pointer aliasing problems into account, it is a challenging problem to design an automated theorem prover for Pointer Logic. 3 Overview of the APL Theorem Prover The basic interface that an ATP provides takes as input a formula and returns a Boolean (“true”, “false”) answer. In addition to this basic interface, ATP may generate proofs witnessing the validity of input formulas, this basic capability is essential to techniques such as Proof-Carrying Code (PCC)[11], where the ATP is an untrusted and potentially complicated program and the proof generated by the ATP can be checked efficiently by a simple program. And our implementation is not an exception. Figure 1 gives an overview of the overall system architecture. Verification condition (VC) Invalid VC Fig.1 Overall structure of the APL theorem prover The system takes as input the verification condition generated by a verification condition generator embedded in the front end of the PLCC compiler. The VC is first propagated to the VC checker, which checks if the VC satisfies the rules of Pointer Logic, if not, the invalid VC will not be handled further more by the APL system. The valid one is put to the decision procedures which will generate its corresponding proofs if existed. Then the VC and Valid VC VC checker Decision procedures VC+Proof Proof checker
王振明等：用于指针逻辑的自动定理证明器 2041 its proofs are propagated to the proof checker,which will check if the proofs are right or not.The correctness of our system doesn't depend on the correctness of the theorem prover.Instead,we only need trust the proof checker.The individual components of APL will be described in some details in the subsequent sections. 3.1 Verification condition In this section we describe the verification condition and introduce an example.First,the form of VC will be demonstrated,and then we present a VC example to help the reader to understand what the goals to be proved look like.The VC has the form as follows: prop→prop (e2.1.0) Each prop above is composed of eight parts,they are:Quant,I N,D,Pred,Darr,Notsure,En.The contents of each part are:Ouant contains the quantifiers,/7 contains the effective pointers,N contains the null pointers,D contains the dangling pointers,Pred contains the recursively defined predicates that appear in the annotations,Darr contains the dynamic array information,Notsure contains the pointers that are represented in the form of forall k: i.j(P),where P could be predicates or pointers,which have k at the exponential position.For example,Notsure may look like the form in (e 2.1.1)or (e 2.1.2).And the last part of prop is Em,which contains the integer linear arithmetic equalities and inequalities.For instance,the Em part may have the form shown in (e 2.1.3). forall(0.nl.(Tree(p→Ichild(-→rchildy-→Ichild) (e2.1.1) forall [.n.(C{p(→rchild,p(→r)'k-→Ichild}) (e2.1.2) i≥1&&iP2>..Pul D or[pu,Pz.Pul Predor [(id.D.(id Darror [(pu Pz,exp)(Pm P2exp] Notsureor [(p,expuexp2.exp),(pexpmexp2,exp)] Eninteger linear arithmetic expression In order to give the reader an overall impression of what the VCs look like,a practical example of VC that appears in the program list_rotate.c which is about the rotation operation on lists is given in Fig.2. As shown in the Fig.2,the first annotation between /*and*/defines an auxiliary predicate describing a singly-linked list.The second annotation between/*@and*/is the pre-condition of the whole function,and the last annotation between /*and*/is the post-condition of the whole function.For lack of space we omit the assertions inserted between the source codes.In this paper,we only consider the proof goals constructed from the verification condition between the /*THE VERIFICATION CONDITION IS:and*/,and do not care about how the verification condition are generated by the verification condition generator(VCG).There are 12 proof goals for the verification condition in the above example.Fig.3 shows some of these proof goals. We can find some facts about the proof obligations in Fig.3 to be proved:first,the goal that is going to be proved is not quantifier-free as shown in (p 2.2.1)and lots of former experiences indicate that this kind of proof ⊙中国科学院软件研究所hp/ww.j0s.org.cn
王振明 等:用于指针逻辑的自动定理证明器 2041 = } its proofs are propagated to the proof checker, which will check if the proofs are right or not. The correctness of our system doesn’t depend on the correctness of the theorem prover. Instead, we only need trust the proof checker. The individual components of APL will be described in some details in the subsequent sections. 3.1 Verification condition In this section we describe the verification condition and introduce an example. First, the form of VC will be demonstrated, and then we present a VC example to help the reader to understand what the goals to be proved look like. The VC has the form as follows: prop→prop (e 2.1.0) Each prop above is composed of eight parts, they are: Quant, Π, N, D, Pred, Darr, Notsure, Env. The contents of each part are: Quant contains the quantifiers, Π contains the effective pointers, N contains the null pointers, D contains the dangling pointers, Pred contains the recursively defined predicates that appear in the annotations, Darr contains the dynamic array information, Notsure contains the pointers that are represented in the form of forall k: i..j(P), where P could be predicates or pointers, which have k at the exponential position. For example, Notsure may look like the form in (e 2.1.1) or (e 2.1.2). And the last part of prop is Env, which contains the integer linear arithmetic equalities and inequalities. For instance, the Env part may have the form shown in (e 2.1.3). forall [0... ].( ( ( ) )) (e 2.1.1) i i n Tree p lchild rchild lchild →→ → (e 2.1.2) 1 forall [1... ].( {{ ( ) , ( ) }}) k k i k n P p rchild p r lchild → →→+ i in j ≥< = 1 & & & & 0 (e 2.1.3) As the above, the goal we are going to prove will be the form of the following: 1 111 1 1 1 1 2 222 2 2 2 2 { ,,,, , , , } { ,,,, , , , Goal Quant N D Pred Darr Notsure Env Quant N D Pred Darr Notsure Env Π Π → (e 2.1.4) And Quant exists n int : 11 12 1 1 2 [] or [[ , ,..., ],...,[ , ,..., ]] i mm m Π pp p p p p j p j 11 12 1 [] or [ , ,..., ] N pp p i 11 12 1 [] or [ , ,..., ] D pp i 1 11 12 1 1 2 [] or [( ,[ , ,..., ]),...,( ,[ , ,..., ])] Pred id p p p id p p p i nmm m 11 12 1 1 2 [] or [( , ,exp ),...,( , ,exp )] Darr p p p p mm m 1 11 12 13 1 2 3 [] or [( ,exp ,exp ,exp ),...,( ,exp ,exp ,exp )] Notsure p mm m m p Env integer linear arithmetic expression In order to give the reader an overall impression of what the VCs look like, a practical example of VC that appears in the program list_rotate.c which is about the rotation operation on lists is given in Fig.2. As shown in the Fig.2, the first annotation between /*and*/ defines an auxiliary predicate describing a singly-linked list. The second annotation between /*@ and*/ is the pre-condition of the whole function, and the last annotation between /*@ and*/ is the post-condition of the whole function. For lack of space we omit the assertions inserted between the source codes. In this paper, we only consider the proof goals constructed from the verification condition between the /*THE VERIFICATION CONDITION IS: and*/, and do not care about how the verification condition are generated by the verification condition generator (VCG). There are 12 proof goals for the verification condition in the above example. Fig.3 shows some of these proof goals. We can find some facts about the proof obligations in Fig.3 to be proved: first, the goal that is going to be proved is not quantifier-free as shown in (p 2.2.1) and lots of former experiences indicate that this kind of proof
2042 Journal of Software软件学报Vol.20,No.8,August2009 obligations is not easy to be proved automatically;second,not all the eight parts mentioned above will be used in the VC as shown in (p 2.2.2)and(p 2.2.3).Obviously,which part will be used depends on the program going to be proved;third,the existence of exponent that indicates how many the next exist as shown in (p 2.2.1)makes the VC not easy to prove.Due to all the facts mentioned above and the characteristics of Pointer Logic,the design and implementation of an automated theorem prover for Pointer Logic is different from that are used for the existing provers. Struct list int data; Struct list"next; list Struct list"p)= Nip P{p}&&lisp→nex)*/ @existsn:inl.(n21&&P{r}&&forallm-l](P{x(→nex)&&P{x(→nex）}&&N→nex)*") PH{xp}&&N{→nexI N{xp时/ Struct list list rotate(Struct listx,Struct listp) if (x!=mull) (p->nex=x; 3x=x-→next p=p→nert p→nexf=nll return x; /THE VERIFICATION CONDITION IS: P,{{pr-→nexl,{x}}&&Np-→1exl exists m:int.(Ppx next)"),next&&Nip-next&&forall2.n-1](Px next))n2sn) P{{xp}}&&N{→next N(x.p) (exists n:int.(n21 &&Px&&forall 1...n-11.(Pnext)&&P(pnexry&&Nixnext)) P{{xp}}&&N{x→nexl) N(x.p)*I 产@existsn:in.(n2l&&P{x}&&foralll.n-l(P{-→nex)i)&&P{p,x-→nex)}&&N(-→nex)+) P,{{xp}&&N{x→nert N(x.p Fig.2 An example of VC P{p,x-→next,{x}&&N{p-→Het→ (p2.2.1) exists n:int.(n21&&&&forall .n1](P(next)) &&P{p,x(-→ex))}&&N{x(→next)H") P{p,x→next,{xr}&&N{p-next→ (p2.2.2) B{x,P}&&N{x→nex P{{p,x→next,{x}&&N{p→next→ (p2.2.3) N(x,pl Fig.3 Examples of proof obligation ⊙中国科学院软件研究所hp/ww.j0s.org.cn
2042 Journal of Software 软件学报 Vol.20, No.8, August 2009 obligations is not easy to be proved automatically; second, not all the eight parts mentioned above will be used in the VC as shown in (p 2.2.2) and (p 2.2.3). Obviously, which part will be used depends on the program going to be proved; third, the existence of exponent that indicates how many the next exist as shown in (p 2.2.1) makes the VC not easy to prove. Due to all the facts mentioned above and the characteristics of Pointer Logic, the design and implementation of an automated theorem prover for Pointer Logic is different from that are used for the existing provers. Struct list { int data; Struct list*next; }; /*list(Struct list*p)= N{p} || Pi{{p}} && list(p→next)*/ /*@exists n: int.(n≥1 && P{{x}} && forall k[1...n−1].(Pi{{x(→next) k }}) && Pi{{x(→next) n }} && N{x(→next) 1+n }) || Pi{{x,p}} && N{→next} || N{x,p}*/ Struct list*list_rotate(Struct list*x,Struct list*p) {if (x!=null) {p→next=x; x=x→next; p=p→next; p→next=null return x; /*THE VERIFICATION CONDITION IS: Pi{{p,x→next,{x}} && N{p→next} || exists n: int.(Pi{{p,x next) n },{x next) n−1 },{x}} && N{p→next} && forall k[2...n−1].(Pi{{x next) k−1 }}) && n≥1 && 2≤n) || Pi{{x,p}} && N{x→next} || N{x,p} ⇒ (exists n: int.(n≥1 && Pi{{x}} && forall k[1...n−1].(Pi{{x(→next) k }}) && Pi{{p,x(→next) n }} && N{x(→next) 1+n }) || Pi{{x,p}} && N{x→next} || N{x,p}*/ } /*@exists n: int.(n≥1 && Pi{{x}} && forall k[1...n−1].(Pi{{x(→next) k }}) && Pi{{p,x(→next) n }} && N{x(→next) 1+n }) || Pi{{x,p}} && N{x→next} || N{x,p}*/ Fig.2 An example of VC {{ , },{ }} & & { } (p 2.2.1) : int.( 1 & & {{ }} & & forall [1... 1].( {{ ( ) }}) & & {{ , ( ) }} & & { ( i k i i n i P p x next x N p next exists n n P x k n P x next P p x next N x → → → ≥ − → → 1 ) }) {{ , },{ }} & & { } (p 2.2.2) {{ , }} & & { } {{ , },{ }} & & { } n i i i next P p x next x N p next P x p N x next P p x next x N p next → + → → → → → → → (p 2.2.3) Nxp {, } Fig.3 Examples of proof obligation
王振明等：用于指针逻辑的自动定理证明器 2043 4 VC Checker There is a good reason for designing such a checker:The verification condition generator generates a large number of VCs for the program being verified,and not all of those VCs are valid according to the properties of Pointer Logic.So there is no need to prove the invalid ones.The role of the VC checker is to check the VCs to be proved if they obey the rules of Pointer Logic before they are propagated to the main theorem proving decision procedures.Some of the rules used by the checker are listed as follows: These rules are directly derived from Pointer Logic.The meaning of these rules will be explained in the rest of this paragraph.The p in the rules (1)to (14)represents a pointer.The suffix 1,2 in /7 N and D indicate the corresponding premise or conclusion respectively.S represents a set which consists of effective pointers that are equal.Pointers in set S should be different from each other,and different sets in /7should not have intersection.In Ref.[7],the reader will find the details of /7 N,D and S.The meaning of rule (1)is that if p is in set /7 and Ni at the same time,then we get false.Rule(2)says that if p is in set /7 and Di at the same time,then we get false.The meaning of rule(3)and rule(4)is similar to that of rule(1)and rule(2).The meaning of rule (14)is that if p and g are in the same set S,and p,g are equal to each other,then we get false.Let us take rule(3)as an example,which indicates that if pointer p in the set N of the premise and it also in the set D of the premise,then we get false.This is because according to Pointer Logic,p should not be a null pointer or a dangling pointer simultaneously. The advantages of designing this VC checker will be shown by our experiments which will be introduced in Section 6.Let us take the program list_zip.c as an example,14 VCs that violate the rules defined in Fig.4 could be filtered out.The run-time cost of the VC checker itself is small,so it greatly saves the time cost of the whole proving process. perpsN perpeD 2) peNpeD③)pe,PEN(4 false false false false =S.S=PP PeS es,p=q(14) false Fig.4 Rules used by the VC checker 5 Proof Generation In this section,we present a new technique for designing theorem prover which mainly based on transformation and substitution for Pointer Logic.Taking the proof obligations to be proved into account,we adopt the method of compositional verification.The original proof goal is divided into small sub-goals,and then each of the new sub-goals is considered.If all of the sub-goals could be proved,then the original goal has a proof.We use all the proofs for the sub-goals to construct the proof of the original goal.In the rest of the section we will give some details about how the goal is splitted into sub-goals and how the sub-goals could be proved by using transformation and substitution. The original goal usually has the form of (e 2.1.4)as described in Section 3.1,and the sub-goals for it are shown in Fig.5. The reason for breaking the original Goal into these 7 sub-goals above is that,according to Pointer Logic,the information of pointers in the premise and conclusion of the proof goal should be equal if the goal could be proved. This is a little different from the traditional rules.In traditional rules,if the premise contains all the information of the conclusion,then the premise implies the conclusion.The fact we require strictly that the information in the premise and conclusion should be equal lies on the essence of Pointer Logic and the presentation of the program states(sets of pointers).This restriction is required only in proving the original goal,but not the sub-goals of it.The ⊙中国科学院软件研究所hp/ww.j0s.org.cn
王振明 等:用于指针逻辑的自动定理证明器 2043 4 VC Checker There is a good reason for designing such a checker: The verification condition generator generates a large number of VCs for the program being verified, and not all of those VCs are valid according to the properties of Pointer Logic. So there is no need to prove the invalid ones. The role of the VC checker is to check the VCs to be proved if they obey the rules of Pointer Logic before they are propagated to the main theorem proving decision procedures. Some of the rules used by the checker are listed as follows: These rules are directly derived from Pointer Logic. The meaning of these rules will be explained in the rest of this paragraph. The p in the rules (1) to (14) represents a pointer. The suffix 1, 2 in Π, N and D indicate the corresponding premise or conclusion respectively. S represents a set which consists of effective pointers that are equal. Pointers in set S should be different from each other, and different sets in Π should not have intersection. In Ref.[7], the reader will find the details of Π, N, D and S. The meaning of rule (1) is that if p is in set Π1 and N1 at the same time, then we get false. Rule (2) says that if p is in set Π1 and D1 at the same time, then we get false. The meaning of rule (3) and rule (4) is similar to that of rule (1) and rule (2). The meaning of rule (14) is that if p and q are in the same set S, and p, q are equal to each other, then we get false. Let us take rule (3) as an example, which indicates that if pointer p in the set N of the premise and it also in the set D of the premise, then we get false. This is because according to Pointer Logic, p should not be a null pointer or a dangling pointer simultaneously. The advantages of designing this VC checker will be shown by our experiments which will be introduced in Section 6. Let us take the program list_zip.c as an example, 14 VCs that violate the rules defined in Fig.4 could be filtered out. The run-time cost of the VC checker itself is small, so it greatly saves the time cost of the whole proving process. 1 1 1 1 1 1 2 2 1 1 2 ,, ,, (1) (2) (3) (4) ... false false false false [ ,..., ,..., ,..., ] [ , ,..., ] (14) false i jn l i i p p N p p D p Np D p p N S S S S S pp p p Sq Sp q Π Π Π Π ∈ ∈ ∈ ∈ ∈ ∈ ∈ ∈ = = ∈ ∈ ≡ Fig.4 Rules used by the VC checker 5 Proof Generation In this section, we present a new technique for designing theorem prover which mainly based on transformation and substitution for Pointer Logic. Taking the proof obligations to be proved into account, we adopt the method of compositional verification. The original proof goal is divided into small sub-goals, and then each of the new sub-goals is considered. If all of the sub-goals could be proved, then the original goal has a proof. We use all the proofs for the sub-goals to construct the proof of the original goal. In the rest of the section we will give some details about how the goal is splitted into sub-goals and how the sub-goals could be proved by using transformation and substitution. The original goal usually has the form of (e 2.1.4) as described in Section 3.1, and the sub-goals for it are shown in Fig.5. The reason for breaking the original Goal into these 7 sub-goals above is that, according to Pointer Logic, the information of pointers in the premise and conclusion of the proof goal should be equal if the goal could be proved. This is a little different from the traditional rules. In traditional rules, if the premise contains all the information of the conclusion, then the premise implies the conclusion. The fact we require strictly that the information in the premise and conclusion should be equal lies on the essence of Pointer Logic and the presentation of the program states (sets of pointers). This restriction is required only in proving the original goal, but not the sub-goals of it. The
2044 Journal of Software软件学报Vol.20,No.8,August2009 equality of the information of pointers will be checked by the proof checker.Goah to Goals are about pointers and Goal,is about integer linear arithmetic.The Quant part is treated specially by the decision procedures we have implemented and does not appear as a sub-goal in Fig.5. Goal1兰{Qal1,I,N1,D,Pred,Dar,Notsur%,Ey}→ GoalQuant,Ih,N:D,Pred Darn,Notsure Em {几2； (N) Goal(Quanh,N:D.Pred Darn,Notsure.Em GoalQuanh,I.ND.Pred,Darn,Notsure,Em {D3} Pred, Goal,Quant.I,N:D.Pred,Darr,Notsure.Emv GoalQuant.N.D.Pred,Darn,Notsure.Em Dar Notsurez Goal,兰{Quant,L,N,D,Pred,Dari,Notsure,Em}→ Quant,Eny, Fig.5 The sub-goals for the original goal VC(Quanh,I,N D,Pred,Darn,Notsure,Env, (Ouant,I,N2,D,Pred,Darr,Notsure,Env) L2s口 (RI) VC'(Quanh,I-,N,D,Pred Darn,Notsure Em (Quant,N2,D2;Predz,Darn,Notsurez,Env) VC(Quanh,N,D,Predi,Darn,Notsure,Em, (Quant,I,N2,D2,Predz,Darn,Notsurez,Env) Em1→Ew2 (R2) VC(Ouanh,I,N,D,Pred Darn,Notsure, (Quant,N2,D,Predz,Darn,Notsure) VC(Quanh,I,N.D,Pred Darr,Notsure,Em (p,qeI lval in VC .(R3) [q/p]lval,in VC forallk m..nexp e Notsure m<n (R4) Notsure'=Notsure-(forall k:m..nexp) forall k:m.nexpe Notsure forallk:n+1.lexpe Notsure (R5) Notsure'=Notsure+(forall k:m.Jexp)-(forall k:m..nexp,forallk:n+1.Jexp) In this paragraph,we will give an introduction to some of the rules used by the decision procedures.These rules are shown in the above figure.Rule RI means that if I is a subset of /7,then the original VC can be transformed to VC,and 7-1 means I7 minus I,as we know,I7 and I are sets.Rule R2 says that if Em implies Em2 then we can get VCfrom VC.Rule R3 describes the substitution of prefix of /val.The Ivalp represents all the Ivals that have prefix p in VC,if (p,q)is an element of 7,then we can substitute all the appearance of p in Ivalp with g.Rule R4 and R5 are used to help proving Goals as shown in Fig.5.Rule R4 says that if the upper bound n is small than the lower bound m for an element of Notsure,then we can delete this element from Notsure and get Notsure'.Rule R5 combines two elements of Notsure into one to get Notsure',by adding the new one to set Notsure and deleting the original two from Notsure.There are also kinds of rules designed for predicates,such as list,dlist and tree.Due to spaces limitations,we will not describe all of those rules used by our decision procedures. Let us see an example.When proving the above goal (p 4.1.1)in Fig.6,we first break this goal into two sub-goals (p 4.1.2)and (p 4.1.3).Now we need to prove two sub-goals:It is easy to prove (p 4.1.2),because the /7 part of the conclusion is a subset of the /7 part of the premise.When proving (p 4.1.3),predicate tree(res→rchild--→lchild)is handled first,we try to find out if tree(es→child-→Ichild④is in the Pred part of the premise,the testing result is that it is not in the Pred set of the premise,then we find pointers those are equal to ⊙中国科学院软件研究所hp/ww.j0s.org.cn
2044 Journal of Software 软件学报 Vol.20, No.8, August 2009 equality of the information of pointers will be checked by the proof checker. Goal1 to Goal6 are about pointers and Goal7 is about integer linear arithmetic. The Quant part is treated specially by the decision procedures we have implemented and does not appear as a sub-goal in Fig.5. 1 1 111 1 1 1 1 2 1 111 1 1 1 1 2 { , , , , , , , } { , , , , , , , } { } Goal Quant N D Pred Darr Notsure Env Goal Quant N D Pred Darr Notsure Env Π Π Π → → 2 3 1 111 1 1 1 1 4 1 111 1 1 1 1 2 { } { , , , , , , , } { , , , , , , , } { } N Goal Quant N D Pred Darr Notsure Env Goal Quant N D Pred Darr Notsure Env D Π Π → → 2 5 1 111 1 1 1 1 6 1 111 1 1 1 1 2 { } { , , , , , , , } { , , , , , , , } { } Pred Goal Quant N D Pred Darr Notsure Env Goal Quant N D Pred Darr Notsure Env Darr Π Π → → 2 7 1 111 1 1 1 1 2 2 { } { ,,,, , , , } { ,} Notsure Goal Quant N D Pred Darr Notsure Env Quant Env Π → Fig.5 The sub-goals for the original goal 1 111 1 1 1 1 2 222 2 2 2 2 2 1 1 1 2 11 1 1 1 1 ({ , , , , , , , }, { , , , , , , , }) ({ , , , , , , , } VC Quant N D Pred Darr Notsure Env Quant N D Pred Darr Notsure Env VC Quant N D Pred Darr Notsure Env Π Π Π Π Π Π ⊆ ′ − 222 2 2 2 2 ( 1) { , , , , , , }) R Quant N D Pred Darr Notsure Env 1 111 1 1 1 1 2 222 2 2 2 2 1 2 1 111 1 1 1 2 222 2 ({ , , , , , , , }, { , , , , , , , }) ({ , , , , , , }, { ,,,, , VC Quant N D Pred Darr Notsure Env Quant N D Pred Darr Notsure Env Env Env VC Quant N D Pred Darr Notsure Quant N D Pred Darr Π Π Π Π → ′ 2 2 ( 2) , }) R Notsure 1 1 111 1 1 1 1 1 1 1 { , , , , , , , }{ , } ( 3) [/ ] p p VC Quant N D Pred Darr Notsure Env p q lval in VC R q p lval in VC Π Π∈ forall : .. exp ( 4) {forall : .. exp} k m n Notsure m n R Notsure Notsure k m n ∈ < ′ = − forall : .. exp forall : 1.. exp ( 5) {forall : .. exp} {forall : .. exp, forall : 1.. exp} k m n Notsure k n l Notsure R Notsure Notsure k m l k m n k n l ∈ + ∈ ′ = + − + In this paragraph, we will give an introduction to some of the rules used by the decision procedures. These rules are shown in the above figure. Rule R1 means that if Π2 is a subset of Π1, then the original VC can be transformed to VC′, and Π1−Π2 means Π1 minus Π2, as we know, Π1 and Π2 are sets. Rule R2 says that if Env1 implies Env2 then we can get VC′ from VC. Rule R3 describes the substitution of prefix of lval. The lvalp represents all the lvals that have prefix p in VC1, if {p,q} is an element of Π1, then we can substitute all the appearance of p in lvalp with q. Rule R4 and R5 are used to help proving Goal6 as shown in Fig.5. Rule R4 says that if the upper bound n is small than the lower bound m for an element of Notsure, then we can delete this element from Notsure and get Notsure′. Rule R5 combines two elements of Notsure into one to get Notsure′, by adding the new one to set Notsure and deleting the original two from Notsure. There are also kinds of rules designed for predicates, such as list, dlist and tree. Due to spaces limitations, we will not describe all of those rules used by our decision procedures. Let us see an example. When proving the above goal (p 4.1.1) in Fig.6, we first break this goal into two sub-goals (p 4.1.2) and (p 4.1.3). Now we need to prove two sub-goals: It is easy to prove (p 4.1.2), because the Π part of the conclusion is a subset of the Π part of the premise. When proving (p 4.1.3), predicate tree(res→rchild→lchild) is handled first, we try to find out if tree(res→rchild→lchild) is in the Pred part of the premise, the testing result is that it is not in the Pred set of the premise, then we find pointers those are equal to
王振明等：用于指针逻辑的自动定理证明器 2045 pointer res-rchild from the /7 part of the conclusion.We find that p and res->rchild are in the same set,thus we substitute res->rchild with p,afterwards we check if tree(p->lchild)in the Pred part of the premise,if the answer is yes,then we prove the predicate tree(res->rchild->lchild).Next,we prove predicate tree(res->rchild>rchild),the proof process of this predicate is similar to the previous one,and we can prove it too.Lastly,we prove predicate tree(res->lchild),we find it in the Pred part of the premise.So we prove this predicate too.Finally,all of the predicates in the conclusion can be proved.So (p 4.1.3)can be proved.And the proof of each predicate consists of the proof of(p 4.1.3).If any of the predicates in the conclusion can not be proved,then(p 4.1.3)can not be proved either. P{{res→rchild,p,{res}}&&N{p-→Ichild&&tree(p-→rchild)&&tree(res→Ichild) (p4.1.10 P{{res→rchild.,pl,{res}}&&tree(res→rchild→Ichild)&&tree(res-→rchild→rchild)&&tree(res→Ichild) {tres→rchild,.p,fres}&&N{p→lchild&&tree(p→rchild&&tree(res→lchild (p4.1.2) Presrchild,p,res B{fres→rchild,.pl,fres}&&N{p→Ichildy&&tree(p-→rchild)&&tree(res→Ichild) (p4.1.3) tree(res→rchild→Ichild)&&ree(es→rchild→rchild)&&tree(res-→lchild) Fig.6 An example for predicate P{p,x→nexi,{x}&&N{p→next (newp2.2.1) (I≥1&&P{p,x(→next)},{x}&&forall k[1.~1+l.(P{(→next)})&&N{x(→next)l+}) As another example,let us consider the proof obligations in Fig.3.For(p 2.2.1),all appearances of n in the conclusion part are instantiated to integer 1 according to our proof strategies.Then we only need to prove the resulting proof goal:(new p 2.2.1).Now we break (new p 2.2.1)into 4 sub-goals,the reader will find out that each of these sub-goals is easy to prove.As to (p 2.2.2),there is no proof for it,and(p 2.2.3)will be filtered out by the VC checker. 5.1 Proof recording Necula strongly advocated that theorem provers ought to generate easily checkable proofs in his paper Just as he suggested,in our work some effort has been spent in trying to produce human readable results,which allows the user to examine the generated proofs.Furthermore,our proof file can be handled easily by machine.Our implementation is inspired by the work of Wongand the work of Geoffrey Norman Watson The type proof defined in SML for recording proofs in Fig.7 will help the reader to catch on how the proofs are recorded.Usually,a proof has 11 fields.Field name records the name of the proof.Field f1,2 record the information of N,D and Darr.Field f4 and f5 record the predicate information of Pred.Field f6,/7 record the information of /7.Field /8,f9 and f10 record the information of Notsure.As to Goah that we mentioned in Fig.5, which involves the Eny part,we only record the name of the proof of it.To a user,recording proof is a feature which can be enabled or disabled.The printing of proof details can be enabled or disabled too.When the printing of the proof detail is disabled,the printout only contains the name of proof for each sub-goal.The right part of Fig.7 gives the proof of(new p2.2.1)mentioned in Section 5. The process of recording proof and generating proof files can be divided into three stages: 1.Recording proofs of the sub-goals; 2. Generating a whole proof by combining all the above proofs in stage 1; @中国科学院软件研究所htp/W.j0s.org.cn
王振明 等:用于指针逻辑的自动定理证明器 2045 pointer res→rchild from the Π part of the conclusion. We find that p and res→rchild are in the same set, thus we substitute res→rchild with p, afterwards we check if tree(p→lchild) in the Pred part of the premise, if the answer is yes, then we prove the predicate tree(res→rchild→lchild). Next, we prove predicate tree(res→rchild→rchild), the proof process of this predicate is similar to the previous one, and we can prove it too. Lastly, we prove predicate tree(res→lchild), we find it in the Pred part of the premise. So we prove this predicate too. Finally, all of the predicates in the conclusion can be proved. So (p 4.1.3) can be proved. And the proof of each predicate consists of the proof of (p 4.1.3). If any of the predicates in the conclusion can not be proved, then (p 4.1.3) can not be proved either. {{ , },{ }} & & { } & & ( ) & & ( ) P res rchild p res N p lchild tree p rchild tree res lchild i → →→ → → ( 4.1.1) {{ , },{ }} & & ( ) & & ( ) & & ( ) {{ , },{ i i p P res rchild p res tree res rchild lchild tree res rchild rchild tree res lchild P res rchild p → → → → → → → res N p lchild tree p rchild tree res lchild }} & & { } & & ( ) & & ( ) →→ → → ( 4.1.2) {{ , },{ }} {{ , },{ }} & & { } & & ( ) & & ( ) i i p P res rchild p res P res rchild p res N p lchild tree p rchild tree res lchild → → →→ → → ( 4.1.3) ( ) & & p tree res rchild lchild tr → → ee res rchild rchild tree res lchild ( ) → → & & () → Fig.6 An example for predicate {{ , },{ }} & & { } (new P p x next x N p next i → → → 1 1 1 p 2.2.1) (1 1 & & {{ , ( ) },{ }} & & forall [1.. ~ 1 1].( {{ ( ) }}) & & { ( ) }) k P p x next x i i k P x next N x next + ≥ → + → → As another example, let us consider the proof obligations in Fig.3. For (p 2.2.1), all appearances of n in the conclusion part are instantiated to integer 1 according to our proof strategies. Then we only need to prove the resulting proof goal: (new p 2.2.1). Now we break (new p 2.2.1) into 4 sub-goals, the reader will find out that each of these sub-goals is easy to prove. As to (p 2.2.2), there is no proof for it, and (p 2.2.3) will be filtered out by the VC checker. 5.1 Proof recording Necula strongly advocated that theorem provers ought to generate easily checkable proofs in his paper[12]. Just as he suggested, in our work some effort has been spent in trying to produce human readable results, which allows the user to examine the generated proofs. Furthermore, our proof file can be handled easily by machine. Our implementation is inspired by the work of Wong[13−15] and the work of Geoffrey Norman Watson[16]. The type proof defined in SML for recording proofs in Fig.7 will help the reader to catch on how the proofs are recorded. Usually, a proof has 11 fields. Field name records the name of the proof. Field f1, f2 record the information of N, D and Darr. Field f3, f4 and f5 record the predicate information of Pred. Field f6, f7 record the information of Π. Field f8, f9 and f10 record the information of Notsure. As to Goal7 that we mentioned in Fig.5, which involves the Env part, we only record the name of the proof of it. To a user, recording proof is a feature which can be enabled or disabled. The printing of proof details can be enabled or disabled too. When the printing of the proof detail is disabled, the printout only contains the name of proof for each sub-goal. The right part of Fig.7 gives the proof of (new p2.2.1) mentioned in Section 5. The process of recording proof and generating proof files can be divided into three stages: 1. Recording proofs of the sub-goals; 2. Generating a whole proof by combining all the above proofs in stage 1;
2046 Journal of Software软件学报Vol.20,No.8,August2009 3. Outputting the proof generated in stage 2 to a text file or the terminal. |中华华华卡中中中华率华布中中中中中中华华*中小中中中中卡小中中中华*卡小中中中中*中中小中中中*中小。 The proof is: |中水水来华中中市*中水水水中中*中中水水中中中*中*中华卡事*中华华中中*中华华中华车华华中 type proof=(name:string, pred null f1:Nval list, paiin f2:Ival list, |f1:f2:f3:f4:f5: f1:f2:f3:f4:f5:f6:f7:f8:f9:f10: f3:(id(val list))list, lf6:{x,{p,x→nex)(I)月 |f7:f8:f9:f10: darr null f4:(id(val list))list, f5:(id(lval list))list, f1:f2:f3:f4:f5:f6:f7:f8:f9:f10: en trans equal f6:hal list list, |f1:x(→nexa)^(2) f7:hval list list, notsure_compare null (Ival*exp*exp*exp)list, |f2:x(-→nex)^(0)+() f1:f2:f3:f4:f5:f6:f7: f3:f4:f5:f6:7:f8:f9:f10:f8:forall k:[1..(1)-(1)(P((x(next)(k)) f9:(hval*exp*exp*exp)list, f10:(lval*exp"exp*exp)list f9:f10: 」dill |f1:f2:f3:f4:f5: eny true |f6:f7:f8:f9:f10: f1:f2:f3:f4:f5:f6:f7:f8:f9:f10: Fig.7 Definition of type proof and proof script for(new p 2.2.1) 6 Proof Checking In Ref.[15],the authors design a proof checker for three main reasons:first,the mechanically generated formal proofs are usually very long;second,the theorem provers are usually very complex so that it is very difficult to verify their correctness;third,the programs that a user develops while doing the proof are very often too complicated and do not have simple mapping to the sequence of inferences performed by the system.Our intention of designing such a checker is different.The fundamental reason is that taking the characteristics of Pointer Logic into account,designing a theorem prover without a proof checker will be difficult to guarantee the soundness of the system,because the implication between the premise and conclusion of the proof goal is based on the equality of the information of pointers.A proof checker will be suitable to deal with this situation.At the beginning we are clear about it,and this makes our implementation of theorem prover is not as complex as the other existing ones,we let the proof checker take the task of ensuring the soundness of the theorem prover.In our implementation,a proof goal may have a proof generated by the theorem prover,but the proof must be checked by the proof checker. To a user,the checker is an ML function which does not read a proof file directly,it takes the verification condition and its corresponding proof as inputs and reports back with either a success which means the proofs are correct or a failure which means the opposite.The checking process is done in a loop.The body of the loop is a case analysis on the values of a string type,actually,it is the name field mentioned above in the definition of type proof of Section 5.1.We evaluate the name filed of all proofs,and then attempt to match it to one of the patterns in a given order.When a successful match occurs,a corresponding expression performing deletion is evaluated.Let's take the pattern en_eq_trans_in as an example,when this pattern matches,the information in the field of fl will be deleted from the N field in the premise,the information in the field of 2 will be deleted from the N field in the conclusion.And this pattern says that after doing substitution to the N field of the conclusion by using equalities in the En field of the conclusion,the resulting N field of the conclusion is a subset of the N field of the premise. There are 55 patterns for the checker now.Each pattern handles some of the fields from f1 to f10.It may happen that the case patterns do not cover all cases,that is,there can be values that do not match any of the patterns.In that case,SML reports a warning stating that the matching is incomplete at compile-time.And at runtime,if an ⊙中国科学院软件研究所hp/ww.j0s.org.cn
2046 Journal of Software 软件学报 Vol.20, No.8, August 2009 3. Outputting the proof generated in stage 2 to a text file or the terminal. { : , 1: , 2 : , 3: ( *( )) , 4 : ( *( )) , 5 : ( * ( )) , 6 : type proof name string f lval list f lval list f id lval list list f id lval list list f id lval list list f lv = , 7 : , 8 : ( * exp* exp*exp) , 9 : ( * exp* exp*exp) , 10 : ( * exp* exp* e al list list f lval list list f lval list f lval list f lval | ************************************************************* | The proof is: | ************************************************************* | _ | 1: 2: 3: 4: 5: | 6 :{ },{ , ( ) ^ | | | | | | | xp) } | | | pai in ff ff f f x p x next list → _ 1: 2 : 3: 4 : 5 : 6 : 7 : 8 : 9 : 10 : (1)} 7 : 8 : 9 : 10 : _ 1: 2: 3: 4: 5: 6: 7: _ _ 1: ( ) ^ (2) 2 : ( ) ^ ((1) (1)) 3: 4 : 5 : 6 : 7 : 8 : 9 : 10 : _ 1: 2: 3: 4: 5: 6 : 7 : 8 : 9 : 10 : pred null ff ff f f f ff f f f f f darr null ff ff f f f en trans equal f x next f x next ffffffff di null ff ff f fffff → → + 8 : 9 : 10 : _ _ 1: 2: 3: 4: 5: 6: 7: 8 : :[1..(1) (1)].( {{ ( ) ^ ( )}}) 9 : 10 : _ 1: 2 : 3: 4 : 5 : 6 : 7 : 8 : 9 : 10 : i fff notsure compare null ff ff f f f f forall k P x next k f f env true ff ff f f f ff f − → Fig.7 Definition of type proof and proof script for (new p 2.2.1) 6 Proof Checking In Ref.[15], the authors design a proof checker for three main reasons: first, the mechanically generated formal proofs are usually very long; second, the theorem provers are usually very complex so that it is very difficult to verify their correctness; third, the programs that a user develops while doing the proof are very often too complicated and do not have simple mapping to the sequence of inferences performed by the system. Our intention of designing such a checker is different. The fundamental reason is that taking the characteristics of Pointer Logic into account, designing a theorem prover without a proof checker will be difficult to guarantee the soundness of the system, because the implication between the premise and conclusion of the proof goal is based on the equality of the information of pointers. A proof checker will be suitable to deal with this situation. At the beginning we are clear about it, and this makes our implementation of theorem prover is not as complex as the other existing ones, we let the proof checker take the task of ensuring the soundness of the theorem prover. In our implementation, a proof goal may have a proof generated by the theorem prover, but the proof must be checked by the proof checker. To a user, the checker is an ML function which does not read a proof file directly, it takes the verification condition and its corresponding proof as inputs and reports back with either a success which means the proofs are correct or a failure which means the opposite. The checking process is done in a loop. The body of the loop is a case analysis on the values of a string type, actually, it is the name field mentioned above in the definition of type proof of Section 5.1. We evaluate the name filed of all proofs, and then attempt to match it to one of the patterns in a given order. When a successful match occurs, a corresponding expression performing deletion is evaluated. Let’s take the pattern en_eq_trans_in as an example, when this pattern matches, the information in the field of f1 will be deleted from the N field in the premise, the information in the field of f2 will be deleted from the N field in the conclusion. And this pattern says that after doing substitution to the N field of the conclusion by using equalities in the Env field of the conclusion, the resulting N field of the conclusion is a subset of the N field of the premise. There are 55 patterns for the checker now. Each pattern handles some of the fields from f1 to f10. It may happen that the case patterns do not cover all cases, that is, there can be values that do not match any of the patterns. In that case, SML reports a warning stating that the matching is incomplete at compile-time. And at runtime, if an