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&&i<n&&j=0 (e2.1.3) As the above,the goal we are going to prove will be the form of the following: Goal兰{Quant,L,N1,D,Pred,Dar,No1sre,Em}→ (e2.1.4) Quant,,1,N,,D.,Pred,,Darr,,Notsure,,Env, And Quant兰exists n:it or [pu P2,.PulPm P2P. Nor [Pu>P2>..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