随着国家、社会和日常生活对软件系统的依赖程度日益增长，安全攸关软件的高可信成为保障国家安全、保持经济可持续发展和维护社会稳定的必要条件。
　形式验证是提高软件可信程度的重要方法。粗略地说，软件的形式验证有两种途径，第一种是模型检测，它通过遍历系统所有状态空间，能够对有穷状态系统进行自动验证，并自动构造不满足验证性质的反例。这种方法在工业界较流行。第二种是逻辑推理，它利用某种程序逻辑进行演算，对程序性质进行严格的推理，产生验证条件，再利用定理证明器进行证明。本文所讨论的方法是基于逻辑推理的方式。
　对于指针程序的推理，关键在于别名的判断和处理。通常所采用的Hoare逻辑的一个重要限制是程序中不同的名字代表不同的程序对象，即不允许出现别名。
　对于指针别名判断的一种解决办法是采用分离逻辑。使用分离逻辑的一个问题是，通常的自动定理证明器都不能证明带分离合取连接词（*，Separating Conjunction）的验证条件，必须为分离逻辑设计专用的自动定理证明工具。
　本文提出一种利用形状图信息来消除访问路径别名，使得指针程序仍然可以用Hoare逻辑来进行验证的方法。
1 PointerC语言和形状图逻辑
1.1 PointerC语言
　PointerC是一个强调指针类型并增加形状声明的类C小语言，详细的语法信息请见参考文献[1]。在结构体声明中，通过指针域指向形状的声明来确定这种结构体用来构造什么形状的数据结构，同时也限定了该结构体类型的指针所能指向的形状。这是对应形状分析的需求所做的语言扩展，所允许的形状有单链表、循环单链表、双向链表、循环双向链表。
1.2 形状图和形状逻辑
　程序验证之前，首先基于形状图逻辑对程序进行形状分析，形状分析为每个程序点构建形状图，这些形状图构成程序验证所需要的指针信息。在此通过举例来介绍形状图[1]。
　以图1（参考文献[1]中有序链表节点插入函数循环不变式的形状图）为例说明形状图和程序点指针等信息的联系。在图1中，圆节点表示指针类型的声明变量；虚边框的矩形节点不代表任何程序元素；矩形节点表示由malLOC生成的结构体变量；灰色矩形节点是浓缩节点，表示若干个（可以是0个）相邻的、属于同一数据结构的、同类型的结构体变量，下侧可以有无代表被浓缩节点个数的整型表达式以及约束该表达式的断言。若没有，则表示被浓缩节点个数是某个自然数，但和任何变量或常数联系不起来。由图1可知，head == ptr1，ptr == ptr1->next，head指向链表的长度是m，ptr指向浓缩节点代表m-1个节点，可用head(->next)m-1上角标的方式来表示。

    可见，形状图可以作为程序断言，它是该图所能表达的指针相等、不相等和别名断言等的合取，包括其中谓词节点和浓缩节点下侧有关表长或被浓缩节点个数的整型数据断言。
　　形状图逻辑就是基于上面观点来设计的Hoare逻辑的一种扩展。程序规范的形式是{G∧Q}S{G′∧Q′}，其中G是形状图，Q是表达程序其他性质的符号断言，两部分的合取G∧Q作为程序点完整的断言。本文程序验证器的第一步工作，在无需程序员提供有关形状的函数前后条件和循环不变式的情况下，利用形状图逻辑对程序进行形状分析。由于从一个语句前的G推导该语句后的G′不受Q的影响，因此形状分析时，把程序规范简化为{G}S{G′}，以此来使用形状图逻辑的推理规则，建立各程序点的形状图G。在形状分析的过程中，还利用循环不变式推断算法得出各循环的循环不变形状图[2]。
　在完成形状分析后，程序验证器进行程序其他性质Q的验证。在{G∧Q}S{G′∧Q′}中，若S不是指针操作语句，则G′和G一样，但Q′可能不同于Q。若S是指针操作语句（指针赋值、分配空间和释放空间等），则除了G′和G可能不同外，Q′和Q可能也有一些细微的区别。下面是本文关注的部分。
2 指针程序的验证方法
　程序点数据结构构成的形状有多种可能时，则G表示为G1∨G2∨…∨Gn。同样，Q也可能是Q1∨Q2∨…∨Qm的析取形式。完整的断言可以整理成析取范式（Disjunctive Normal Form）G1∧Q1∨G2∧Q2∨…∨Gk∧Qk的形式。根据形状图逻辑，可以用析取范式的一种情况为例来讨论，写成G∧Q，G和Q分别都是合取形式。   
   程序验证器基于形状图逻辑[2]进行最强后条件演算并产生验证条件，验证条件由证明器Z3[3]自动证明。
2.1 形状图和符号断言之间的联系
　符号断言Q中允许出现指针是否等于NULL或两个指针是否相等的断言。即使函数前后条件和循环不变式中没有这样的断言，它们也会因为出现在条件语句或循环语句的布尔表达式中，而在最强后条件演算过程中被加到Q中。
　Q中指针等于NULL或两个指针相等的断言会因为和G中的信息重复而被吸收，或因有矛盾而使得G∧Q为假。
　Q中访问路径的合法性依赖于G。例如，在Q中若出现非指针型的访问路径p -> … -> data，则忽略->data所剩下的前缀应该是G上到达某个结构节点的一条访问路径，若是到达悬空节点、null节点或不存在这样的路径则都非法的，若是到达谓词节点则视谓词节点展开后的情况决定。
　Q中的访问路径之间是否有别名，Q中的访问路径和下一条语句S中的访问路径之间,以及S中的访问路径之间是否有别名都依赖于G，即利用G可以判断。
　在指针操作语句中，在对指针u赋值时可能会影响符号断言：符号断言中若有以u或u为前缀的访问路径，则要用和u相等但不是别名的u′来代换u。另一个影响符号断言的场合是，在free语句之后应该删除涉及被释放节点上数据的原子断言。
　G中也会有符号断言，附加在浓缩节点上，用来限制它代表结构节点的个数。G的符号断言和Q的符号断言不会有矛盾，但前者有时会给出更准确的信息。

[1] [2]  下一页