形状图逻辑和形状系统 Shape graph logic and shape system

·基于双链表谓词定义的规则。 ·添加或取消ε=0的浓缩节点的规则。例如图5的规则(1)。 ·e>0的浓缩节点的展开和折叠规则。例如图5的规则(2)。 由于1和r的对称性，图5的规则(1)和(2)包括了浓缩节点处于结构节点右边的情况。 ·在带e和a的浓缩节点作为双向链表边缘节点时的展开与折叠规则。它们和图5的规 则(1)和(2)略有区别，图5的规则(3)是其中的一条。 ·无约束浓缩节点的展开与折叠规则。例如图5的规则(4)。浓缩节点右边是其他节点 以及浓缩节点本身是双向链表边缘节点的规则类似。 (2)导出规则 类似于单链表的情况，但没有可作为归纳定义的等价规则。 双链表定义和变换规则维持一个重要原则：除标记为r和1的边外，无其他边指向浓缩 节点。若有这种边，则浓缩节点展开时，不知该边应指在展开后的最左还是最右结构节点上。 e.a e,a e-l,a a→(e==0)(1) a(e>=1)(2) 0。 a(e==0)(3) 图5双链表的部分等价规则 3、二叉树的等价规则 除了基于tre(s)谓词定义的规则外，二叉树中有关浓缩节点的规则类似于单向链表的规 则，区别在于每个结构节点和浓缩节点多了一条指向谓词节点的边。图6的规则(1)和(2)是 其中的两条。 ree tree tree tree tree tree a-(e>=l)(1) a→(e>=1)(2) 图6二叉树的部分等价规则 从上述浓缩节点的展开与折叠规则可知，浓缩节点是若干相邻同类结构节点（出边条数 和标记都一样)的浓缩表示。 4、对浓缩节点的e和a进行替换的等价规则 图7的规则(1)和(2)分别是单链表和双链表浓缩节点在两边的e和a的变量集一样时的 规则。浓缩节点是双向链表边缘节点时的规则以及二叉树浓缩节点的规则可类似地给出。 6

6  基于双链表谓词定义的规则。  添加或取消 e = 0 的浓缩节点的规则。例如图 5 的规则(1)。  e > 0 的浓缩节点的展开和折叠规则。例如图 5 的规则(2)。 由于 l 和 r 的对称性，图 5 的规则(1)和(2)包括了浓缩节点处于结构节点右边的情况。  在带 e 和 a 的浓缩节点作为双向链表边缘节点时的展开与折叠规则。它们和图 5 的规 则(1)和(2)略有区别，图 5 的规则(3)是其中的一条。  无约束浓缩节点的展开与折叠规则。例如图 5 的规则(4)。浓缩节点右边是其他节点 以及浓缩节点本身是双向链表边缘节点的规则类似。 （2）导出规则 类似于单链表的情况，但没有可作为归纳定义的等价规则。 双链表定义和变换规则维持一个重要原则：除标记为 r 和 l 的边外，无其他边指向浓缩 节点。若有这种边，则浓缩节点展开时，不知该边应指在展开后的最左还是最右结构节点上。 3、二叉树的等价规则 除了基于 tree(s)谓词定义的规则外，二叉树中有关浓缩节点的规则类似于单向链表的规 则，区别在于每个结构节点和浓缩节点多了一条指向谓词节点的边。图 6 的规则(1)和(2)是 其中的两条。 从上述浓缩节点的展开与折叠规则可知，浓缩节点是若干相邻同类结构节点（出边条数 和标记都一样）的浓缩表示。 4、对浓缩节点的 e 和 a 进行替换的等价规则 图 7 的规则(1)和(2)分别是单链表和双链表浓缩节点在两边的 e 和 a 的变量集一样时的 规则。浓缩节点是双向链表边缘节点时的规则以及二叉树浓缩节点的规则可类似地给出。 图 5 双链表的部分等价规则  r pk r l l e, a r l r pk r l l a  (e ==0) a  (e >=1)  e, a r r l l e-1, a r l r r l l (1) (2)  a  (e ==0)  r l  r e, a r l r l (3) (4)   pk r l r l r l r l r l r l pk r r l l r l pk 图 6 二叉树的部分等价规则  e-1, a p1 pk r r l  tree l  tree e, a p1 pk r l  tree a  (e >=1) (1) a  (e >=1) e, a  p1 pk r l  tree e-1, a p1 pk r r l  tree l  tree (2)

出 el,al e2,a2 I e1,ar I e2,a2 (a1→(e1=e2Aa2)n(a2→(e2==e1Aa)(1) (a1→(e1==e2Λa2)A(a2→(c2=e1Aa1)(2) 图7对浓缩节点的e和a进行变换的部分等价规则 使用等价规则，可以对形状图进行变换。例如，若有等价规则W1一W和上下文G0, 则将该规则用于GW]可得到GW],反之亦然。写成G[W]一G[W]。类似地，由规则 W台W1vW知道GW一G[W]VG[W]。 下面再考虑蕴涵规则，它们用来表示保持语义蕴涵的形状图变换规则。蕴涵性在定义形 状图的语义后证明。 1、从等价规则W台W1VW2,可得W1三W和W三W两条蕴涵规则。 2、若等价规则W1台W3的副条件是(a1→(e1=c2Aa)A(a2→(e2=e1Aa),则有蕴涵规 则W1三W3和W→Wi,其副条件分别是(a1→(e1=e2Aa)和(a2→(e2=e1Aa1)。 3、将等价规则中浓缩节点改成无约束浓缩节点的蕴涵规则 ·若等价规则W1一W中，W和W2的浓缩节点分别带e1与a1和e2与a2且e1<e2,则 有蕴涵规则P1一2，W1与W2和W与W2的区别在于浓缩节点改为无约束浓缩节点。 ·若在等价规则W1白W2中，W2有带e与a的浓缩节点，W1无浓缩节点，则有蕴涵规 则W1一W2,其中严2和W2的区别在于W2中的浓缩节点改为无约束浓缩节点。 2.4形状图的语义 对于像C这样有动态存储分配的编程语言，形状图节点(ul和悬空节点除外)指称机 器栈单元、堆块或堆块集，边代表相应指针的值。一个没有浓缩节点和谓词节点的形状图是 一个机器状态中指针型数据的图形表示，而一般的形状图则是某个机器状态集的图形表示。 先定义节点和边的含义。在有栈和堆的机器上，节点所代表的程序变量及指称如下。 (1)声明节点代表程序中的声明指针，其出边的标记就是该声明指针的名字。声明节 点指称栈上的存储单元。 (2)结构节点代表由malloc调用动态生成的结构体变量，其出边的条数及标记与该结 构体变量的域指针的个数和名字一致。结构节点指称一个堆块，其存储单元的个数和地址与 该节点的出边条数和标记一样。 为集中于关注的重点，忽略非指针的变量及它们在机器上的存储单元。另外把无约束浓 缩节点看成带n和n≥0的浓缩节点，并入浓缩节点一起讨论。 (3)带e和a的浓缩节点代表n个结构体变量，指称n个分离的堆块，若e的值是n。 (4)u山节点和悬空节点都不代表任何程序元素，当然也不指称机器上任何东西。 (5)谓词节点代表若干个动态生成的结构体变量，指称堆上若干个分离的堆块。基于 23节的谓词展开规则，根据下面给出的有向边含义，可以明确这些堆块之间的联系。 有向边不代表任何程序元素，也不指称机器上任何存储单元。边的指向表明由其标记所 代表的声明指针（栈单元）或域指针（堆块单元）的值。 (1)若边指向结构节点，则相应指针的值是该结构节点所指称的堆块的地址。 (2)若边指向ul节点（悬空节点），则相应指针的值等于NULL(是悬空指针)。 由此可知，形状图中n条边集中指向一个还是分散指向n个nul节点（悬空节点）不 影响形状图的含义。为简单起见，本文是按分散指向来介绍规则的。 (3)边指向带e和a的浓缩节点。若e>0,则相应指针的值是浓缩节点展开后第1个 结构节点（以该边的指向为序）所指称的堆块的地址：若ε=O,则相应指针的含义在删除 这个节点后的形状图上确定。 1

7 使用等价规则，可以对形状图进行变换。例如，若有等价规则 W1W2 和上下文 G[]， 则将该规则用于 G[W1]可得到 G[W2]，反之亦然。写成 G[W1]  G[W2]。类似地，由规则 WW1W2知道 G[W]  G[W1]  G[W2]。 下面再考虑蕴涵规则，它们用来表示保持语义蕴涵的形状图变换规则。蕴涵性在定义形 状图的语义后证明。 1、从等价规则 WW1  W2，可得 W1  W 和 W2  W 两条蕴涵规则。 2、若等价规则 W1W2 的副条件是(a1  (e1==e2  a2))(a2  (e2==e1a1)，则有蕴涵规 则 W1W2和 W2W1，其副条件分别是(a1  (e1==e2a2))和(a2  (e2==e1a1)。 3、将等价规则中浓缩节点改成无约束浓缩节点的蕴涵规则  若等价规则 W1W2 中，W1 和 W2的浓缩节点分别带 e1 与 a1 和 e2 与 a2且 e1 < e2，则 有蕴涵规则 W1W2，W1与 W2 和 W1 与 W2的区别在于浓缩节点改为无约束浓缩节点。  若在等价规则 W1W2 中，W2 有带 e 与 a 的浓缩节点，W1无浓缩节点，则有蕴涵规 则 W1W2，其中 W2 和 W2 的区别在于 W2 中的浓缩节点改为无约束浓缩节点。 2.4 形状图的语义 对于像 C 这样有动态存储分配的编程语言，形状图节点（null 和悬空节点除外）指称机 器栈单元、堆块或堆块集，边代表相应指针的值。一个没有浓缩节点和谓词节点的形状图是 一个机器状态中指针型数据的图形表示，而一般的形状图则是某个机器状态集的图形表示。 先定义节点和边的含义。在有栈和堆的机器上，节点所代表的程序变量及指称如下。 （1）声明节点代表程序中的声明指针，其出边的标记就是该声明指针的名字。声明节 点指称栈上的存储单元。 （2）结构节点代表由 malloc 调用动态生成的结构体变量，其出边的条数及标记与该结 构体变量的域指针的个数和名字一致。结构节点指称一个堆块，其存储单元的个数和地址与 该节点的出边条数和标记一样。 为集中于关注的重点，忽略非指针的变量及它们在机器上的存储单元。另外把无约束浓 缩节点看成带 n 和 n  0 的浓缩节点，并入浓缩节点一起讨论。 （3）带 e 和 a 的浓缩节点代表 n 个结构体变量，指称 n 个分离的堆块，若 e 的值是 n。 （4）null 节点和悬空节点都不代表任何程序元素，当然也不指称机器上任何东西。 （5）谓词节点代表若干个动态生成的结构体变量，指称堆上若干个分离的堆块。基于 2.3 节的谓词展开规则，根据下面给出的有向边含义，可以明确这些堆块之间的联系。 有向边不代表任何程序元素，也不指称机器上任何存储单元。边的指向表明由其标记所 代表的声明指针（栈单元）或域指针（堆块单元）的值。 （1）若边指向结构节点，则相应指针的值是该结构节点所指称的堆块的地址。 （2）若边指向 null 节点（悬空节点），则相应指针的值等于 NULL（是悬空指针）。 由此可知，形状图中 n 条边集中指向一个还是分散指向 n 个 null 节点（悬空节点）不 影响形状图的含义。为简单起见，本文是按分散指向来介绍规则的。 （3）边指向带 e 和 a 的浓缩节点。若 e > 0，则相应指针的值是浓缩节点展开后第 1 个 结构节点（以该边的指向为序）所指称的堆块的地址；若 e = 0，则相应指针的含义在删除 这个节点后的形状图上确定。 图 7 对浓缩节点的 e 和 a 进行变换的部分等价规则 (a1(e1==e2a2))(a2(e2==e1a1))  e2, a2 p1 pk nt e1, a1 p1 pk nt (1)  r r l l e1, a1 r r l l e2, a2 (a1(e1==e2a2))(a2(e2==e1a1)) (2)

(4)若边指向谓词节点，则边的含义在展开谓词节点后的形状图上确定。 再定义形状图的语义。对于非NULL且非悬空的指针，认为它的值就是它所指向堆块 的抽象地址，对应地，动态分配的各堆块的地址是各不相同的抽象值。再认为栈和各堆块上 的存储单元分别按声明指针和域指针的名字访问。机器的抽象状态（以下简称机器状态）就 可由两个函数：sa:DecVar→AbsValueN,△}和sr:AbsValue×FieldVar→AbsValueN,△} 构成，其中sa的定义域是声明指针集，它给出声明指针的抽象值。AbsValue是堆块抽象地 址集，FieldVar是域指针名字集，sr给出程序能访问到的各堆块的域指针的抽象值，N和△是 两个特殊的抽象值。下面用s或s,s)表示机器状态。 在此简化下，基于先前节点和边的含义，一个没有浓缩节点和谓词节点的形状图G则 是某个机器状态的图形表示，而一般的形状图则是某个机器状态集的图形表示。 定义4形状图G所代表的机器状态集DG刀由下面几条规则定义。 (1)若G无浓缩节点和谓词节点，则DG刀中只有一个状态。G直接体现该状态，其中 所有声明节点及其出边的指向构成函数s,各结构节点及其出边的指向构成函数s (2)G有带e和a的浓缩节点。若a蕴涵e可等于k个值，这k种情况下浓缩节点完 全展开后的形状图分别是G1.,Gk,则DGD=卫G0U.U卫G0:若a蕴涵e可等于0， 1,.,浓缩节点完全展开成n个结构节点(n≥0)的形状图是Gn,则四GD=四G0UnG☐ (3)若G有谓词节点，且谓词节点展开后的形状图是G或G1vG2,则加G刀=DGT 或DGD=DG0UIG0。 很容易进一步定义形状图G1vG2y..VGn的语义。 形状图上的路径描述采用和程序中访问路径同样的语法形式，以利于讨论两者之间的对 应。显然，只需要考虑从声明节点开始到达某个节点的路径，分成下面两种情况。 (1)路径的完全表示。若路径最多到达浓缩节点，则由依次列出路径各边上的标记来 表示该路径。若边上的标记依次为p,L,【,则写成p>>r。 (2)路径的浓缩表示。若路径包括带e和a的浓缩节点的出边l,则路径需使用上角标 来表示重复次数。例如在图2(b)中，有head(->next)m和head(->next)m>next等路径。 显然，形状图上一条路径的最后一条边上的标记所代表的程序指针，与程序中表示这个 指针的访问路径一致，以下统称它们为访问路径。 形状图是程序中指针有效性断言和指针相等断言等的图形表示。 定义5形状图G所表示的断言集A口G刀由下面这些有关指针的断言组成： (1)指向结构节点的指针都是有效指针，指向ul节点或悬空节点的指针都是无效指 针。 (2)指向同一个结构节点或谓词节点的指针相等，指向浓缩节点展开后的同一个结构 节点的指针相等，例如图2(b)表示的断言中有head(->next)m>next=ptr: (3)指向u山节点（悬空节点）的指针都等于NULL(是悬空指针)： (4)指向谓词节点的指针都满足相应的谓词。 基于这个断言集，可以知道哪些指针不相等，可以推导哪些访问路径互为别名。 定理1对任何形状图G,DG刀的状态都满足A☐GD的所有断言，写成Vs:刃GD.s☐ADG刀。 并且对任何sgIG刀，若dom(s'd)=dom(sd)(se)且二元函数sr:AbsValue×FieldVar→ AbsValueN,△}的AbsValue和FieldVar的大小和sr的一样，则s'口ADGI。 证明概述G上访问路径集用AccessPath表示，IGD用State表示。则求访问路径u所 代表指针的值的函数GetAbsValue:AccessPath×State→AbsValuefN,△}的定义如下： GetAbsValueu(sd,sf)=sdu), 若u是声明变量 Get4bs'alue u☐sa,s)=sy(Get4 bsValuev(sa,s,next),若u是v->next的形式 8

8 （4）若边指向谓词节点，则边的含义在展开谓词节点后的形状图上确定。 再定义形状图的语义。对于非 NULL 且非悬空的指针，认为它的值就是它所指向堆块 的抽象地址，对应地，动态分配的各堆块的地址是各不相同的抽象值。再认为栈和各堆块上 的存储单元分别按声明指针和域指针的名字访问。机器的抽象状态（以下简称机器状态）就 可由两个函数：sd : DecVar  AbsValue{,}和 sf : AbsValue  FieldVar  AbsValue{,} 构成，其中 sd 的定义域是声明指针集，它给出声明指针的抽象值。AbsValue 是堆块抽象地 址集，FieldVar 是域指针名字集，sf 给出程序能访问到的各堆块的域指针的抽象值，和是 两个特殊的抽象值。下面用 s 或sd, sf表示机器状态。 在此简化下，基于先前节点和边的含义，一个没有浓缩节点和谓词节点的形状图 G 则 是某个机器状态的图形表示，而一般的形状图则是某个机器状态集的图形表示。 定义 4 形状图 G 所代表的机器状态集￾G￾由下面几条规则定义。 （1）若 G 无浓缩节点和谓词节点，则￾G￾中只有一个状态。G 直接体现该状态，其中 所有声明节点及其出边的指向构成函数 sd，各结构节点及其出边的指向构成函数 sf。 （2）G 有带 e 和 a 的浓缩节点。若 a 蕴涵 e 可等于 k 个值，这 k 种情况下浓缩节点完 全展开后的形状图分别是 G1,…, Gk，则￾G￾ = ￾G1￾  …  ￾Gk￾；若 a 蕴涵 e 可等于 0, 1,…，浓缩节点完全展开成 n 个结构节点（n  0）的形状图是 Gn，则￾G￾ = ￾G0￾  ￾G1￾  …。 （3）若 G 有谓词节点，且谓词节点展开后的形状图是 G或 G1G2，则￾G￾ = ￾G￾ 或￾G￾ = ￾G1￾  ￾G2￾。 很容易进一步定义形状图 G1  G2  … Gn 的语义。 形状图上的路径描述采用和程序中访问路径同样的语法形式，以利于讨论两者之间的对 应。显然，只需要考虑从声明节点开始到达某个节点的路径，分成下面两种情况。 （1）路径的完全表示。若路径最多到达浓缩节点，则由依次列出路径各边上的标记来 表示该路径。若边上的标记依次为 p, l, r，则写成 p->l->r。 （2）路径的浓缩表示。若路径包括带 e 和 a 的浓缩节点的出边 l，则路径需使用上角标 来表示重复次数。例如在图 2(b)中，有 head(->next)m和 head(->next)m->next 等路径。 显然，形状图上一条路径的最后一条边上的标记所代表的程序指针，与程序中表示这个 指针的访问路径一致，以下统称它们为访问路径。 形状图是程序中指针有效性断言和指针相等断言等的图形表示。 定义 5 形状图 G 所表示的断言集￾G￾由下面这些有关指针的断言组成： （1）指向结构节点的指针都是有效指针，指向 null 节点或悬空节点的指针都是无效指 针。 （2）指向同一个结构节点或谓词节点的指针相等，指向浓缩节点展开后的同一个结构 节点的指针相等，例如图 2(b)表示的断言中有 head(->next)m->next == ptr； （3）指向 null 节点（悬空节点）的指针都等于 NULL（是悬空指针）； （4）指向谓词节点的指针都满足相应的谓词。 基于这个断言集，可以知道哪些指针不相等，可以推导哪些访问路径互为别名。 定理 1 对任何形状图 G，￾G￾的状态都满足￾G￾的所有断言，写成s:￾G￾. s￾￾G￾。 并且对任何 s￾G￾，若 dom(sd) = dom(sd)（s￾G￾）且二元函数 sf : AbsValue  FieldVar  AbsValue{,}的 AbsValue 和 FieldVar 的大小和 sf的一样，则 s￾￾G￾。 证明概述 G 上访问路径集用 AccessPath 表示，￾G￾用 State 表示。则求访问路径 u 所 代表指针的值的函数 GetAbsValue : AccessPath  State  AbsValue{,}的定义如下： GetAbsValue￾u￾sd, sf = sd(u)， 若 u 是声明变量 GetAbsValue￾u￾sd, sf = sf (GetAbsValue￾v￾sd, sf, next)，若 u 是 v->next 的形式