2470 计算 机 学报 2016年 ptrl-head;ptr=head->next;j=0; 用含相应虚拟变量的线性表达式来表示， (2)从第3节知道，形状图蕴涵关系判定方法的 终止性依赖于判断浓缩节点之间蕴涵与否的(e== head nex 1e% e'∧a)→a'的证明的终止性.下面是相关的分析. while (ptr!=NULL)( 对于循环体S的任意一条执行路径，对于除第 1次迭代计算以外的其他各次迭代计算的结果形状 t 图，若与上次迭代计算的结果形状图相比，某浓缩节 点所代表的节点数发生变化，则再次迭代计算引起 的变化与本次迭代计算的变化相同.若循环前某浓 ptrl=ptr:ptr-=ptr->next;j+l; (j==1) 缩节点代表ax+b个节点，第1次迭代时，个数变化 D 是d,随后各次迭代的个数变化是c,则该路径执行 Iptr y(y>1)次结束时，该浓缩节点代表的节点数是(a.x+ b)+(cy+d),由于(ax+b)在循环执行过程中不 }把最左结构节点等价变换成结构节点个数为且 变，因此在图13算法中证明形状图之间的蕴涵时可 j==1的浓缩节点.把j==1抽象成>=0，得到G 当成常量.这样，在每次迭代计算过程中，浓缩节点 所代表节点的个数本质上可用该路径的虚拟变量的 线性表达式来表示，这就保证了该浓缩节点的表达 ead nex nex 式e维持为线性.类似的分析可知a中的整型表达 ,>=0 式也是线性.这就保证(e==e'∧a)→a'的证明会终 从G,开始进行第2次迭代 止.图14例子的迭代过程体现了这里所说的对浓缩 略去中间的部分形状图 (j==2)》 节点的抽象。 另一方面，在有p=p→next这样指针赋值的 情况下，除第1次迭代计算外，若一次迭代计算的结 G○he4nex 13 果形状图中出现无声明节点指向的结构节点，但又 j-1,>=1A==2 不能折叠成（或并入相邻）浓缩节点，则表明该结构 把最左结构节点并入左边浓缩节点，后者个数增为j 节点的出边的指向不符合数据结构定义的要求，先 且j==2(>=1多余).把j==2抽象成=0，得到G 前关于循环语句的3种用法中不会出现这样的情 况.因此，若经抽象后，相邻2个声明指针所指向的 ptrl 节点之间的结构和浓缩节点的个数大于3（简称节 点个数约束)，则在循环体结束点的形状检查[]会 ,1=0 报告错误并终止迭代， 图14推断循环不变式的迭代过程 例如，对于各节点都有指针域1和r的双向非 (3)若形状检查没有发现错误，算法第(4)步的 空链表，用循环依次将各节点的I域置为NULL且 蕴涵式最终会成立， r域的指向不变.代码如下： 该算法终止的理由概述如下： p=head; (1)本文为循环体S的每条执行路径都安排累 while(p→rl=NULL){ 计该路径执行次数的虚拟变量.选择一种合适的虚 p=p→r:p→l=NULL: 拟变量命名方式，能应对出现并列和嵌套循环的情 } 况以及循环体中出现并列和嵌套条件语句的情况. 这相当于废弃1域，用r来构成一个单链表.图15 在增加虚拟变量时，还要把表达虚拟变量之间关系 (1)是循环人口的形状图，图15(2)是经过3次迭代 的等式或不等式加到相关形状图中. 的形状图.本算法无法把已经遍历过的结构节点折 通过增设虚拟变量，结合下面(2)有关浓缩节点 叠为浓缩节点，因为双向链表没有相应的规则.形状 的e表达式为线性的讨论，算法第(3)步的抽象就能 检查会因两个相邻声明节点超出节点个数约束而报 够成功，即可以把浓缩节点所概括的节点数抽象为 告错误图１４推断循环不变式的迭代过程 （３）若形状检查没有发现错误，算法第（４）步的 蕴涵式最终会成立． 该算法终止的理由概述如下： （１）本文为循环体犛的每条执行路径都安排累 计该路径执行次数的虚拟变量．选择一种合适的虚 拟变量命名方式，能应对出现并列和嵌套循环的情 况以及循环体中出现并列和嵌套条件语句的情况． 在增加虚拟变量时，还要把表达虚拟变量之间关系 的等式或不等式加到相关形状图中． 通过增设虚拟变量，结合下面（２）有关浓缩节点 的ｅ表达式为线性的讨论，算法第（３）步的抽象就能 够成功，即可以把浓缩节点所概括的节点数抽象为 用含相应虚拟变量的线性表达式来表示． （２）从第３节知道，形状图蕴涵关系判定方法的 终止性依赖于判断浓缩节点之间蕴涵与否的（ｅ＝＝ ｅ′∧ａ）ａ′的证明的终止性．下面是相关的分析． 对于循环体犛的任意一条执行路径，对于除第 １次迭代计算以外的其他各次迭代计算的结果形状 图，若与上次迭代计算的结果形状图相比，某浓缩节 点所代表的节点数发生变化，则再次迭代计算引起 的变化与本次迭代计算的变化相同．若循环前某浓 缩节点代表犪狓＋犫个节点，第１次迭代时，个数变化 是犱，随后各次迭代的个数变化是犮，则该路径执行 狔（狔＞１）次结束时，该浓缩节点代表的节点数是（犪狓＋ 犫）＋（犮狔＋犱），由于（犪狓＋犫）在循环执行过程中不 变，因此在图１３算法中证明形状图之间的蕴涵时可 当成常量．这样，在每次迭代计算过程中，浓缩节点 所代表节点的个数本质上可用该路径的虚拟变量的 线性表达式来表示，这就保证了该浓缩节点的表达 式ｅ维持为线性．类似的分析可知ａ中的整型表达 式也是线性．这就保证（ｅ＝＝ｅ′∧ａ）ａ′的证明会终 止．图１４例子的迭代过程体现了这里所说的对浓缩 节点的抽象． 另一方面，在有狆＝狆→ｎｅｘｔ这样指针赋值的 情况下，除第１次迭代计算外，若一次迭代计算的结 果形状图中出现无声明节点指向的结构节点，但又 不能折叠成（或并入相邻）浓缩节点．则表明该结构 节点的出边的指向不符合数据结构定义的要求，先 前关于循环语句的３种用法中不会出现这样的情 况．因此，若经抽象后，相邻２个声明指针所指向的 节点之间的结构和浓缩节点的个数大于３（简称节 点个数约束），则在循环体结束点的形状检查［１０］会 报告错误并终止迭代． 例如，对于各节点都有指针域ｌ和ｒ的双向非 空链表，用循环依次将各节点的ｌ域置为ＮＵＬＬ且 ｒ域的指向不变．代码如下： 狆＝ｈｅａｄ； ｗｈｉｌｅ（狆→ｒ！＝ＮＵＬＬ）｛ 狆＝狆→ｒ；狆→ｌ＝ＮＵＬＬ； ｝ 这相当于废弃ｌ域，用ｒ来构成一个单链表．图１５ （１）是循环入口的形状图，图１５（２）是经过３次迭代 的形状图．本算法无法把已经遍历过的结构节点折 叠为浓缩节点，因为双向链表没有相应的规则．形状 检查会因两个相邻声明节点超出节点个数约束而报 告错误． ２４７０ 计 算 机 学 报 ２０１６年