陈意云等：一种用于指针程序验证的指针逻辑 425 list(p)p(iplist(p->next))tree(p)p)v(ip)ntree(p->I)tree(p->r)). 高级类型系统也被用在检查指针程序的安全性上.例如，Smith,Walker和Morrisett提出别名类型24，其新类 型系统的主要特征是一组别名约束别名约束描述了存储的形状，函数使用这些约束来规范它期望的存储形状， 如果当前的存储不符合所给出的约束，那么类型系统保证函数不会被调用别名类型非常类似于分离逻辑中包 含空公式、指向谓词和分离合取的片段，并且也是为低级语言程序设计的.DeLine和Fahndrich设计了一种编程 语言Vult,它带别名类型的一种变异2.Vault提供了一种叫做类型看守的新特征，程序员可以用它来规范领域 专用的资源管理协议，Vault的类型检查器通过穷尽搜索，报告任何对协议的违例.Vault已经用在设备驱动器的 内存管理和软件协议的推理上.程序逻辑和类型系统的主要区别是：类型系统，尤其是Vut,能够较好地支持自 动推理，而程序逻辑允许连接词的多样性和复杂的约束，因此有很强的表达能力 6结束语 本文改进了一种可对指针程序进行精确分析的逻辑系统，它可用来证明指针程序是否满足PointerC语言 定型规则的副条件，以支持指针程序的安全性证明及其他性质的证明.指针逻辑目前还只能描述单链表、双链 表和二叉树等指针相等与否有规律的数据结构，尚不能恰当描述无环有向图等指针相等与否出现部分不确定 的数据结构.我们正在扩展指针逻辑以适应这样的需求.另外，有限制地允许指针算术运算，以适应编程中经常 使用的calloc存储分配的方案也正在实施中. References: [1]Necula GC.Proof-Carrying code.In:Proc.of the 24th ACM Symp.on Principles of Programming Languages.1997.106-119. http://portal.acm.org/citation.cfm?id=263712 2]Morrisett G,Walker D,Crary K,Glew N.From system F to typed assembly language.In:Proc.of the 25th ACM Sigplan-Sigact Symp.on Principles of Programming Languages.1998.85-97.http://portal.acm.org/citation.cfm?id=319345 [3]Mandelbaum Y,Walker D,Harper R.An effective theory of type refinements.In:Proc.of the 8th Int'l Conf.on Functional Programming.2003.213-225.http://portal.acm.org/citation.cfm?id=944746.944725 [4]Appel AW.Foundational proof-carrying code.In:Proc.of the 16th Annual IEEE Symp.on Logic in Computer Science.2001. 247-258.http://portal.acm.org/citation.cfm?id=871860&dl=ACM&coll=ACM&CFID=67109554&CFTOKEN=53036453 (5]Yu DC,Hamid NA,Shao Z.Building certified libraries for PCC:Dynamic storage allocation.Science of Computer Programming, 2004,50(1-3:101-127. [6]Feng XY,Shao Z,Vaynberg A,Xiang S,Ni ZZ.Modular verification of assembly code with stack-based control abstractions.In: Proc.of the 2006 ACM SIGPLAN Conf.on Programming Language Design and Implementation.2006.401-414. http://portal.acm.org/citation.cfm?id=1133255.1134028 7]Xi HW.Applied type system:extended abstract.In:The Post-Workshop Proc.of the TYPES 2003.LNCS 3085,Springer-Verlag. 2004.394-408.http://www.springerlink.com/content/pc3xfhle3fdu4ecn/ [8]Necula GC,Lee P.The design and implementation of a certifying compiler.In:Proc.of the 1998 ACM Sigplan Conf.on Programming Language Design and Implementation.1998.333-344.http://portal.acm.org/citation.cfm?id=277752 [9]Colby C.Lee P,Necula GC,Blau F,Plesko M,Cline K.A certifying compiler for Java.In:Proc.of the 2000 ACM SIGPLAN Conf. on Programming Language Design and Implementation.2000.95-107.http://portal.acm.org/citation.cfm?id=349315 [10]Hua BJ,Chen YY,Ge L,Wang ZF.The PointerC programming language specification.Technical Report,http://ssg.ustcsz.edu.cn/ Iss/doc/index.html [11]Chen YY,Hua BJ,Ge L,Wang ZF.A pointer logic for safety verification of pointer programs.Chinese Journal of Computers, 2008,31(3):372-380 (in Chinese with English abstract). [12]Chen YY,Ge L,Hua BJ,Li ZP,Cheng L,Wang ZF.A pointer logic and certifying compiler.Frontiers of Computer Science in China,2007,1(3:297-312. [13]Hua BJ,Chen YY,Li ZP,Wang ZF,Ge L.Design and proof of a safe programming language.Chinese Journal of Computers,2008, 31(4):556-564 (in Chinese with English abstract). ©中国科学院软件研究所htp:wwv.c-s-a.org.cn陈意云 等:一种用于指针程序验证的指针逻辑 425 是 list(p){p}N∨({p}∧list(p->next))和 tree(p){p}N∨({p}∧tree(p->l)∧tree(p->r)). 高级类型系统也被用在检查指针程序的安全性上.例如,Smith,Walker 和 Morrisett 提出别名类型[24],其新类 型系统的主要特征是一组别名约束.别名约束描述了存储的形状,函数使用这些约束来规范它期望的存储形状. 如果当前的存储不符合所给出的约束,那么类型系统保证函数不会被调用.别名类型非常类似于分离逻辑中包 含空公式、指向谓词和分离合取的片段,并且也是为低级语言程序设计的.DeLine 和 Fähndrich 设计了一种编程 语言 Vault,它带别名类型的一种变异[25].Vault 提供了一种叫做类型看守的新特征,程序员可以用它来规范领域 专用的资源管理协议;Vault 的类型检查器通过穷尽搜索,报告任何对协议的违例.Vault 已经用在设备驱动器的 内存管理和软件协议的推理上.程序逻辑和类型系统的主要区别是:类型系统,尤其是 Vault,能够较好地支持自 动推理,而程序逻辑允许连接词的多样性和复杂的约束,因此有很强的表达能力. 6 结束语 本文改进了一种可对指针程序进行精确分析的逻辑系统,它可用来证明指针程序是否满足 PointerC 语言 定型规则的副条件,以支持指针程序的安全性证明及其他性质的证明.指针逻辑目前还只能描述单链表、双链 表和二叉树等指针相等与否有规律的数据结构,尚不能恰当描述无环有向图等指针相等与否出现部分不确定 的数据结构.我们正在扩展指针逻辑以适应这样的需求.另外,有限制地允许指针算术运算,以适应编程中经常 使用的 calloc 存储分配的方案也正在实施中. References: [1] Necula GC. Proof-Carrying code. In: Proc. of the 24th ACM Symp. on Principles of Programming Languages. 1997. 106−119. http://portal.acm.org/citation.cfm?id=263712 [2] Morrisett G, Walker D, Crary K, Glew N. From system F to typed assembly language. In: Proc. of the 25th ACM Sigplan-Sigact Symp. on Principles of Programming Languages. 1998. 85−97. http://portal.acm.org/citation.cfm?id=319345 [3] Mandelbaum Y, Walker D, Harper R. An effective theory of type refinements. In: Proc. of the 8th Int’l Conf. on Functional Programming. 2003. 213−225. http://portal.acm.org/citation.cfm?id=944746.944725 [4] Appel AW. Foundational proof-carrying code. In: Proc. of the 16th Annual IEEE Symp. on Logic in Computer Science. 2001. 247−258. http://portal.acm.org/citation.cfm?id=871860&dl=ACM&coll=ACM&CFID=67109554&CFTOKEN=53036453 [5] Yu DC, Hamid NA, Shao Z. Building certified libraries for PCC: Dynamic storage allocation. Science of Computer Programming, 2004,50(1-3):101−127. [6] Feng XY, Shao Z, Vaynberg A, Xiang S, Ni ZZ. Modular verification of assembly code with stack-based control abstractions. In: Proc. of the 2006 ACM SIGPLAN Conf. on Programming Language Design and Implementation. 2006. 401−414. http://portal.acm.org/citation.cfm?id=1133255.1134028 [7] Xi HW. Applied type system: extended abstract. In: The Post-Workshop Proc. of the TYPES 2003. LNCS 3085, Springer-Verlag, 2004. 394−408. http://www.springerlink.com/content/pc3xfh1e3fdu4ecn/ [8] Necula GC, Lee P. The design and implementation of a certifying compiler. In: Proc. of the 1998 ACM Sigplan Conf. on Programming Language Design and Implementation. 1998. 333−344. http://portal.acm.org/citation.cfm?id=277752 [9] Colby C, Lee P, Necula GC, Blau F, Plesko M, Cline K. A certifying compiler for Java. In: Proc. of the 2000 ACM SIGPLAN Conf. on Programming Language Design and Implementation. 2000. 95−107. http://portal.acm.org/citation.cfm?id= 349315 [10] Hua BJ, Chen YY, Ge L, Wang ZF. The PointerC programming language specification. Technical Report, http://ssg.ustcsz.edu.cn/ lss/doc/index.html [11] Chen YY, Hua BJ, Ge L, Wang ZF. A pointer logic for safety verification of pointer programs. Chinese Journal of Computers, 2008,31(3):372−380 (in Chinese with English abstract). [12] Chen YY, Ge L, Hua BJ, Li ZP, Cheng L, Wang ZF. A pointer logic and certifying compiler. Frontiers of Computer Science in China, 2007,1(3):297−312. [13] Hua BJ, Chen YY, Li ZP, Wang ZF, Ge L. Design and proof of a safe programming language. Chinese Journal of Computers, 2008, 31(4):556−564 (in Chinese with English abstract)