2.2 程序推理规则的扩展
　在使用推理规则从语句S的前条件G∧Q产生后条件G′∧Q′时，要保证Q合法、Q和G无重复与矛盾。
　先考虑S是指针操作语句。修改指针型数据的简单语句会引起指针值的变化，或者是存储堆块的增减，因而导致形状图的变化。根据2.1节的介绍知道，对Q的影响是访问路径的替换或者删除部分断言。先假定Q和S无别名，有别名的情况在考虑非指针操作语句时介绍。下面给出各种语句规则。
　(1)指针型赋值语句u=v
　若u既不是null指针也不是悬空指针，则按下面规则得到后断言。
　{G∧Q} u = v {G′∧Q[u′/u]}
其中G′是由形状分析得到的形状图，Q[u′/u]表示Q中作为访问路径（包括作为前缀情况）的u和其相等且不互为别名的访问路径u′代换。
　(2)对指针赋值的其他语句
　分配空间语句u=malLOC(t)和函数调用语句ret=f(act)有关Q的处理同上面赋值语句的规则一样。
　(3)释放空间语句free(u)
　释放u指向的节点后，Q中含u或u的别名的原子断言不应再存在，因此规则如下：
    {G∧Q} free(u) {G′∧Q′}
其中Q′由把Q中含u或u的别名的原子断言都删除而得到。
　很容易明白，若Q无别名，则这些语句的规则不会导致Q′出现别名，因为它们对Q做的小修改都不会引入别名。
　再考虑非指针操作语句。只要前断言Q和语句S中无别名，则使用Hoare的赋值公理就是可靠的。若有别名，则可以先用G的信息来消除别名（把互为别名的访问路径改成都用其中同一条访问路径），然后再用赋值公理。定义eliminate_aliases函数为(S′,Q′)=eliminate_aliases(G, S, Q),它根据G消除S和Q中的别名，得到S′和Q′。
　把Hoare逻辑的赋值公理限定为无别名时才能使用，并增加下面的消除别名推理规则，就可以对含访问路径别名的程序进行推理。
    对于修改指针型数据的语句，其前断言Q可能是程序员提供的，例如不排除循环不变式中 Q存在别名，因此有时也需要这条规则。
　复合、条件和循环语句的规则以及推论规则的形式和Hoare逻辑相应规则的形式一致。
 
3 系统原型
　基于形状图逻辑，实现了PointerC语言的一个程序验证器[1]，它能够验证使用图1所定义的各种形状的程序。除了验证形状外，还能验证节点上数据的一些性质。本文对有序链表插入节点的函数进行了验证。
　该验证器分成下面几个模块，按所列次序顺序执行：
　(1)普通编译器的前端。对源程序进行词法分析、语法分析和静态语义检查后，生成抽象语法树。
　(2)形状分析。遍历抽象语法树，根据形状声明和形状图逻辑来生成各程序点的形状图。
　(3)验证条件的生成。遍历抽象语法树，根据程序员提供的函数前后条件和循环不变式，按最强后条件演算方式为各函数生成验证条件。
　(4)验证条件的证明。将生成的各验证条件G∧Q?圯Q′，按照上一节所介绍的方法翻译成P∧Q?圯Q′的形式，逐个交给证明器进行证明。
    本文提出一种利用形状图信息来消除访问路径别名，使得指针程序仍然可以用Hoare逻辑来进行验证的方法，并利用可自动定理证明器的支持，开发了一个PointerC语言的程序验证器原型，展示了该方法的可行性。
参考文献
[1] ZHANG Y, LI Z P, CHEN Y Y, et al. Shape graph logIC and A shape system (Extended Verison).URL:http://ssg.ustcsz.edu.cn/content/shape-graph-logic.2010(11).
[2] NECULA G. Proof-carrying code,In Proc.24th ACM Symp.On Principles of Prog.Lang. New York, 1997(1):106-119.
[3] MOURA L D, BJORNER N. Z3: An Efficient SMT solver, conference on tools and algorithms for the construction and analysis of SystEMS(TACAS). Budapest, Hungary, volume 4963 of LNCS, 2008:337-340.

上一页  [1] [2]