424 Journal of Software软件学报Vol.21,No.3,March2010 名，因而可以克服别名给Hoare逻辑带来的困难.我们扩展Hoare逻辑的出发点是，不同的访问路径被认为是代 表不同的指针，除非能够证明它们互为别名指针逻辑的推理规则用来从语句前那个程序点的指针信息来推导 该语句后那个程序点的指针信息」 分离逻辑不像指针逻辑那样能够防止内存泄漏，它的推理规则不能排除会引起内存泄漏的语句通常，内存 泄漏是指存在不能被程序访问的并且尚未释放的堆块.例如，下面程序段的前后断言可以用分离逻辑验证1，但 是，由于对赋值x:=il采用通常的Hoare逻辑赋值公理，该段程序引起的内存泄漏未被发现 {emp}x=cons(10),{x→l0}x=nil{3x.→10}. 为了解决这个问题，Reynolds等人提出了精确断言(precise assertion)概念l1,但它的定义基于抽象机器，而 不是基于断言的语法特征。 指针逻辑的最大问题是，其推理规则需要使用一些比语法代换复杂得多的基本运算，使得它难以用于手工 验证.若对PointerC语言和断言语言val的语法添加下面两点限制，本质上得到分离逻辑的另一种表示形式.有 了这两点限制，指针逻辑的别名计算被大大简化： (I)PointerC的val限制为hval:=idid->id,并且赋值语句的左右两边不同时出现id->id的形式： (2)断言语言的val不使用val(->idp的形式 指针逻辑的这种形式区别于分离逻辑之处在于： (1)存在一些高级语言特征：类型化、按域名访问而不是按偏移访问等： (2)断言中采用访问路径集合，而不需要分离合取连接词等. 与分离逻辑比，其优点是： (1)新言演算的规则比分离逻辑的简单清晰； (2)能够验证程序是否会出现内存泄漏， 5相关工作 指针逻辑本质上是一种精确指针分析的方法，其不同于一般指针分析方法的显著优点是，它用访问路径集 合来表示程序点的指针信息，用Hoa爬风格的推理规则来表示语句引起的指针信息变化.这样，它可用于高级语 言程序的Hoare风格程序验证中， 采用访问路径集合方式来表示指针信息源于Jonkers用无存储语义(storeless semantics)来抽象内存地 址)在无存储语义中，每个动态分配的对象由一组能够到达它的访问路径来表示，整个堆的无存储表示就由所 有访问路径集合的一个划分来表示在无存储表示中，互为别名的访问路径出现在同一个集合中近年来，使用 无存储语义的研究820仍然采用这种冗余的表示方式.而我们只在访问路径集合中保留互为别名路径中的一 条路径，通过推导得到其他访问路径（若需要的话），并且，我们的方法能够较好地表示出像双向循环链表这样带 环的数据结构 在证明程序性质方面，Bornat也使用Hoare风格来推导指针程序的性质2，把堆看成由指针索引的一群对 象，并把每个对象看成由域名索引的一组成员，这样，堆上对象成员的引用对应到两次索引他基于域名相同与 否引入了对象成员代换公理，由此扩展了Hoar逻辑的赋值公理，用于证明指针程序的性质在用高阶逻辑系统 Isabelle/HOL2证明指针程序性质时，Mehta和Nipkow采用类似的办法.Marche等人在他们的原型工具 Caduceus2]中也是这样Bornat的方法和我们的方法都可以看成使用两次索引来解决别名，但方式上有较大区 别.Bornat所引入的公理和推理规则比较简洁，它们用于逆向的最弱前条件演算中.我们的公理和推理规则不如 Bornat的那么简洁，但是它们以正向方式收集更多的指针信息.与Bornat的方法相比，我们的方法有下列优势： (I)PointerC提供显式的释放堆空间函数fee,指针逻辑用来发现潜在的内存泄漏，但是Bornat的方式只 能用在依赖垃圾收集器进行堆管理的场合， (2)我们可以管理带环的数据结构，但Bornat假定数据结构无环； (3)在我们的方式中，数据结构的归纳定义比Bornat的方式简单得多，例如，单链表和二叉树的定义分别 ©中国科学院软件研究所htp:wwv.c-s-a.org.cn424 Journal of Software 软件学报 Vol.21, No.3, March 2010 名,因而可以克服别名给 Hoare 逻辑带来的困难.我们扩展 Hoare 逻辑的出发点是,不同的访问路径被认为是代 表不同的指针,除非能够证明它们互为别名.指针逻辑的推理规则用来从语句前那个程序点的指针信息来推导 该语句后那个程序点的指针信息. 分离逻辑不像指针逻辑那样能够防止内存泄漏,它的推理规则不能排除会引起内存泄漏的语句.通常,内存 泄漏是指存在不能被程序访问的并且尚未释放的堆块.例如,下面程序段的前后断言可以用分离逻辑验证[16],但 是,由于对赋值 x:=nil 采用通常的 Hoare 逻辑赋值公理,该段程序引起的内存泄漏未被发现. {emp} x:=cons(10); {x610} x:=nil {∃x.x610}. 为了解决这个问题,Reynolds 等人提出了精确断言(precise assertion)概念[16],但它的定义基于抽象机器,而 不是基于断言的语法特征. 指针逻辑的最大问题是,其推理规则需要使用一些比语法代换复杂得多的基本运算,使得它难以用于手工 验证.若对 PointerC 语言和断言语言 lval 的语法添加下面两点限制,本质上得到分离逻辑的另一种表示形式.有 了这两点限制,指针逻辑的别名计算被大大简化: (1) PointerC 的 lval 限制为 lval::=id|id->id,并且赋值语句的左右两边不同时出现 id->id 的形式; (2) 断言语言的 lval 不使用 lval(->id) exp 的形式. 指针逻辑的这种形式区别于分离逻辑之处在于: (1) 存在一些高级语言特征:类型化、按域名访问而不是按偏移访问等; (2) 断言中采用访问路径集合,而不需要分离合取连接词等. 与分离逻辑比,其优点是: (1) 断言演算的规则比分离逻辑的简单清晰; (2) 能够验证程序是否会出现内存泄漏. 5 相关工作 指针逻辑本质上是一种精确指针分析的方法,其不同于一般指针分析方法的显著优点是,它用访问路径集 合来表示程序点的指针信息,用 Hoare 风格的推理规则来表示语句引起的指针信息变化.这样,它可用于高级语 言程序的 Hoare 风格程序验证中. 采用访问路径集合方式来表示指针信息源于 Jonkers 用无存储语义(storeless semantics)来抽象内存地 址[17].在无存储语义中,每个动态分配的对象由一组能够到达它的访问路径来表示,整个堆的无存储表示就由所 有访问路径集合的一个划分来表示.在无存储表示中,互为别名的访问路径出现在同一个集合中.近年来,使用 无存储语义的研究[18−20]仍然采用这种冗余的表示方式.而我们只在访问路径集合中保留互为别名路径中的一 条路径,通过推导得到其他访问路径(若需要的话).并且,我们的方法能够较好地表示出像双向循环链表这样带 环的数据结构. 在证明程序性质方面,Bornat 也使用 Hoare 风格来推导指针程序的性质[21],把堆看成由指针索引的一群对 象,并把每个对象看成由域名索引的一组成员,这样,堆上对象成员的引用对应到两次索引.他基于域名相同与 否引入了对象成员代换公理,由此扩展了 Hoare 逻辑的赋值公理,用于证明指针程序的性质.在用高阶逻辑系统 Isabelle/HOL[22]证明指针程序性质时,Mehta 和 Nipkow 采用类似的办法.Marché 等人在他们的原型工具 Caduceus[23]中也是这样.Bornat 的方法和我们的方法都可以看成使用两次索引来解决别名,但方式上有较大区 别.Bornat 所引入的公理和推理规则比较简洁,它们用于逆向的最弱前条件演算中.我们的公理和推理规则不如 Bornat 的那么简洁,但是它们以正向方式收集更多的指针信息.与 Bornat 的方法相比,我们的方法有下列优势: (1) PointerC 提供显式的释放堆空间函数 free,指针逻辑用来发现潜在的内存泄漏,但是 Bornat 的方式只 能用在依赖垃圾收集器进行堆管理的场合; (2) 我们可以管理带环的数据结构,但 Bornat 假定数据结构无环; (3) 在我们的方式中,数据结构的归纳定义比 Bornat 的方式简单得多,例如,单链表和二叉树的定义分别