形状图逻辑和形状系统 Shape graph logic and shape system.pdf_大学文库

形状图逻辑和形状系统 (中国科学技术大学计算机科学与技术学院，安徽合肥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 被称为形状子图。在介绍形状图语义时可知，在 G1G2 中，G1 和 G2 各代表程序状态的不同部分，而在 G1G2 中，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)

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 与 a1a2 的浓缩节点的规则，两个相邻的无约束浓缩节点等价于一个无约束浓缩节点的规则。  单个结构节点等价于带 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 

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)

(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{,}的定义如下： GetAbsValueusd, sf = sd(u)，若 u 是声明变量 GetAbsValueusd, sf = sf (GetAbsValuevsd, sf, next)，若 u 是 v->next 的形式

显然，指向一个节点的u∈AccessPath的值就是该节点所代表堆块的抽象地址或者属于 {N,△}，指向同一个节点的u,vEAccessPath的抽象值相同。因此，对不含浓缩节点和谓词节点的G,定理1成立。仿照定义4的步骤进行归纳证明，可将定理1扩大到一般的G。定理2若使用等价变换规则可得G一G或者G台G1vG2,那么DGD=四GD或者 IGD=IG0UIG0,并且对任何s:IGD,s☐ADGD当且仅当SOADGO或者s0ADGD当且仅当s☐A0G0或s0A0G0。若使用蕴涵变换规则，则把状态集的相等改成子集包含，把当且仅当改成蕴含。证明概要对每条形状图变换规则，依据定义4中对应的状态集构造规则来证明。例如，若由图4的规则(5)得到G一G1vG2,则根据定义4的规则(3)可以知道，加GD可以分成两个子集IG0UIGD,其中的状态分别满足A☐G0和ADG知。由定理2，当把形状图看成断言集合时，形状图的变换规则就是断言演算的等价规则或蕴涵规则。并且这些规则对所考虑的语义模型有效(valid)。由此，形状图可以作为程序断言，形状图之间的符号A和V分别是逻辑合取和析取连接词。通常使用析取范式G1VG2V.VGk来表示数据结构形状的不同情况。形状图之间的符号一和→分别可以看成逻辑等价和蕴涵连接词。 2.5形状图和符号断言之间的联系形状图是关于易变数据结构中的指针的断言，它们可以和符号断言一起进行演算。例如，条件语句的推理规则会使语句中布尔表达式u一NULL和u=v等(u和v都是指针型访问路径)和形状图形成合取，对它们需要有特殊的演算规则。这类断言若和形状图无矛盾则被忽略：有矛盾则否定形状图，连形状图一起的整个断言为假。图8(1)是一条这样的规则。 nt! ==NULL false e,a e,ana' (1) (2) 图8形状图和符号断言合取的部分规则同样，程序中出现约束©取值的断言a'时，需要把它加到相应浓缩节点的断言上。图 8(2)是一条这样的规则。若a八a'为假则整个断言为假。在图8(1)的规则中，放在边下方的山和k是访问路径而不是边的标记（边的标记在边的上方)，它们对使用该规则的要求与标记情况略有不同。把该规则中的窗口称为W,若对 G[仍使用该规则时，G[们要有到达W中节点的访问路径u。k同样表示访问路径。第3节的规则中出现在边下面的u和V,含义和这里的一样。这些规则对语义模型的有效性也不难证明。 2.6形状图和访问路径集合之间的联系在设计形状图逻辑之前，我们曾经设计过一种指针逻辑[21]。指针逻辑是一种符号化了的形状图逻辑。在这里先比较形状图和指针逻辑的访问路径集合。我们用循环双向链表插入函数中的一段代码以及程序点的形状图和访问路径集合来比较这两种逻辑。在图9中，对于p所指向的循环双向链表，在找到插入位置(q所指向节点的左邻)后，该段代码实施把s所指向节点插入链表的操作。n是链表长度(n≥0)，i是q 所指向节点之前的节点数。链表节点的类型是typedef struct node{Node*I;Node*r,..)Node。图9仅给出插在表中某位置(0r)2>l,表示p->r->r>l。 9

9 显然，指向一个节点的 uAccessPath 的值就是该节点所代表堆块的抽象地址或者属于 {,}，指向同一个节点的 u, vAccessPath 的抽象值相同。因此，对不含浓缩节点和谓词节点的 G，定理 1 成立。仿照定义 4 的步骤进行归纳证明，可将定理 1 扩大到一般的 G。定理 2 若使用等价变换规则可得 G  G或者 G  G1G2，那么G=G或者 G=G1G2，并且对任何 s:G，sG当且仅当 sG或者 sG当且仅当 sG1或 sG2。若使用蕴涵变换规则，则把状态集的相等改成子集包含，把当且仅当改成蕴含。证明概要对每条形状图变换规则，依据定义 4 中对应的状态集构造规则来证明。例如，若由图 4 的规则(5)得到 G  G1G2，则根据定义 4 的规则（3）可以知道，G可以分成两个子集G1  G2，其中的状态分别满足G1和G2。由定理 2，当把形状图看成断言集合时，形状图的变换规则就是断言演算的等价规则或蕴涵规则。并且这些规则对所考虑的语义模型有效（valid）。由此，形状图可以作为程序断言，形状图之间的符号和分别是逻辑合取和析取连接词。通常使用析取范式 G1 G2 … Gk来表示数据结构形状的不同情况。形状图之间的符号 和分别可以看成逻辑等价和蕴涵连接词。 2.5 形状图和符号断言之间的联系形状图是关于易变数据结构中的指针的断言，它们可以和符号断言一起进行演算。例如，条件语句的推理规则会使语句中布尔表达式 u==NULL 和 u!=v 等（u 和 v 都是指针型访问路径）和形状图形成合取，对它们需要有特殊的演算规则。这类断言若和形状图无矛盾则被忽略；有矛盾则否定形状图，连形状图一起的整个断言为假。图 8(1)是一条这样的规则。同样，程序中出现约束 e 取值的断言 a时，需要把它加到相应浓缩节点的断言上。图 8(2)是一条这样的规则。若 aa为假则整个断言为假。在图 8(1)的规则中，放在边下方的 u 和 uk 是访问路径而不是边的标记（边的标记在边的上方），它们对使用该规则的要求与标记情况略有不同。把该规则中的窗口称为 W，若对 G[W]使用该规则时，G[W]要有到达 W 中节点的访问路径 u。uk 同样表示访问路径。第 3 节的规则中出现在边下面的 u 和 v，含义和这里的一样。这些规则对语义模型的有效性也不难证明。 2.6 形状图和访问路径集合之间的联系在设计形状图逻辑之前，我们曾经设计过一种指针逻辑[21]。指针逻辑是一种符号化了的形状图逻辑。在这里先比较形状图和指针逻辑的访问路径集合。我们用循环双向链表插入函数中的一段代码以及程序点的形状图和访问路径集合来比较这两种逻辑。在图 9 中，对于 p 所指向的循环双向链表，在找到插入位置（q 所指向节点的左邻）后，该段代码实施把 s 所指向节点插入链表的操作。n 是链表长度（n  0），i 是 q 所指向节点之前的节点数。链表节点的类型是 typedef struct node{Node* l; Node* r;…}Node。图 9 仅给出插在表中某位置（0 r)2 ->l，表示p->r->r->l。图 8 形状图和符号断言合取的部分规则 e, a p1 pk nt  a  e, aa p1 pk nt  u==NULL  false u uk (1) (2)

(2)浓缩节点对应到若干个（由浓缩节点下的e和a确定）访问路径集合，它们可以用全称量词断言来概括。不过，对单向链表而言，当有多个指针指向被浓缩节点序列中的左边缘节点时，它对应的访问路径集合不能包括到全称量词断言中。 (3)所有NULL节点（悬空节点）对应到一个带下角标N的访问路径集合，所有指向 NULL节点（悬空节点）的有向边和该集合中的访问路径一一对应。 (4)没有与谓词节点对应的访问路径集合，但形状谓词对应到一个用访问路径集合来定义的谓词。例如图3中的二叉树定义对应到下面的定义： tree(s)s'Nv(s!tree(s->1)A tree(s->r)) (5)没有与声明节点对应的访问路径集合，因为没有指向声明节点的指针。显然，指向同一个节点（悬空节点除外）的指针都相等对应到同一个集合（带下角标D 的集合除外)中的访问路径所代表的指针都相等。访问路径集合也就是相等指针的集合。当有多条访问路径可表示一个指针时，指针逻辑取其中一条来代表该指针。这样，访问路径集合可以看成指针相等断言集合，因而也可以像形状图那样，对访问路径集合进行合取或析取。 2.3节的形状图变换规则在指针逻辑的断言语言中也都有对应的断言演算规则。例如，在被浓缩的边缘节点也能包括在带全称量词的断言中时，浓缩节点的展开和折叠规则对应到谓词逻辑中全称量词断言所囊括区间的展开和折叠规则。在指针逻辑中，对应图8(1)的规则如下： ∑1A.,A∑n-lA"ANA△Au=NULL→false 其中各个Σ是对应到各结构节点的访问路径集合，N和△分别是NULL指针集合和悬空指针集合。"表示u所在的指针集合，它相当于图8(1)规则的窗口。形状图指针集合 (p,p(->r)",p->r->I)Vk:1..i-1.(p(->r) p->r1>l}A{qp(->,p(>)1->}A k:i+1n-l.{p(->r',p(->r)l->}A{s}A n-i-1.i>0An>i (s->r,S->ID Ai>0A n>i s->=q->;q->>r=s,体下面仅给出1rr,p->r->l}(k:1.i-2.{p(->r}', p(->r)1>A{s->,p(>r,q->}A {p(->r以，s}A{s->r}D{q,q->r->l}A 1-2.1 n-i-1.i>1An>i Vk:i+1..n-1.(q(->r)ki,q(->r)it->1) i>lAn>i s->r=q;q->1=s; {p,q(->rP,p->r->}Ak:li-1.{p(->r)' G江 p->r)+1->}Λ{p(->r,q->l,s}A{s->L,q q->r->I)^Vk:i+I..n-1.(q(->r)ki, i-1.i>1 n-i-1,i>lAn>i q(->r)kitl>l)i>1n>i s=NULL:q=NULL:体下面是0≤i≤的各种情况都能满足的形状图和对应的访问路径集合*/ 9 {p,p(->r),p->r->l}k:ln{p(->r', N p(->r)>q SINAn>=0 n,n> 图9循环双向链表插入函数的部分代码和断言 0

10 （2）浓缩节点对应到若干个（由浓缩节点下的 e 和 a 确定）访问路径集合，它们可以用全称量词断言来概括。不过，对单向链表而言，当有多个指针指向被浓缩节点序列中的左边缘节点时，它对应的访问路径集合不能包括到全称量词断言中。（3）所有 NULL 节点（悬空节点）对应到一个带下角标 N 的访问路径集合，所有指向 NULL 节点（悬空节点）的有向边和该集合中的访问路径一一对应。（4）没有与谓词节点对应的访问路径集合，但形状谓词对应到一个用访问路径集合来定义的谓词。例如图 3 中的二叉树定义对应到下面的定义： tree(s) {s}N  ({s}  tree(s->l)  tree(s->r)) （5）没有与声明节点对应的访问路径集合，因为没有指向声明节点的指针。显然，指向同一个节点（悬空节点除外）的指针都相等对应到同一个集合（带下角标 D 的集合除外）中的访问路径所代表的指针都相等。访问路径集合也就是相等指针的集合。当有多条访问路径可表示一个指针时，指针逻辑取其中一条来代表该指针。这样，访问路径集合可以看成指针相等断言集合，因而也可以像形状图那样，对访问路径集合进行合取或析取。 2.3 节的形状图变换规则在指针逻辑的断言语言中也都有对应的断言演算规则。例如，在被浓缩的边缘节点也能包括在带全称量词的断言中时，浓缩节点的展开和折叠规则对应到谓词逻辑中全称量词断言所囊括区间的展开和折叠规则。在指针逻辑中，对应图 8(1)的规则如下： 1  …   n1  u     u == NULL  false 其中各个是对应到各结构节点的访问路径集合，和分别是 NULL 指针集合和悬空指针集合。u 表示 u 所在的指针集合，它相当于图 8(1)规则的窗口。图 9 循环双向链表插入函数的部分代码和断言 s->l = q->l; q->l->r = s; /*下面仅给出 1r = q; q->l = s; {p, p(->r)n, p->r->l}  k:1..i-1.{p(->r)k, p(->r)k+1->l}  {q, p(->r)i , p(->r)i+1->l}  k:i+1..n-1.{p(->r)k , p(->r)k+1->l}  {s}  {s->r, s->l}D  i > 0  n > i {p, q(->r)n-i, p->r->l}  (k:1..i-2.{p(->r)k , p(->r)k+1->l}  {s->l, p(->r)i-1, q->l}  {p(->r)i , s}  {s->r}D  {q, q->r->l}  k:i+1..n-1.{q(->r)k-i, q(->r)k-i+1->l}  i > 1  n > i  l p i-1, i>0 q r r r r l l l n-i-1,i>0 n>i  s r  l l p i-1, i>1 r r l q r r l l n-i-1, i>1 n>i s r l l p r  i-2, i>1 r l q r r l l n-i-1,i>1 n>i s r l r l {p, q(->r)n-i, p->r->l}  k:1..i-1.{p(->r)k , p(->r)k+1->l}  {p(->r)i , q->l, s}  {s->r, q, q->r->l}  k:i+1..n-1.{q(->r)k-i, q(->r)k-i+1->l}  i >1  n > i {p, p(->r)n+1, p->r->l}  k:1..n.{p(->r)k , p(->r)k+1  ->l}  {q, s}N  n >= 0 q  s  l p n, n>=0 r l r 