12期 张昱等：形状图理论的定理证明 2471 ① Suan和Sar (2)从函数前形状图gmn和Sm通过形状图逻 (1) 辑的规则得到Go,使得{g,}Swm{go}.令i=0 (3)根据形状图逻辑的规则计算G+1,使得 {gtn}Sx{gi+1}.其中gm,和g:作为Sx中出现的 递归函数调用的前后形状图 (4)应用抽象规则计算9+1，使得9：+1→9+1. ead (5)若G+1→GV…VGg,则goV…Vg:是函数 后形状图；否则，i=i十1，转(3). (2) 除了推断递归函数的函数前后条件需先分析函 数的非递归和递归的执行路径外，本算法与图13算 图15循环不变形状图推断过程报告错误的例子 法没有本质上的区别，把本算法的第(2)到(5)步与 (3)由于声明指针的个数有限，再加上(2)提到 图13算法的第(1)到(4)步比较就可以看出这一点. 的节点个数约束，在循环体结束点能形成的不等价 形状图有限.若未见报告程序错误，则一定存在i, 5 形状图理论和整数理论组合的 使得G+1→GoV…VG成立. 判定方法 4.3递归函数前后形状图的推断 对于非递归函数，可以从函数前形状图自动推 在程序验证器原型中，验证条件生成器所产生 断函数后形状图.但该方法难以用到有指针型形参 的验证条件的一般形式是： 且返回值是指针的递归函数，因为推断递归函数前 (G.1∧Q.)V…V(G1.mΛQ.m)→ 后形状图时要用到该函数的前后形状图， (G2.1ΛQ2.1)V…V(G2.mΛQ2.m) 若仅有指针型的形参，或仅有指针型的返回值， 其中Q代表符号断言的合取，并且其中没有指针相 根据形状系统对函数调用点和返回点的形状约束， 等性断言和有效性断言. 函数的递归性并没有给形状分析带来困难.倘若形 验证条件的证明是形状图理论和整数线性算术 参和返回值都是指针型，则虽有形状系统的约束，在 理论的组合的判定问题.首先，形状图之间蕴涵的证 函数返回点也不能确定实参指针和返回指针之间的 明要根据形状图理论.其次，Q中像p→d<q→nxt→ 关系，因而不能确定函数后形状图.关注实参指针是 d这样的断言，需要根据形状图来判断p→d和q→ 因为它的值在被调用函数中虽不变，但其指向的节 nxt·d分别是属于哪个节点的数据. 点在数据结构中的位置可能会变，为此，函数的前形 注意，在形状图中，浓缩节点和谓词节点可能附 状图增设虚拟变量来表示实参指针，它与形参指针 带e和a.这表明形状图理论内部涉及线性整数算 指向同一个节点，并据此来推断函数后形状图。 术理论，它与本节讨论的理论组合的判定问题没有 可以像推断循环不变形状图那样迭代推断函数 联系，因为系统原型限定e和a只依赖整型声明变 后形状图.因为计算会终止的递归函数总有非递归 量，不依赖于节点的数据.因为e和a是决定该浓缩 的出口，可以先通过非递归路径得到函数后形状图 节点或谓词节点所代表的链表（段）的长度、或者所 的初值，然后再在递归路径上迭代求解. 代表的二叉树片段的高度的表达式和断言，通常在 对于直接递归函数，若函数体中的循环语句里 实际编程中不会把决定某种数据结构的长度或高度 面没有递归调用（通常如此），则函数前后形状图的 的信息存放在该数据结构节点的域中， 推断方法概述如下： 本节讨论组合理论的两种证明方式 (1)通过程序分析，确定函数体中非递归执行 5.1易变数据结构上被关注性质的描述 路径和递归执行路径的语句序列.这里所说的执行 通常关注易变数据结构3个层次的性质： 路径把无递归调用的循环语句看成一个语句，把两 (1)各个节点是否连接成预定的形状 个分支都有（或都无）递归调用的条件语句也看成 该性质的验证在形状分析阶段完成，程序员只 个语句，以减少要考虑的路径数.为叙述方便，假定 要像声明类型那样声明形状即可.这仅是形状图理 非递归和递归的执行路径各一条，语句序列分别是 论上的问题.图１５循环不变形状图推断过程报告错误的例子 （３）由于声明指针的个数有限，再加上（２）提到 的节点个数约束，在循环体结束点能形成的不等价 形状图有限．若未见报告程序错误，则一定存在犻， 使得%犻＋１%０∨…∨%犻成立． ４３递归函数前后形状图的推断 对于非递归函数，可以从函数前形状图自动推 断函数后形状图．但该方法难以用到有指针型形参 且返回值是指针的递归函数，因为推断递归函数前 后形状图时要用到该函数的前后形状图． 若仅有指针型的形参，或仅有指针型的返回值， 根据形状系统对函数调用点和返回点的形状约束， 函数的递归性并没有给形状分析带来困难．倘若形 参和返回值都是指针型，则虽有形状系统的约束，在 函数返回点也不能确定实参指针和返回指针之间的 关系，因而不能确定函数后形状图．关注实参指针是 因为它的值在被调用函数中虽不变，但其指向的节 点在数据结构中的位置可能会变．为此，函数的前形 状图增设虚拟变量来表示实参指针，它与形参指针 指向同一个节点，并据此来推断函数后形状图． 可以像推断循环不变形状图那样迭代推断函数 后形状图．因为计算会终止的递归函数总有非递归 的出口，可以先通过非递归路径得到函数后形状图 的初值，然后再在递归路径上迭代求解． 对于直接递归函数，若函数体中的循环语句里 面没有递归调用（通常如此），则函数前后形状图的 推断方法概述如下： （１）通过程序分析，确定函数体中非递归执行 路径和递归执行路径的语句序列．这里所说的执行 路径把无递归调用的循环语句看成一个语句，把两 个分支都有（或都无）递归调用的条件语句也看成一 个语句，以减少要考虑的路径数．为叙述方便，假定 非递归和递归的执行路径各一条，语句序列分别是 犛狀狅狀和犛狉犲犮． （２）从函数前形状图%犲狀狋狉狔和犛狀狅狀通过形状图逻 辑的规则得到%０，使得｛%犲狀狋狉狔｝犛狀狅狀｛%０｝．令犻＝０． （３）根据形状图逻辑的规则计算%′犻＋１，使得 ｛%犲狀狋狉狔｝犛狉犲犮｛%′犻＋１｝．其中%犲狀狋狉狔和%犻作为犛狉犲犮中出现的 递归函数调用的前后形状图． （４）应用抽象规则计算%犻＋１，使得%′犻＋１%犻＋１． （５）若%犻＋１%０∨…∨%犻，则%０∨…∨%犻是函数 后形状图；否则，犻＝犻＋１，转（３）． 除了推断递归函数的函数前后条件需先分析函 数的非递归和递归的执行路径外，本算法与图１３算 法没有本质上的区别，把本算法的第（２）到（５）步与 图１３算法的第（１）到（４）步比较就可以看出这一点． ５形状图理论和整数理论组合的 判定方法 在程序验证器原型中，验证条件生成器所产生 的验证条件的一般形式是： （犌１，１∧犙１，１）∨…∨（犌１，犿∧犙１，犿） （犌２，１∧犙２，１）∨…∨（犌２，狀∧犙２，狀） 其中犙代表符号断言的合取，并且其中没有指针相 等性断言和有效性断言． 验证条件的证明是形状图理论和整数线性算术 理论的组合的判定问题．首先，形状图之间蕴涵的证 明要根据形状图理论．其次，犙中像狆→犱＜狇→ｎｘｔ→ 犱这样的断言，需要根据形状图来判断狆→犱和狇→ ｎｘｔ→犱分别是属于哪个节点的数据． 注意，在形状图中，浓缩节点和谓词节点可能附 带ｅ和ａ．这表明形状图理论内部涉及线性整数算 术理论．它与本节讨论的理论组合的判定问题没有 联系，因为系统原型限定ｅ和ａ只依赖整型声明变 量，不依赖于节点的数据．因为ｅ和ａ是决定该浓缩 节点或谓词节点所代表的链表（段）的长度、或者所 代表的二叉树片段的高度的表达式和断言，通常在 实际编程中不会把决定某种数据结构的长度或高度 的信息存放在该数据结构节点的域中． 本节讨论组合理论的两种证明方式． ５１易变数据结构上被关注性质的描述 通常关注易变数据结构３个层次的性质： （１）各个节点是否连接成预定的形状 该性质的验证在形状分析阶段完成，程序员只 要像声明类型那样声明形状即可．这仅是形状图理 论上的问题． １２期 张昱等：形状图理论的定理证明 ２４７１