2468 计算 机 学报 2016年 等价重写系统并未考虑个数不同的形状图之间的等 3.3 G.1V…VG.m→G2.1V…VG2.n的判定方法 价性，为此需要利用文献[10]中2.3节里的W台 该判定方法用于程序分析和验证过程中对形状 W:VW2等价规则（如图11）展开形状图，以期建立 图蕴涵关系的判定，例如第4节的循环不变形状图 个数不同的形状图之间的等价性.结合应用场合的 和递归函数前后形状图的推断算法需要用到该方 特点，本文讨论的等价式中各形状图的声明变量集 法.先定义节点相容和形状图相容。 都相同，等价式的判定方法如下： 定义4.节点n1和2若满足下面的条件，则 1相容于2（与定义1的区别仅在条件(2）). (1)1和n2是同类节点.并且若都是声明节点、 结构节点或浓缩节点，则有同样的出边及其标记：若 都是谓词节点，则谓词名相同。 (2)若1和2是同类浓缩节点或谓词节点，且 图11从二叉树定义得到的等价规则 分别带e1与a1和e2与a2,则必须满足(e1==e2 (1)若G.1和G2.1的声明变量集不同则该等价 a1)→a2. 式不成立，否则继续下面步骤. 定义5.形状子图G1和G2若满足下面3个条 (2)将上式中所有的形状图，用3.1节介绍的 件，则称G1相容于G2: 形状图重写系统把它们归约到最简形状图.仍用原 (1)G的节点集N到G2的节点集N2有一对一 来的符号G1.(1≤i≤m)或G2,(1≤j≤n)代表各形 的函数f,使得N2一f(N1)若非空，则其中只有浓 状图的最简形状图. 缩节点并且每个浓缩节点的(e==0)八a可满足， (3)若某个G1.:(1≤i≤m)的某条尽可能长的且 即这些浓缩节点可以有e等于0的情况， 不经过浓缩节点的访问路径是某个G2.,(1≤j≤n) (2)对任何n∈N1,n相容于f(n). 的某条不经过浓缩节点的访问路径的真前缀，并且 (3)对任何n∈N1,若n和f(n)的某标记相 若G1.:中的这条访问路径指向的节点可以用W台 同的出边分别指向节点1和2，则2经过m个 W1VW,的等价规则展开，则将其展开.反之亦然.直 (m≥0)属于N2一f(N1)的浓缩节点后所到达的2 到不存在这样的路径或者虽存在但不能展开为止. 和1满足f(11)=n2, 为防止滥用W台W,VWz这类等价规则，需要 对于图12的G1和G2,G1的那个浓缩节点经f 从访问路径的比较上加以限制.例如，若G1:中有不 函数映射到G2最右边的那个浓缩节点.因为G2左 能再延长的二叉树访问路径p→1，G2,中有访问路 边两个浓缩节点的和k都可以等于0，所以G1相 径p→r,且在G:中p→1指向谓词节点，则可以 容于G2. 根据图11的二叉树等价规则将G1:展开，其中等价 规则中的s是占位符，可以通配访问路径p→1中的 1.该规则由图2的二叉树定义得到. 文献[10]中2.3节里的所有的W台W,VW2都 像图11这样，右边W1或W2中指向谓词节点或浓缩 节点的访问路径比W的多一个结构体的指针域，因 此不会出现等价式左右两边的形状图不断交替展开 nt 而不终止的情况 经过这样的展开，原等价式变换成G.:V…V m>=0Am<5k>=0Mk<8 G Gim台G2.,V…VG2.. (4)对每个G1:(1≤i≤m'),若存在某个G2 图12帮助理解定义5的两个形状图 (1≤≤n'),使得G:和G2相同，并且反之亦然，则 定义6.形状图G1和G2若满足下面的条件， G.1V…VG1m台G2.1V…VG2m,否则该式不成立. 则称G相容于G2. 显然，若上述方法中涉及的由整型线性表达式 G,和G2的形状子图一一对应并且G的每个形 之间的关系式所构成的断言都可判定，则G.1V…V 状子图相容于G2中对应的形状子图. G1.m台G2.1V…VG2n可判定. 在证明形状图之间的蕴涵时，需要考虑在用等等价重写系统并未考虑个数不同的形状图之间的等 价性，为此需要利用文献［１０］中２．３节里的犠 犠１∨犠２等价规则（如图１１）展开形状图，以期建立 个数不同的形状图之间的等价性．结合应用场合的 特点，本文讨论的等价式中各形状图的声明变量集 都相同，等价式的判定方法如下： 图１１从二叉树定义得到的等价规则 （１）若犌１，１和犌２，１的声明变量集不同则该等价 式不成立．否则继续下面步骤． （２）将上式中所有的形状图，用３．１节介绍的 形状图重写系统把它们归约到最简形状图．仍用原 来的符号犌１，犻（１犻犿）或犌２，犼（１犼狀）代表各形 状图的最简形状图． （３）若某个犌１，犻（１犻犿）的某条尽可能长的且 不经过浓缩节点的访问路径是某个犌２，犼（１犼狀） 的某条不经过浓缩节点的访问路径的真前缀，并且 若犌１，犻中的这条访问路径指向的节点可以用犠 犠１∨犠２的等价规则展开，则将其展开．反之亦然．直 到不存在这样的路径或者虽存在但不能展开为止． 为防止滥用犠犠１∨犠２这类等价规则，需要 从访问路径的比较上加以限制．例如，若犌１，犻中有不 能再延长的二叉树访问路径狆→ｌ，犌２，犼中有访问路 径狆→ｌ→ｒ，且在犌１，犻中狆→ｌ指向谓词节点，则可以 根据图１１的二叉树等价规则将犌１，犻展开，其中等价 规则中的ｓ是占位符，可以通配访问路径狆→ｌ中的 ｌ．该规则由图２的二叉树定义得到． 文献［１０］中２．３节里的所有的犠犠１∨犠２都 像图１１这样，右边犠１或犠２中指向谓词节点或浓缩 节点的访问路径比犠的多一个结构体的指针域，因 此不会出现等价式左右两边的形状图不断交替展开 而不终止的情况． 经过这样的展开，原等价式变换成犌′１，１∨…∨ 犌′１，犿′犌′２，１∨…∨犌′２，狀′． （４）对每个犌′１，犻（１犻犿′），若存在某个犌′２，犼 （１犼狀′），使得犌′１，犻和犌′２，犼相同，并且反之亦然，则 犌１，１∨…∨犌１，犿犌２，１∨…∨犌２，狀，否则该式不成立． 显然，若上述方法中涉及的由整型线性表达式 之间的关系式所构成的断言都可判定，则犌１，１∨…∨ 犌１，犿犌２，１∨…∨犌２，狀可判定． ３３犌１，１∨…∨犌１，犿犌２，１∨…∨犌２，狀的判定方法 该判定方法用于程序分析和验证过程中对形状 图蕴涵关系的判定，例如第４节的循环不变形状图 和递归函数前后形状图的推断算法需要用到该方 法．先定义节点相容和形状图相容． 定义４．节点狀１和狀２若满足下面的条件，则 狀１相容于狀２（与定义１的区别仅在条件（２））． （１）狀１和狀２是同类节点．并且若都是声明节点、 结构节点或浓缩节点，则有同样的出边及其标记；若 都是谓词节点，则谓词名相同． （２）若狀１和狀２是同类浓缩节点或谓词节点，且 分别带ｅ１与ａ１和ｅ２与ａ２，则必须满足（ｅ１＝＝ｅ２∧ ａ１）ａ２．定义５．形状子图犌１和犌２若满足下面３个条 件，则称犌１相容于犌２． （１）犌１的节点集犖１到犌２的节点集犖２有一对一 的函数犳，使得犖２－犳（犖１）若非空，则其中只有浓 缩节点并且每个浓缩节点的（ｅ＝＝０）∧ａ可满足， 即这些浓缩节点可以有ｅ等于０的情况． （２）对任何狀∈犖１，狀相容于犳（狀）． （３）对任何狀∈犖１，若狀和犳（狀）的某标记相 同的出边分别指向节点狀１和狀２，则狀２经过犿个 （犿０）属于犖２－犳（犖１）的浓缩节点后所到达的狀′２ 和狀１满足犳（狀１）＝狀′２． 对于图１２的犌１和犌２，犌１的那个浓缩节点经犳 函数映射到犌２最右边的那个浓缩节点．因为犌２左 边两个浓缩节点的犿和犽都可以等于０，所以犌１相 容于犌２． 图１２帮助理解定义５的两个形状图 定义６．形状图犌１和犌２若满足下面的条件， 则称犌１相容于犌２． 犌１和犌２的形状子图一一对应并且犌１的每个形 状子图相容于犌２中对应的形状子图． 在证明形状图之间的蕴涵时，需要考虑在用等 ２４６８ 计 算 机 学 报 ２０１６年