12期 张昱等：形状图理论的定理证明 2469 价重写系统化简形状图后，适当地使用形状图的蕴 使用的双向链表倒置算法。 涵规则.所使用的蕴涵规则是2.2节中第(1)类蕴涵 对于这类循环，在循环体的每条执行路径上，声 规则，即由W台W,VW2得到的W→W和W2→W: 明指针在形状图上的移动引起的形状图变化主要体 而对于第(2)和(3)类蕴涵规则，由于它们都是针对 现在浓缩节点所代表的节点个数的变化上 浓缩节点的e和a的规则，其效果已体现在节点相 4.1循环不变形状图推断算法的框架 容的定义中，因而不必作为重写规则 根据基于抽象解释的循环不变式推断框架[四， G1.1V…VG1.m→G2.1V…VG2n的判定方法可 循环不变形状图的推断算法框架如图13.为表达简 通过略微修改3.2节的等价式判断方法中的(3)和 单起见，本节用字母9表示可以出现形状图析取的 (4)两点即可得到： 形状图. (3)若某个G2(1≤≤n)的某条尽可能长的且 不经过浓缩节点的访问路径是某个G1.:(1≤i≤m) 对于循环while(B)S (1)计算循环前条件Go=Gm.i=0. 的某条不经过浓缩节点的访问路径或其真前缀，但 (2)根据形状图逻辑的规则计算G+1,使得 不是指向同类节点，则尝试使用上面提到的蕴涵规 (G:A B)SIG+). (3)应用抽象规则计算G:+1,使得G+1→G:+1. 则对G:进行重写. (4)若G+1→SoV…VG:,则GoV…VG:是循环不变形状 例如，若图11规则右部两个窗口之一和左部窗 图，否则，i=十1，转(2). 口分别出现在G1:和G2中的上述位置，则使用相应 图13循环不变形状图推断的算法框架 蕴涵规则重写G1,把窗口中内容归约成谓词节点. (4)对每个G1(1≤i≤m),若存在某个G2 下面对图13的算法框架做一些解释： (1≤j≤n),使得G1:相容于G2,则GV…VG1.m→ (1)算法第(2)步根据形状图逻辑的规则计算 G2.V…VG2m,否则该蕴涵式不成立 G+1,G:∧B代表形状图g:和符号断言B的合取， 若碰到引起内存泄漏的操作、悬空指针或null指 4 循环不变形状图和递归函数前后 针脱引用(dereference)操作，则无规则可用，报告 形状图的推断 错误 (2)算法第(3)步的抽象是指：对形状图上随循 本节应用第3节的形状图理论判定方法来推断 环迭代次数变化而变化的浓缩节点（指其代表的结 循环不变形状图.该推断方法的一个变种可用来推 构节点数随迭代次数变化而变化)，把其代表结构节 断递归函数的前后形状图. 点数的表达式换成能概括多次（甚至全部）迭代情况 形状图是指针有效性和指针相等性断言的集合 的表达式.应用的抽象规则是采用文献[10]中第 的图形表示，循环不变形状图就是循环不变式中有 2.3节的蕴涵规则， 关指针断言的那部分不变式，函数前后形状图就是 (3)算法第(4)步G+1→gV…V9:的证明是采 函数前后条件中有关指针的那部分断言. 用3.3节的判定方法， 对易变数据结构的处理，循环语句通常完成下 以2.3节的那段单链表代码（假定至少有一个 面功能之一： 表元)的循环不变形状图（图8(1）)的推断为例.各 (1)寻找数据结构中的操作位置或依次对各节 程序点的形状图见图14，图中j是形状分析系统引 点上数据进行操作，这时，除了某些声明指针的指向 入的虚拟变量.第1次迭代后G1→G不成立，但第2 在节点间移动外，形状图没有其他变化。 次迭代后能证明G2→G。VG1,因此G。VG1是循环 (2)循环体的每次迭代都在对数据结构进行节 不变形状图.由于G→G,因此GVG1可简化为 点插入或删除.循环体执行过程中虽然破坏了数据 G1.由于没有程序变量可以替代G1中的虚拟变量j, 结构的形状，但每次到达循环体结束点时，形状得到 则略去j,得到结果就是图8(1). 恢复，仅节点个数发生变化 4.2算法终止的讨论 (3)循环体的每次迭代都在对数据结构某些节 图13算法终止取决于下面3点： 点的边的指向进行调整，并且有可能出现这样的情 (1)算法第(3)步的抽象能够成功 况：每次迭代结束时形状并未得到恢复，但在整个循 (2)算法第(4)步的蕴涵式的证明因得到结果 环执行结束时形状得到恢复，例如文献[10]中例2 而终止或因形状检查发现错误而终止价重写系统化简形状图后，适当地使用形状图的蕴 涵规则．所使用的蕴涵规则是２．２节中第（１）类蕴涵 规则，即由犠犠１∨犠２得到的犠１犠和犠２犠； 而对于第（２）和（３）类蕴涵规则，由于它们都是针对 浓缩节点的ｅ和ａ的规则，其效果已体现在节点相 容的定义中，因而不必作为重写规则． 犌１，１∨…∨犌１，犿犌２，１∨…∨犌２，狀的判定方法可 通过略微修改３．２节的等价式判断方法中的（３）和 （４）两点即可得到： （３）若某个犌２，犼（１犼狀）的某条尽可能长的且 不经过浓缩节点的访问路径是某个犌１，犻（１犻犿） 的某条不经过浓缩节点的访问路径或其真前缀，但 不是指向同类节点，则尝试使用上面提到的蕴涵规 则对犌１，犻进行重写． 例如，若图１１规则右部两个窗口之一和左部窗 口分别出现在犌１，犻和犌２，犼中的上述位置，则使用相应 蕴涵规则重写犌１，犻，把窗口中内容归约成谓词节点． （４）对每个犌１，犻（１犻犿），若存在某个犌２，犼 （１犼狀），使得犌１，犻相容于犌２，犼，则犌１，１∨…∨犌１，犿 犌２，１∨…∨犌２，狀，否则该蕴涵式不成立． ４循环不变形状图和递归函数前后 形状图的推断 本节应用第３节的形状图理论判定方法来推断 循环不变形状图．该推断方法的一个变种可用来推 断递归函数的前后形状图． 形状图是指针有效性和指针相等性断言的集合 的图形表示，循环不变形状图就是循环不变式中有 关指针断言的那部分不变式，函数前后形状图就是 函数前后条件中有关指针的那部分断言． 对易变数据结构的处理，循环语句通常完成下 面功能之一： （１）寻找数据结构中的操作位置或依次对各节 点上数据进行操作．这时，除了某些声明指针的指向 在节点间移动外，形状图没有其他变化． （２）循环体的每次迭代都在对数据结构进行节 点插入或删除．循环体执行过程中虽然破坏了数据 结构的形状，但每次到达循环体结束点时，形状得到 恢复，仅节点个数发生变化． （３）循环体的每次迭代都在对数据结构某些节 点的边的指向进行调整，并且有可能出现这样的情 况：每次迭代结束时形状并未得到恢复，但在整个循 环执行结束时形状得到恢复．例如文献［１０］中例２ 使用的双向链表倒置算法． 对于这类循环，在循环体的每条执行路径上，声 明指针在形状图上的移动引起的形状图变化主要体 现在浓缩节点所代表的节点个数的变化上． ４１循环不变形状图推断算法的框架 根据基于抽象解释的循环不变式推断框架［１１］， 循环不变形状图的推断算法框架如图１３．为表达简 单起见，本节用字母%表示可以出现形状图析取的 形状图． 对于循环ｗｈｉｌｅ（犅）犛 （１）计算循环前条件%０＝%狆狉犲．犻＝０． （２）根据形状图逻辑的规则计算%′犻＋１，使得 ｛%犻∧犅｝犛｛%′犻＋１｝． （３）应用抽象规则计算%犻＋１，使得%′犻＋１%犻＋１． （４）若%犻＋１%０∨…∨%犻，则%０∨…∨%犻是循环不变形状 图；否则，犻＝犻＋１，转（２）． 图１３循环不变形状图推断的算法框架 下面对图１３的算法框架做一些解释： （１）算法第（２）步根据形状图逻辑的规则计算 %′犻＋１，%犻∧犅代表形状图%犻和符号断言犅的合取［１１］． 若碰到引起内存泄漏的操作、悬空指针或ｎｕｌｌ指 针脱引用（ｄｅｒｅｆｅｒｅｎｃｅ）操作，则无规则可用，报告 错误．（２）算法第（３）步的抽象是指：对形状图上随循 环迭代次数变化而变化的浓缩节点（指其代表的结 构节点数随迭代次数变化而变化），把其代表结构节 点数的表达式换成能概括多次（甚至全部）迭代情况 的表达式．应用的抽象规则是采用文献［１０］中第 ２．３节的蕴涵规则． （３）算法第（４）步%犻＋１%０∨…∨%犻的证明是采 用３．３节的判定方法． 以２．３节的那段单链表代码（假定至少有一个 表元）的循环不变形状图（图８（１））的推断为例．各 程序点的形状图见图１４，图中犼是形状分析系统引 入的虚拟变量．第１次迭代后犌１犌０不成立，但第２ 次迭代后能证明犌２犌０∨犌１，因此犌０∨犌１是循环 不变形状图．由于犌０犌１，因此犌０∨犌１可简化为 犌１．由于没有程序变量可以替代犌１中的虚拟变量犼， 则略去犼，得到结果就是图８（１）． ４２算法终止的讨论 图１３算法终止取决于下面３点： （１）算法第（３）步的抽象能够成功． （２）算法第（４）步的蕴涵式的证明因得到结果 而终止或因形状检查发现错误而终止． １２期 张昱等：形状图理论的定理证明 ２４６９