梁红瑾等：处理指针相等关系不确定的指针逻辑 339 (TI....TTAIAADAOIP=q(Tilp...Tm-pA(TPIp-p)IANIp+p)DlpnOlp) 对于赋值前的平测试leak(SP,p). 注意到第1条规则要求赋值前leak(SP,p)为假，而第2条规则只是在赋值前测试leak(SP,p),如果Ieak(SP,p) 为真，则给出可能内存泄漏的警告信息 (2)p的别名在Ⅱ或∥的某个集合中，q的别名在D冲的情况类似 2)非指针类型的赋值语句、分配空间语句及复合、条件、循环语句的规则 仍然使用原来指针逻辑的规则 3)释放空间语句free(p) 只有p的别名在Ⅱ或l∥的某个集合中，才能使用free函数.当p的别名在Ⅱ的某个集合中时，free(p)的规则与 原先的指针逻辑的一致.若p的别名在从的某个集合中，那么所用规则虽然相同，但是因为可能存在其他∥集 合的指针与p指向同一个对象，所以必须给出可能出现悬空指针的警告信息. 4)分情况规则、结构规则和函数调用规则 仍然使用原来指针逻辑的规则例 2证明实例 2.1 Schorr-Vaite.算法 Schorr--Waite算法是一种非递归的有向图遍历算法，它从根节点开始深度优先遍历有向图的所有节点，但 仅使用图本身的指针实现回溯该算法的基本思想在于，由于遍历过程中总是有临时指针指向当前节点的前驱， 使得从前驱指向下一个节点的指针是冗余的，可以利用它指向前驱节点的前驱，直至图的根节点这种指针的翻 转链(reverse pointer chain)实现了图的回溯，相当于一个栈。 我们使用指针逻辑证明Schorr-Waite算法满足PointerC的基本安全策略，即程序运行时不出现通过NULL 指针或悬空指针来存取所指向的对象的操作，不把NULL指针或悬空指针作为fre函数调用的实在参数、不发 生内存泄漏等.本例没有证明该算法的正确性（即该算法遍历图上所有节点），因为指针逻辑对这个问题的证明 没有特别的优势. 使用该算法的C版本，与文献[10]中的做法一样.我们修改了循环条件和f条件中的布尔表达式，将布尔条 件显式化，以便正确反映到代码的前后条件上，但为了避免过多地修改程序，假定程序中的布尔表达式仍按短路 计算其节点类型定义如下： typedef struct node{ boolean m,c, struct node◆l,*r, node: 其中，I和r分别是指向左子节点和右子节点的指针（可为NULL),m是节点的遍历标志，c用于区分左、右子 节点哪个己访问过，是算法内部使用的， 使用扩展的指针逻辑描述这种二叉有向图结构： graph(p)(p)([p]ngraph(p->D)ngraph(p->r)), 其中，{pw表示空图.另一种情况p]graph(p->)Ngraph(p->r)表示非空图.注意，该定义与二叉树和二叉有向无环 图定义的区别若仅依据该定义，一个带环有向图的展开式将是无限的，但是本例用节点的标志信息m和c来识别 环，因此该定义在此是恰当的 下面以Schorr--Waite图遍历算法的安全性证明为例，展示扩展的指针逻辑在指针相等关系不确定的数据结 构中的应用.限于篇幅，只给出主要程序点的断言， graph(root) ©中国科学院软件研究所 http://www.c-s-a.org.cn梁红瑾 等:处理指针相等关系不确定的指针逻辑 339 {T 1∧…∧T m−1∧T p ∧Π ∧N q ∧D∧Q}p=q{T 1/p∧…∧T m−1/p∧(T p /p−p)∧Π ∧(N q /p+p)∧D/p∧Q/p} 对于赋值前的Ψ,测试leak(S p ,p). 注意到第 1 条规则要求赋值前leak(S p ,p)为假;而第 2 条规则只是在赋值前测试leak(S p ,p),如果leak(S p ,p) 为真,则给出可能内存泄漏的警告信息. (2) p 的别名在Π 或U 的某个集合中,q 的别名在D中的情况类似. 2) 非指针类型的赋值语句、分配空间语句及复合、条件、循环语句的规则 仍然使用原来指针逻辑的规则[5]. 3) 释放空间语句 free(p) 只有p的别名在Π 或U 的某个集合中,才能使用free函数.当p的别名在Π 的某个集合中时,free(p)的规则与 原先的指针逻辑[5]一致.若p的别名在U 的某个集合中,那么所用规则虽然相同,但是因为可能存在其他U 集 合的指针与 p 指向同一个对象,所以必须给出可能出现悬空指针的警告信息. 4) 分情况规则、结构规则和函数调用规则 仍然使用原来指针逻辑的规则[5]. 2 证明实例 2.1 Schorr-Waite算法 Schorr-Waite算法[9]是一种非递归的有向图遍历算法,它从根节点开始深度优先遍历有向图的所有节点,但 仅使用图本身的指针实现回溯.该算法的基本思想在于,由于遍历过程中总是有临时指针指向当前节点的前驱, 使得从前驱指向下一个节点的指针是冗余的,可以利用它指向前驱节点的前驱,直至图的根节点.这种指针的翻 转链(reverse pointer chain)实现了图的回溯,相当于一个栈. 我们使用指针逻辑证明 Schorr-Waite 算法满足 PointerC 的基本安全策略,即程序运行时不出现通过 NULL 指针或悬空指针来存取所指向的对象的操作,不把 NULL 指针或悬空指针作为 free 函数调用的实在参数、不发 生内存泄漏等.本例没有证明该算法的正确性(即该算法遍历图上所有节点),因为指针逻辑对这个问题的证明 没有特别的优势. 使用该算法的 C 版本,与文献[10]中的做法一样.我们修改了循环条件和 if 条件中的布尔表达式,将布尔条 件显式化,以便正确反映到代码的前后条件上,但为了避免过多地修改程序,假定程序中的布尔表达式仍按短路 计算.其节点类型定义如下: typedef struct node { boolean m, c; struct node *l, *r; } node; 其中,l 和 r 分别是指向左子节点和右子节点的指针(可为 NULL),m 是节点的遍历标志,c 用于区分左、右子 节点哪个已访问过,是算法内部使用的. 使用扩展的指针逻辑描述这种二叉有向图结构: graph(p){p}N∨([p]∧graph(p->l)∧graph(p->r)), 其中,{p}N表示空图.另一种情况[p]∧graph(p->l)∧graph(p->r)表示非空图.注意,该定义与二叉树和二叉有向无环 图定义的区别.若仅依据该定义,一个带环有向图的展开式将是无限的,但是本例用节点的标志信息m和c来识别 环,因此该定义在此是恰当的. 下面以 Schorr-Waite 图遍历算法的安全性证明为例,展示扩展的指针逻辑在指针相等关系不确定的数据结 构中的应用.限于篇幅,只给出主要程序点的断言. {graph(root)}