深圳pcb抄板介绍验证指针程序的方法

    形式验证是提高软件可信程度的重要方法。粗略地说，软件的形式验证有两种途径，第一种是模型检测，它通过遍历系统所有状态空间，能够对有穷状态系统进行自动验证，并自动构造不满足验证性质的反例。这种方法在工业界较流行。第二种是逻辑推理，它利用某种程序逻辑进行演算，对程序性质进行严格的推理，产生验证条件，再利用定理证明器进行证明。本文所讨论的方法是基于逻辑推理的方式。

    对于指针程序的推理，关键在于别名的判断和处理。通常所采用的Hoare逻辑的一个重要限制是程序中不同的名字代表不同的程序对象，即不允许出现别名。

    对于指针别名判断的一种解决办法是采用分离逻辑。使用分离逻辑的一个问题是，pcb抄板通常的自动定理证明器都不能证明带分离合取连接词（*，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]。