形状图逻辑和形状系统 (中国科学技术大学计算机科学与技术学院，安徽合肥230026) (中国科学技术大学苏州研究院软件安全实验室，江苏苏州215123) 摘要：指针程序的分析和验证一直是个难题，本文用形状图逻辑和形状系统来解决其中的困难，并 采取先用形状分析构建各程序点的形状图，再借助形状图进行其它性质验证的两阶段方式完成指针程序的 验证。所实现的系统原型可自动验证使用splay tree,treap,AVL tree和AAtree等数据结构的程序。 本文提出一种直接把形状图作为程序中指针断言的形状图逻辑。它是Hoare逻辑的一种扩展，可用于 对操作易变数据结构的指针程序的分析和验证。用形状图表示指针断言的好处是，便于程序验证阶段获取 所需的指针信息。其次，提出形状系统概念。它要求程序员在声明含自引用的结构体类型时，指明其指针 域参与构建的数据结构的形状，在形状分析阶段的形状检查据此排除所构建的形状偏离程序员期望的程序。 其好处是可免去程序员为程序验证提供有关指针的函数前后条件和循环不变式。此外，还提出利用形状图 来消除访问路径别名，让程序验证阶段对形状以外性质的验证仍用Hoar©逻辑的规则进行推理的方法。该 方法使得程序验证阶段生成的验证条件仍可以用通常的定理证明器来证明。 关键词：形状图逻辑、形状系统、程序验证、形状分析、指针逻辑 1、引言 随着国家、社会和日常生活对软件系统的依赖程度日益增长，复杂软件系统的正确、安 全（包括safety和security)和可靠等对安全攸关的基础设施和应用是至关重要的。安全攸 关软件的高可信成了保障国家安全、保持经济可持续发展和维护社会稳定的必要条件。 形式验证是提高软件可信程度的重要方法。粗略地说，软件的形式验证有两种途径。 The first approach is model checking,which consists of a systematically exhaustive exploration of the mathematical model。模型检测方法已经在工业界逐步得到应用。The second approach is logical inference.It consists of using a formal version of mathematical reasoning about software systems,usually using theorem proving software such as Isabelle/HOL[1]or Coq[2]theorem provers.在这种途径中，大部分的研究围绕采用某种演算来产生验证条件，然后用某个定理 证明器来证明验证条件，如Ynot[3引、Spec#[4]和ESC/Java[5]。有些研究依靠符号计算及其 过程中的定理证明来避免验证条件生成步骤，如smallfoot6]和jStar[7]。还有的研究采用经 严格证明的变换，从抽象规范逐步求精得到具体程序，如Perfect Developer[8]。虽然这些工 具己在实验室研发出来，但是尚无可供工业界使用的产品问世。究其原因，根源在于自动定 理证明方面的困难。因为不管是验证条件的证明、循环不变式的推断、访问路径（访问堆变 量的表达式)的别名判断、断言语言的表达能力和领域专用逻辑的设计等，最终都受到自动 定理证明器的能力的影响。 在研究自动定理证明技术的同时，也应该考虑怎样降低对自动定理证明器的能力的期 望。例如，设计新的编程语言机制来提高合法程序的门槛，以排除部分有逻辑错误的程序。 还有，采用程序分析方法来收集程序信息，用所得信息来支持程序验证。这些都有可能减轻 自动定理证明器的负担。本文介绍在指针程序验证方法的研究中，我们采用先形状分析，后 程序验证所取得的进展。 第一，提出一种把形状图直接作为指针相等断言集以及指针有效性断言集的方法，并基 1
1 形状图逻辑和形状系统 (中国科学技术大学 计算机科学与技术学院，安徽 合肥 230026 ) (中国科学技术大学 苏州研究院软件安全实验室，江苏 苏州 215123) 摘要：指针程序的分析和验证一直是个难题，本文用形状图逻辑和形状系统来解决其中的困难，并 采取先用形状分析构建各程序点的形状图，再借助形状图进行其它性质验证的两阶段方式完成指针程序的 验证。所实现的系统原型可自动验证使用 splay tree, treap, AVL tree 和 AA tree 等数据结构的程序。 本文提出一种直接把形状图作为程序中指针断言的形状图逻辑。它是 Hoare 逻辑的一种扩展，可用于 对操作易变数据结构的指针程序的分析和验证。用形状图表示指针断言的好处是，便于程序验证阶段获取 所需的指针信息。其次，提出形状系统概念。它要求程序员在声明含自引用的结构体类型时，指明其指针 域参与构建的数据结构的形状，在形状分析阶段的形状检查据此排除所构建的形状偏离程序员期望的程序。 其好处是可免去程序员为程序验证提供有关指针的函数前后条件和循环不变式。此外，还提出利用形状图 来消除访问路径别名，让程序验证阶段对形状以外性质的验证仍用 Hoare 逻辑的规则进行推理的方法。该 方法使得程序验证阶段生成的验证条件仍可以用通常的定理证明器来证明。 关键词： 形状图逻辑、形状系统、程序验证、形状分析、指针逻辑 1、引言 随着国家、社会和日常生活对软件系统的依赖程度日益增长，复杂软件系统的正确、安 全（包括 safety 和 security）和可靠等对安全攸关的基础设施和应用是至关重要的。安全攸 关软件的高可信成了保障国家安全、保持经济可持续发展和维护社会稳定的必要条件。 形式验证是提高软件可信程度的重要方法。粗略地说，软件的形式验证有两种途径。 The first approach is model checking, which consists of a systematically exhaustive exploration of the mathematical model。模型检测方法已经在工业界逐步得到应用。The second approach is logical inference. It consists of using a formal version of mathematical reasoning about software systems, usually using theorem proving software such as Isabelle/HOL[1] or Coq[2] theorem provers. 在这种途径中，大部分的研究围绕采用某种演算来产生验证条件，然后用某个定理 证明器来证明验证条件，如 Ynot[3]、Spec#[4]和 ESC/Java[5]。有些研究依靠符号计算及其 过程中的定理证明来避免验证条件生成步骤，如 smallfoot[6]和 jStar[7]。还有的研究采用经 严格证明的变换，从抽象规范逐步求精得到具体程序，如 Perfect Developer[8]。虽然这些工 具已在实验室研发出来，但是尚无可供工业界使用的产品问世。究其原因，根源在于自动定 理证明方面的困难。因为不管是验证条件的证明、循环不变式的推断、访问路径（访问堆变 量的表达式）的别名判断、断言语言的表达能力和领域专用逻辑的设计等，最终都受到自动 定理证明器的能力的影响。 在研究自动定理证明技术的同时，也应该考虑怎样降低对自动定理证明器的能力的期 望。例如，设计新的编程语言机制来提高合法程序的门槛，以排除部分有逻辑错误的程序。 还有，采用程序分析方法来收集程序信息，用所得信息来支持程序验证。这些都有可能减轻 自动定理证明器的负担。本文介绍在指针程序验证方法的研究中，我们采用先形状分析，后 程序验证所取得的进展。 第一，提出一种把形状图直接作为指针相等断言集以及指针有效性断言集的方法，并基
于此设计出形状图逻辑。形状图逻辑是Hoare逻辑的一种扩展，主要增加了对指针操作语句 的推理规则。该逻辑可用于操作易变数据结构的指针程序的分析和验证。 基于对指针算术运算和取地址运算(&)等的限制，本文的形状图可以精确表达相应程 序点指针（包括静态声明的指针和动态分配的结构体变量中的域指针）之间的相等关系和各 指针有效与否（有指向对象的指针称为有效指针），并可用来查询访问路径的别名等。在形 状分析和程序验证两阶段都把形状图看成图形表示的指针相等断言集，并都用形状图逻辑来 进行推理。形状分析阶段主要用其中指针操作语句的规则来构建各程序点的形状图：程序验 证阶段则利用形状图提供的信息来验证形状以外的其他程序性质，如二叉树的有序性。可以 说，这是把指针性质的证明从程序验证中剥离出来，先行在形状分析阶段完成。两个阶段都 采用形状图逻辑有利于整个程序逻辑的可靠性的证明。 用形状图作为指针相等断言的好处是，便于分析时从指针操作语句之前的指针断言集获 得其后的指针断言集，也便于程序验证时获取所需的指针信息。例如，指向节点的指针是否 多于1个（用于防止内存泄漏），2条访问路径是否互为别名（用于消除访问路径别名）。 第二，提出形状系统概念，粗略地说它类似于类型系统。本文为一个类C小语言PointerC 设计一种形状系统，它包括所允许构建的形状及其严格定义、形状推断规则和形状检查规则。 形状系统要求程序员声明含自引用的结构体类型（指其中有这样的域：它们的类型是该结构 体类型的指针类型)参与构建的形状。形状分析阶段利用形状推断规则来推断各结构体变量 链接成的形状，并依据形状检查规则来判断在被关注的程序点，所推断出的形状与程序员的 声明是否一致，由此拒绝没有构造出（或操作在）程序员所声明形状的程序，减少分析和验 证要应付的情况。 形状系统带来的明显好处是，免去程序员为程序验证提供作为函数前后条件和循环不变 式一部分的函数前后形状图和循环不变形状图。由此，用形状图作为指针相等断言不会给程 序员添加麻烦。 第三，提出利用形状图来消除访问路径别名，使形状以外性质的验证仍可用Hoare逻辑 的规则进行推理的方法。Hoare逻辑的一个重要局限是程序中不同的名字（包括访问路径） 必须代表不同的程序对象，即不允许出现别名。倘若能够保证在使用Hoar爬逻辑的赋值公理 时，所涉及的语句和断言中没有别名，则该规则的使用是可靠的。在程序验证阶段，形状图 被用来作为判断和消除访问路径别名的依据，先消除别名，然后再用赋值公理。 这种做的好处是，避免像Hor逻辑的某些扩展（如分离逻辑）那样需要专门的定理证 明器来证明验证条件。 第四，实现了一个指针程序验证系统的原型。该原型可以验证易变数据结构上较为复杂 的程序，如sorted circular doubly--linked list,binary search tree,.splay tree,treap,AVL tree和 AA tree的插入和删除函数。 本文组织如下。第2节介绍形状图并把形状图看成断言，第3节介绍形状图逻辑，第4 节介绍形状系统。第5节介绍为PointerC语言开发的程序验证系统的原型。第6节和相关 研究工作进行比较。第7节是总结。 2、形状图作为指针断言 形状图是描述程序中静态声明的指针型变量（简称声明指针）和动态分配的结构体中指 针型域变量（简称域指针）的指向的一种有向图，它不仅准确地表达了指针之间的相等关系， 还可用来判断访问路径的别名等。 本节主要定义形状图及其语义，并把形状图看成有关指针的断言。 2.1形状图的语法 和图论中的有向图不一样，形状图的顶点有六种形式，见图1。它们主要用来表示程序 2
2 于此设计出形状图逻辑。形状图逻辑是 Hoare 逻辑的一种扩展，主要增加了对指针操作语句 的推理规则。该逻辑可用于操作易变数据结构的指针程序的分析和验证。 基于对指针算术运算和取地址运算（&）等的限制，本文的形状图可以精确表达相应程 序点指针（包括静态声明的指针和动态分配的结构体变量中的域指针）之间的相等关系和各 指针有效与否（有指向对象的指针称为有效指针），并可用来查询访问路径的别名等。在形 状分析和程序验证两阶段都把形状图看成图形表示的指针相等断言集，并都用形状图逻辑来 进行推理。形状分析阶段主要用其中指针操作语句的规则来构建各程序点的形状图；程序验 证阶段则利用形状图提供的信息来验证形状以外的其他程序性质，如二叉树的有序性。可以 说，这是把指针性质的证明从程序验证中剥离出来，先行在形状分析阶段完成。两个阶段都 采用形状图逻辑有利于整个程序逻辑的可靠性的证明。 用形状图作为指针相等断言的好处是，便于分析时从指针操作语句之前的指针断言集获 得其后的指针断言集，也便于程序验证时获取所需的指针信息。例如，指向节点的指针是否 多于 1 个（用于防止内存泄漏），2 条访问路径是否互为别名（用于消除访问路径别名）。 第二，提出形状系统概念，粗略地说它类似于类型系统。本文为一个类 C 小语言 PointerC 设计一种形状系统，它包括所允许构建的形状及其严格定义、形状推断规则和形状检查规则。 形状系统要求程序员声明含自引用的结构体类型（指其中有这样的域：它们的类型是该结构 体类型的指针类型）参与构建的形状。形状分析阶段利用形状推断规则来推断各结构体变量 链接成的形状，并依据形状检查规则来判断在被关注的程序点，所推断出的形状与程序员的 声明是否一致，由此拒绝没有构造出（或操作在）程序员所声明形状的程序，减少分析和验 证要应付的情况。 形状系统带来的明显好处是，免去程序员为程序验证提供作为函数前后条件和循环不变 式一部分的函数前后形状图和循环不变形状图。由此，用形状图作为指针相等断言不会给程 序员添加麻烦。 第三，提出利用形状图来消除访问路径别名，使形状以外性质的验证仍可用 Hoare 逻辑 的规则进行推理的方法。Hoare 逻辑的一个重要局限是程序中不同的名字（包括访问路径） 必须代表不同的程序对象，即不允许出现别名。倘若能够保证在使用 Hoare 逻辑的赋值公理 时，所涉及的语句和断言中没有别名，则该规则的使用是可靠的。在程序验证阶段，形状图 被用来作为判断和消除访问路径别名的依据，先消除别名，然后再用赋值公理。 这种做的好处是，避免像 Hoare 逻辑的某些扩展（如分离逻辑）那样需要专门的定理证 明器来证明验证条件。 第四，实现了一个指针程序验证系统的原型。该原型可以验证易变数据结构上较为复杂 的程序，如 sorted circular doubly-linked list, binary search tree, splay tree, treap, AVL tree 和 AA tree 的插入和删除函数。 本文组织如下。第 2 节介绍形状图并把形状图看成断言，第 3 节介绍形状图逻辑，第 4 节介绍形状系统。第 5 节介绍为 PointerC 语言开发的程序验证系统的原型。第 6 节和相关 研究工作进行比较。第 7 节是总结。 2、形状图作为指针断言 形状图是描述程序中静态声明的指针型变量（简称声明指针）和动态分配的结构体中指 针型域变量（简称域指针）的指向的一种有向图，它不仅准确地表达了指针之间的相等关系， 还可用来判断访问路径的别名等。 本节主要定义形状图及其语义，并把形状图看成有关指针的断言。 2.1 形状图的语法 和图论中的有向图不一样，形状图的顶点有六种形式，见图 1。它们主要用来表示程序
操作的栈单元或堆块，在此称为节点。下面是六种节点的名称和语法。 (1)声明节点：圆节点。 (2)结构节点：矩形节点。 (3)u山节点：虚线边框的矩形节点，中间含字母N。 (4)悬空节点：虚线边框的矩形节点，中间含字母△。 (5)浓缩节点：灰色矩形节点，下侧有表达式e以及约束e取值范围的断言a。e是仅 使用常量和变量的整型线性表达式，a是这类表达式的关系运算的逻辑合取式。若灰色矩形 下无e和a,称为无约束浓缩节点，它表示被浓缩的结构节点个数任意，可以是0个。 (6)谓词节点：矩形节点，中间含字母n,节点下侧有作为谓词名字的标识符name, 还有与浓缩节点中一致的表达式e和断言a。 O e.a name,e,a 声明节点结构节点ul节点悬空节点浓缩节点谓词节点 图1形状图的各种节点 形状图的有向边上都有标识符作为其标记。有向边及其连接的节点满足如下语法约束。 (1)声明节点：只有唯一的出边，没有入边。 (2)结构节点和浓缩节点：有入边和出边，各出边的标记不相同。 (3)ul节点、悬空节点和谓词节点：有入边，没有出边。 定义1(1)节点和有向边满足上述语法约束，各声明节点出边标记相异，且边被视为 无向时则连通的图形(diagram)是形状图。 (2)若形状图G1,G2,,G的声明节点出边标记集两两相交都为空，则由逻辑合取符 号A连接的G1AG2A.入Gm也是形状图。 (3)若形状图G1,G2,,Gn的声明节点出边标记集都相同，则逻辑析取符号V连接的 G1VGV..VGm也是形状图。 本文中符号G仅用来表示不含符号V的形状图，并且不含符号入的形状图G被称为形状 子图。在介绍形状图语义时可知，在G八G2中，G1和G2各代表程序状态的不同部分，而在 G1vG2中，G和G2代表不同的程序状态。 受编程语言类型系统的约束，本文涉及的形状图只是定义1确立的形状图集的子集，因 为类型系统保证源于不同结构体类型的结构节点在形状图上不会相邻。 图2是两个表示单向链表的形状图。在讨论形状图的语义后会知道，下面程序片段（假 定head指向的单向链表至少有一个表元) ptrl head;ptr head->next; while(ptr !NULL) ptrl ptr;ptr ptr->next; 的循环不变特性由图2(a)概括，其中head和ptr所指向的浓缩节点分别代表m和n(m,n≥0) 个表元。由此可知，浓缩节点的e代表被浓缩的结构节点的个数：指向ul节点的有向边是 NULL指针。在循环体中第1个语句之前的程序点，单向链表的特点由图2b)概括。 ptrl ○eagr vptr next next next (a) (b 图2形状图的两个例子 3
3 操作的栈单元或堆块，在此称为节点。下面是六种节点的名称和语法。 （1）声明节点：圆节点。 （2）结构节点：矩形节点。 （3）null 节点：虚线边框的矩形节点，中间含字母。 （4）悬空节点：虚线边框的矩形节点，中间含字母。 （5）浓缩节点：灰色矩形节点，下侧有表达式 e 以及约束 e 取值范围的断言 a。e 是仅 使用常量和变量的整型线性表达式，a 是这类表达式的关系运算的逻辑合取式。若灰色矩形 下无 e 和 a，称为无约束浓缩节点，它表示被浓缩的结构节点个数任意，可以是 0 个。 （6）谓词节点：矩形节点，中间含字母，节点下侧有作为谓词名字的标识符 name， 还有与浓缩节点中一致的表达式 e 和断言 a。 形状图的有向边上都有标识符作为其标记。有向边及其连接的节点满足如下语法约束。 （1）声明节点：只有唯一的出边，没有入边。 （2）结构节点和浓缩节点：有入边和出边，各出边的标记不相同。 （3）null 节点、悬空节点和谓词节点：有入边，没有出边。 定义 1 （1）节点和有向边满足上述语法约束，各声明节点出边标记相异，且边被视为 无向时则连通的图形（diagram）是形状图。 （2）若形状图 G1, G2, …, Gn 的声明节点出边标记集两两相交都为空，则由逻辑合取符 号连接的 G1 G2 … Gn 也是形状图。 （3）若形状图 G1, G2, …, Gn 的声明节点出边标记集都相同，则逻辑析取符号连接的 G1 G2 … Gn 也是形状图。 本文中符号 G 仅用来表示不含符号的形状图，并且不含符号的形状图 G 被称为形状 子图。在介绍形状图语义时可知，在 G1G2 中，G1 和 G2 各代表程序状态的不同部分，而在 G1G2 中，G1 和 G2 代表不同的程序状态。 受编程语言类型系统的约束，本文涉及的形状图只是定义 1 确立的形状图集的子集，因 为类型系统保证源于不同结构体类型的结构节点在形状图上不会相邻。 图 2 是两个表示单向链表的形状图。在讨论形状图的语义后会知道，下面程序片段（假 定 head 指向的单向链表至少有一个表元） ptr1 = head; ptr = head->next; while (ptr != NULL) { ptr1 = ptr; ptr = ptr->next; } 的循环不变特性由图 2(a)概括，其中 head 和 ptr 所指向的浓缩节点分别代表 m 和 n（m, n 0） 个表元。由此可知，浓缩节点的 e 代表被浓缩的结构节点的个数；指向 null 节点的有向边是 NULL 指针。在循环体中第 1 个语句之前的程序点，单向链表的特点由图 2(b)概括。 图 2 形状图的两个例子 (b) head next next ptr next ptr1 head next next ptr next ptr1 next (a) 图 1 形状图的各种节点 声明节点 结构节点 null 节点 悬空节点 浓缩节点 e, a 谓词节点 name, e, a
2.2数据结构的形状图 图3给出基于形状图定义的单链表（包括单向链表和循环单向链表）、双链表（包括双 向链表和循环双向链表)和二叉树，其中最左边的dist(s,e,a)等符号表示是为了便于在文中 的引用。在这些形状图中，边上的标记都是占位符，可根据程序的需要来选择名字。 可以看出，把dist(s,e,a)的2个定义中的e和a部分略去，再用符号v连接它们，就得 到dist(s)的定义。为节约篇幅，Iist(s)、c list((s)和c dlist(s)定义的形状图没有在图3列出。 单向链表 list(s,e,a) list,e,a (1) e,a nt 循环单向链表 Gs> Π0 c list(s,e,a) c list,e,a (2) e,a 双向链表 G>加G>w dlist(s,e,a) G回加C dlist,e,a dlist,e,a a→(e=0)(3) a→(e>-1)(4) 双向链表 dlist(s) dlist 8C0 (5) 循环双向链表 c dlist(s,e,a) G>回加Gw G回G2☑ c dlist,e,a c dlist,e,a Ae-1 a a-(e=0)(6) a(e>=l)(7) 二叉树 n tree(s) G回加G>vG tree tree (8) tree 图3各种形状谓词的定义 定义2图3定义式（包括因篇幅限制未列出的定义式）左右两边出现的形状子图，都 称为数据结构最简(minimal)形状图。 2.3形状图的变换规则 在给出变换规则之前，需先定义窗口，它描述形状子图上被关注的那部分。 定义3一个形状图的某子图上用点划线方框明示并满足下面条件的部分称为窗口，形 状图的其余部分称为窗口的上下文。窗口需要满足的条件如下： (1)形状图的各节点处于窗口或上下文中，不得与窗口的方框边界相交。 (2)窗口内各节点之间的边都处于窗口中：表达窗口中节点与上下文中节点联系的穿 越方框边界的边属于窗口，它们的一份拷贝在上下文中。 窗口W和上下文G]的匹配就是检查穿越W边界的边和G]中的拷贝边能否重合，重 合后得到的形状图用G[门表示。 在下述规则中出现的窗口有这样一种缩写：若要求从窗口外指向窗口内某节点至少要有 一条边（如图4的p1),则可能还有的其他边（可以是0条）用一条标记为p的边统一表示。 4
4 2.2 数据结构的形状图 图 3 给出基于形状图定义的单链表（包括单向链表和循环单向链表）、双链表（包括双 向链表和循环双向链表）和二叉树，其中最左边的 dlist(s, e, a)等符号表示是为了便于在文中 的引用。在这些形状图中，边上的标记都是占位符，可根据程序的需要来选择名字。 可以看出，把 dlist(s, e, a)的 2 个定义中的 e 和 a 部分略去，再用符号连接它们，就得 到 dlist(s)的定义。为节约篇幅，list(s)、c_list(s)和 c_dlist(s)定义的形状图没有在图 3 列出。 定义 2 图 3 定义式（包括因篇幅限制未列出的定义式）左右两边出现的形状子图，都 称为数据结构最简（minimal）形状图。 2.3 形状图的变换规则 在给出变换规则之前，需先定义窗口，它描述形状子图上被关注的那部分。 定义 3 一个形状图的某子图上用点划线方框明示并满足下面条件的部分称为窗口，形 状图的其余部分称为窗口的上下文。窗口需要满足的条件如下： （1）形状图的各节点处于窗口或上下文中，不得与窗口的方框边界相交。 （2）窗口内各节点之间的边都处于窗口中；表达窗口中节点与上下文中节点联系的穿 越方框边界的边属于窗口，它们的一份拷贝在上下文中。 窗口 W 和上下文 G[ ]的匹配就是检查穿越 W 边界的边和 G[ ]中的拷贝边能否重合，重 合后得到的形状图用 G[W]表示。 在下述规则中出现的窗口有这样一种缩写：若要求从窗口外指向窗口内某节点至少要有 一条边（如图 4 的 p1），则可能还有的其他边（可以是 0 条）用一条标记为 pk 的边统一表示。 二叉树 tree(s) s tree r tree l s s tree 图 3 各种形状谓词的定义 单向链表 list(s, e, a) e, a s nt s list, e, a 双向链表 dlist(s) s s dlist r r l l s 循环单向链表 c_list(s, e, a) s c_list, e, a e, a s nt 双向链表 dlist(s, e, a) s dlist, e, a s a (e == 0) a (e>=1) e-1, a r r l l s s dlist, e, a 循环双向链表 c_dlist(s, e, a) s a (e == 0) s c_dlist, e, a a (e>=1) r l l s e-1, a r s c_dlist, e, a (8) (6) (7) (5) (4) (3) (2) (1)
下面首先介绍等价变换规则，它们用来表示保持语义等价的形状图变换规则。语义等价 性在定义形状图的语义后证明。 1、单链表的等价规则 (1)基本规则 ·基于单链表谓词定义的规则。例如，由图3的1ist(s,e,a)定义得到的规则见图4的规 则(1) ·添加或取消e=0的浓缩节点的规则。例如，图4的规则(2)和(3)。针对规则(2)，把规 则(2)右部窗口中的浓缩节点和结构节点交换一下位置，也是一条规则。另外，把该规则中 的结构节点改成谓词、ul或悬空节点（它们都没有nt出边），结果也是规则。 ·e>0的浓缩节点的展开和折叠规则。例如，图4的规则(4)。把规则(4)右部窗口中的 浓缩节点和结构节点交换一下位置，也是一条规则。 ·无约束浓缩节点的展开与折叠规则。例如图4的规则(5)和(6)。规则（⑤）针对由一个无 约束浓缩节点构成的循环单向链表。规则(6)右部第1个窗口中的结构节点和浓缩节点交换 一下位置，结果也是一条规则。仿照规则(6)可以得到浓缩节点右边是其他节点的规则。 ·谓词节点的展开与折叠规则。图4的规则(7)和(8)是这种规则。 list,e,a e.a e.a (1) a(e==0)(2) nt p1-- e,a e-1.a 三(e=0)(3) a→(e>=l) 4 一一1 nt ▣nt (5 (6) list,e,a list,e,a list,e-1,a a→(e=0)(7) a→(e>=l)(8) 图4单链表的部分等价规则 (2)导出规则 ·分别带e1与a1和e2与a2的两个相邻浓缩节点等价于一个带e1+e2与a1Aa2的浓缩节点 的规则，两个相邻的无约束浓缩节点等价于一个无约束浓缩节点的规则。 ·单个结构节点等价于带1与tu的浓缩节点的规则。 ·可以作为list(s,e,a)谓词另一种归纳定义的规则。将图4规则(7和(8)的右部用析取符 号链接并略去多余的pk及相应边，可作为ist(s,e,a)定义的右部。list(s)也有类似的规则。 2、双链表的等价规则 (1)基本规则 5
5 下面首先介绍等价变换规则，它们用来表示保持语义等价的形状图变换规则。语义等价 性在定义形状图的语义后证明。 1、单链表的等价规则 （1）基本规则 基于单链表谓词定义的规则。例如，由图 3 的 list(s, e, a)定义得到的规则见图 4 的规 则(1)。 添加或取消 e = 0 的浓缩节点的规则。例如，图 4 的规则(2)和(3)。针对规则(2)，把规 则(2)右部窗口中的浓缩节点和结构节点交换一下位置，也是一条规则。另外，把该规则中 的结构节点改成谓词、null 或悬空节点（它们都没有 nt 出边），结果也是规则。 e > 0 的浓缩节点的展开和折叠规则。例如，图 4 的规则(4)。把规则(4)右部窗口中的 浓缩节点和结构节点交换一下位置，也是一条规则。 无约束浓缩节点的展开与折叠规则。例如图 4 的规则(5)和(6)。规则(5)针对由一个无 约束浓缩节点构成的循环单向链表。规则(6)右部第 1 个窗口中的结构节点和浓缩节点交换 一下位置，结果也是一条规则。仿照规则(6)可以得到浓缩节点右边是其他节点的规则。 谓词节点的展开与折叠规则。图 4 的规则(7)和(8)是这种规则。 （2）导出规则 分别带 e1与 a1 和 e2 与 a2 的两个相邻浓缩节点等价于一个带 e1+e2 与 a1a2 的浓缩节点 的规则，两个相邻的无约束浓缩节点等价于一个无约束浓缩节点的规则。 单个结构节点等价于带 1 与 true 的浓缩节点的规则。 可以作为 list(s, e, a)谓词另一种归纳定义的规则。将图 4 规则(7)和(8)的右部用析取符 号链接并略去多余的 pk及相应边，可作为 list(s, e, a)定义的右部。list(s)也有类似的规则。 2、双链表的等价规则 （1）基本规则 图 4 单链表的部分等价规则 a (e == 0) e, a p1 pk nt nt p1 pk nt list, e, a p1 pk e, a nt p1 pk (1) (2) e, a p1 pk nt e-1, a p1 pk nt nt a (e >=1) (4) e, a nt p1 pk a (e == 0) (3) p1 pk nt p1 pk nt nt p1 pk (5) p1 pk nt p1 pk list, e-1, a list, e, a p1 pk a (e== 0) (7) a (e>=1) (8) list, e, a p1 pk p1 pk p1 pk nt p1 pk nt nt (6) p1 pk