342 Journal of Software软件学报Vol.2l,No.2,February2010 Bornat引入了“spatial-separation assertions'”表达对象或节点间的分离关系.我们扩展的指针逻辑虽然称作处理 指针相等关系不确定的结构，但这种不确定性是有限制的，至少在同一个访问路径集合内的指针都是确定相等 的；并且，当对象的指针信息完整时，我们的指针逻辑可以精确地描述它，而不会产生二义性 分离逻辑也可以描述有向图等结构共享不明确的数据结构.由于分离逻辑强调分离堆之间互无影响的特 点，所以在描述有向无环图时，分离逻辑可以清晰地表达无环的特征但分离逻辑不提供描述分离堆之间联系的 机制，而有向图中的别名关系错综复杂，使得难以用分离逻辑表达访问路径间的相等关系，即结构的共享关系 文献[14]中使用一种部分图(partial graph,即其允许出现不指明后继的节点)收集有向图的结构共享信息，仅明确 标记并展开共享结构的第一次出现，其他出现则标记为第一次出现的引用而不再具体展开.这种做法利用部分 图的概念克服了分离逻辑在表达共享关系上的困难，但是却需要太多的关于环境(environment)的信息.即便是 证明很简单的例子，如copy DAGs,,也需要很大的工作量1 在证明程序的安全性方面，由于指针逻辑将程序的安全性描述为定型规则的副条件，所以对程序的安全性 验证及不安全因素的检测都是内在的.例如，用指针逻辑证明Schorr-Waite:算法的安全性时非常简洁，没有明显 的表述安全性的断言.Yang在使用分离逻辑证明Schorr-.Waite算法的正确性时ls1需要引入noDangling(x)来描述 x不是悬空指针的特性.在使用原型工具CADUCEUS证明Schorr-Waite算法的正确性时Io引入了valid(x)表达类 似的含义 另外，无论是Bornat对Hoare逻辑的扩展还是分离逻辑，目前都只用于一些比较简单的例子，如Schorr-Waite 算法、CopyDags函数等，而没有用于如第2.2节所述的较为复杂的实际程序.虽然该例是手工证明的，但我们将 进一步开发plcc,以支持较为复杂程序的自动验证， 4结束语 本文扩展了为PointerC语言设计的可对指针程序进行精确分析的指针逻辑，使其可以描述图等指针相等 与否不确定的数据结构，以支持这种数据结构上的指针程序的性质证明扩展的处理指针相等关系不确定的指 针逻辑的推理规则都是应实际需求而提出的因此可能并不完善 到目前为止，除了需要工具支持以外，使用指针逻辑进行程序验证的另一个局限是需要程序员提供程序的 前、后断言和循环不变式，这些都限制了本文方法的应用.为了尽量减轻程序员的负担，我们将尝试仅让程序员 声明指针变量指向数据结构的种类（单链表、二叉树等）并提供函数的前、后断言，然后自动推导函数代码中的 循环不变式 References: [1]Reynolds JC.Separation logic:A logic for shared mutable data structures.In:Proc.of the 17th Annual IEEE Symp.on Logic in Computer Science.Copenhagen:IEEE Computer Society Press,2002.55-74. [2]Hua BJ,Chen YY,Ge L,Wang ZF.The PointerC programming language specification.Technical Report.http://kyhcs.ustcsz.edu. cn/old/lss/doc/ [3]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). [4]Chen YY,Ge L,Hua BJ,Li ZP,Liu C,Wang ZF.A pointer logic and certifying compiler.Frontiers of Computer Science in China, 2007,1(3:297-312. [5]Chen YY,Li ZP,Wang ZF,Hua BJ.A pointer logic for verification of pointer programs.Technical Report,2010. http://kyhcs.ustcsz.edu.cn/Iss [6]Wang ZF,Chen YY,Wang ZM,Wang W,Tian B.An extension to pointer logic for verification.In:Proc.of the 2nd IEEE/IFIP Int'l Symp.on Theoretical Aspects of Software Engineering.Nanjing:IEEE Computer Society Press,2008.49-56. [7]Hua BJ,Chen YY,Li ZP,Wang ZF,Ge L.Design and proof of a safe programming language PointerC.Chinese Journal of Computers,2008,31(4):556-564 (in Chinese with English abstract). ©中国科学院软件研究所htp:/www.c-s-a.org.cn342 Journal of Software 软件学报 Vol.21, No.2, February 2010 Bornat 引入了“spatial-separation assertions”表达对象或节点间的分离关系.我们扩展的指针逻辑虽然称作处理 指针相等关系不确定的结构,但这种不确定性是有限制的,至少在同一个访问路径集合内的指针都是确定相等 的;并且,当对象的指针信息完整时,我们的指针逻辑可以精确地描述它,而不会产生二义性. 分离逻辑也可以描述有向图等结构共享不明确的数据结构.由于分离逻辑强调分离堆之间互无影响的特 点,所以在描述有向无环图时,分离逻辑可以清晰地表达无环的特征.但分离逻辑不提供描述分离堆之间联系的 机制,而有向图中的别名关系错综复杂,使得难以用分离逻辑表达访问路径间的相等关系,即结构的共享关系. 文献[14]中使用一种部分图(partial graph,即其允许出现不指明后继的节点)收集有向图的结构共享信息,仅明确 标记并展开共享结构的第一次出现,其他出现则标记为第一次出现的引用而不再具体展开.这种做法利用部分 图的概念克服了分离逻辑在表达共享关系上的困难,但是却需要太多的关于环境(environment)的信息.即便是 证明很简单的例子,如copy DAGs,也需要很大的工作量[14]. 在证明程序的安全性方面,由于指针逻辑将程序的安全性描述为定型规则的副条件,所以对程序的安全性 验证及不安全因素的检测都是内在的.例如,用指针逻辑证明Schorr-Waite算法的安全性时非常简洁,没有明显 的表述安全性的断言.Yang在使用分离逻辑证明Schorr-Waite算法的正确性时[15]需要引入noDangling(x)来描述 x不是悬空指针的特性.在使用原型工具CADUCEUS证明Schorr-Waite算法的正确性时[10]引入了valid(x)表达类 似的含义. 另外,无论是 Bornat 对 Hoare 逻辑的扩展还是分离逻辑,目前都只用于一些比较简单的例子,如 Schorr-Waite 算法、CopyDags 函数等,而没有用于如第 2.2 节所述的较为复杂的实际程序.虽然该例是手工证明的,但我们将 进一步开发 plcc,以支持较为复杂程序的自动验证. 4 结束语 本文扩展了为 PointerC 语言设计的可对指针程序进行精确分析的指针逻辑,使其可以描述图等指针相等 与否不确定的数据结构,以支持这种数据结构上的指针程序的性质证明.扩展的处理指针相等关系不确定的指 针逻辑的推理规则都是应实际需求而提出的,因此可能并不完善. 到目前为止,除了需要工具支持以外,使用指针逻辑进行程序验证的另一个局限是需要程序员提供程序的 前、后断言和循环不变式,这些都限制了本文方法的应用.为了尽量减轻程序员的负担,我们将尝试仅让程序员 声明指针变量指向数据结构的种类(单链表、二叉树等)并提供函数的前、后断言,然后自动推导函数代码中的 循环不变式. References: [1] Reynolds JC. Separation logic: A logic for shared mutable data structures. In: Proc. of the 17th Annual IEEE Symp. on Logic in Computer Science. Copenhagen: IEEE Computer Society Press, 2002. 55−74. [2] Hua BJ, Chen YY, Ge L, Wang ZF. The PointerC programming language specification. Technical Report. http://kyhcs.ustcsz.edu. cn/old/lss/doc/ [3] 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). [4] Chen YY, Ge L, Hua BJ, Li ZP, Liu C, Wang ZF. A pointer logic and certifying compiler. Frontiers of Computer Science in China, 2007,1(3):297−312. [5] Chen YY, Li ZP, Wang ZF, Hua BJ. A pointer logic for verification of pointer programs. Technical Report, 2010. http://kyhcs.ustcsz.edu.cn/lss [6] Wang ZF, Chen YY, Wang ZM, Wang W, Tian B. An extension to pointer logic for verification. In: Proc. of the 2nd IEEE/IFIP Int’l Symp. on Theoretical Aspects of Software Engineering. Nanjing: IEEE Computer Society Press, 2008. 49−56. [7] Hua BJ, Chen YY, Li ZP, Wang ZF, Ge L. Design and proof of a safe programming language PointerC. Chinese Journal of Computers, 2008,31(4):556−564 (in Chinese with English abstract)