2472 计 算 机 学 报 2016年 (2)与形状有关的性质 (1)图16前一部分是自定义谓词以及这些谓 例如链表的长度、树的高度、二叉树的两边是否 词之间性质定理的语法，后一部分是断言的语法.谓 平衡和节点之间的可达性等.这些性质很容易归纳 词应用可出现在布尔表达式中，因而可出现在断 定义，虽然循环链表的长度的归纳定义会略显复杂 言中 (3)与各节点上数据排列有关的性质 (2)程序员用图16的文法编写的断言中出现 当数据需按序排列时，一个数据存放到哪个节 的变量，若不是程序变量，则称之为逻辑变量. 点依赖于对数据结构上节点的定序.线性链表上节 (3)量词约束变元的论域只能是整数域或它的 点之间的定序比较简单，二叉树上节点之间有多种 某个区间，因而禁止使用指针型约束变元.在需要由 定序方式.这样，数据是否有序的比较必定涉及数据 存在量词来约束指针型变元的地方，可以用指针型 所属节点在数据结构上的位置. 逻辑变量来代替. 在定义上述性质时，比较简单的方式是用以指 下面用有序单链表来解释为什么需要提供性质 针为参数（可能还有其他参数）的归纳谓词.另一种 定理.有序单链表的归纳定义如下： 方式是先定义节点之间的可达关系，然后基于此再使 SortedList(Node'p)△ 用量词来定义所需的性质.用这两种方式描述性质都 ==NULLV-nxt==NULLV 比较有利于对操作易变数据结构的递归程序的验证. p→d=p*nxt→d∧SortedList(p→nxt) 本文的系统原型针对形状图上浓缩节点的特 在一个子句中，若出现以p为前缀的访问路 点，还提供使用量词来概括数据性质的方式，以方便 径，则默认有断言p=NULL.SortedList的定义从 操作易变数据结构的循环程序的验证.例如有序单 表尾向表头方向归纳.但是，在遍历有序单链表时， 链表可定义为 例如图17单链表插入函数中的循环代码（暂且不关 SortedList(Node'p)△ 心图17中的断言)，其遍历方向是从表头向表尾，因 3m:N.((-nxt)"==NULLA 此还需要用下述表段谓词和性质定理， i:l.m-l.p(+nxt)-1→d<=p(+nxt)→d) SortedListSeg(Node'p,Node'g)A 其中Node类型由typedef struct node{intd;struct ==gAg!=NULLV node'nxt}Node给出，其中p(→nxt)代表p→nxt… p+d<=p-→nxt-→dN →nxt,共i个“→nxt”.在该定义中，量词的约束变 SortedListSeg(p->nxt,q) 元出现在访问路径的上角标中.这种直接基于编程 和 语言中访问路径语法的定义显得比较直观， SortedListSeg(p,q)∧q*d<=qnxt→d 5.2符号断言语言 台SortedListSeg(p,q→nxt) 为便于下面的讨论，将系统原型所使用的断言 这个性质定理保证已扫描过的表段再加入下一个被 语言的抽象语法描述在图16.几点说明如下： 扫描的节点，结果仍然是表段 SortedList和SortedListSeg两个谓词之间的 id∈Identifier(程序中的标识符集) tm∈Sidenti fier(程序中结构体类型的名字集) 如下性质定理也是验证时不可缺的： predicate definition SortedListSeg(p,q)∧SortedList(q)→ pd::=predicate id(pp..)=a predicate parameter SortedList(p) pp::=t id 上述2个性质定理都需要程序员提供，因为它们的 parameter type 证明需要基于表段的长度进行归纳，基于演绎推理 t:=intlin* property theorem 的自动定理证明器难以发现这样的性质， pt:=theorem a1→d2 theorem a1台az assertion(boolexp是布尔表达式，其产生式略去) SortedList谓词出现在函数的前后断言中，而 a::=boolerplYid:d.al3id:d.al(a) SortedListSeg谓词出现在循环不变式中，后者的定 domain(intexp是整型表达式，其产生式略去) d::=ZM N+interp1-interpz 义只要能支持函数前后条件的证明就足矣，没有必 l-value 要选择最一般的定义，即把被验证函数中不会出现 lo:=…|lv(→id)rp 的情况也囊括在内，以免给验证增添不必要的麻烦 (左值lw是各类型exp的一种选择) 在断言文法及其类型系统的基础上，还要限制 图16符号断言语言的抽象语法 断言中的整型表达式必须是线性表达式，（２）与形状有关的性质 例如链表的长度、树的高度、二叉树的两边是否 平衡和节点之间的可达性等．这些性质很容易归纳 定义，虽然循环链表的长度的归纳定义会略显复杂． （３）与各节点上数据排列有关的性质 当数据需按序排列时，一个数据存放到哪个节 点依赖于对数据结构上节点的定序．线性链表上节 点之间的定序比较简单，二叉树上节点之间有多种 定序方式．这样，数据是否有序的比较必定涉及数据 所属节点在数据结构上的位置． 在定义上述性质时，比较简单的方式是用以指 针为参数（可能还有其他参数）的归纳谓词．另一种 方式是先定义节点之间的可达关系，然后基于此再使 用量词来定义所需的性质．用这两种方式描述性质都 比较有利于对操作易变数据结构的递归程序的验证． 本文的系统原型针对形状图上浓缩节点的特 点，还提供使用量词来概括数据性质的方式，以方便 操作易变数据结构的循环程序的验证．例如有序单 链表可定义为 ＳｏｒｔｅｄＬｉｓｔ（Ｎｏｄｅ狆） 犿：&．（狆（→ｎｘｔ）犿＝＝ＮＵＬＬ∧ 犻：１．．犿－１．狆（→ｎｘｔ）犻－１→犱＜＝狆（→ｎｘｔ）犻→犱） 其中Ｎｏｄｅ类型由ｔｙｐｅｄｅｆｓｔｒｕｃｔｎｏｄｅ｛ｉｎｔ犱；ｓｔｒｕｃｔ ｎｏｄｅｎｘｔ｝Ｎｏｄｅ给出，其中狆（→ｎｘｔ）犻代表狆→ｎｘｔ… →ｎｘｔ，共犻个“→ｎｘｔ”．在该定义中，量词的约束变 元出现在访问路径的上角标中．这种直接基于编程 语言中访问路径语法的定义显得比较直观． ５２符号断言语言 为便于下面的讨论，将系统原型所使用的断言 语言的抽象语法描述在图１６．几点说明如下： 犻犱∈犐犱犲狀狋犻犳犻犲狉（程序中的标识符集） 狋狀∈犛犻犱犲狀狋犻犳犻犲狉（程序中结构体类型的名字集） ｐｒｅｄｉｃａｔｅｄｅｆｉｎｉｔｉｏｎ 狆犱∷＝狆狉犲犱犻犮犪狋犲犻犱（狆狆１，…，狆狆犽）＝犪 ｐｒｅｄｉｃａｔｅｐａｒａｍｅｔｅｒ 狆狆∷＝狋犻犱 ｐａｒａｍｅｔｅｒｔｙｐｅ 狋∷＝犻狀狋｜狋狀 ｐｒｏｐｅｒｔｙｔｈｅｏｒｅｍ 狆狋∷＝狋犺犲狅狉犲犿犪１犪２｜狋犺犲狅狉犲犿犪１犪２ ａｓｓｅｒｔｉｏｎ（犫狅狅犾犲狓狆是布尔表达式，其产生式略去） 犪∷＝犫狅狅犾犲狓狆｜犻犱：犱．犪｜犻犱：犱．犪｜（犪） ｄｏｍａｉｎ（犻狀狋犲狓狆是整型表达式，其产生式略去） 犱∷＝'｜&｜&＋｜犻狀狋犲狓狆１…犻狀狋犲狓狆２ ｌｖａｌｕｅ犾狏∷＝…｜犾狏（→犻犱）犻狀狋犲狓狆 （左值犾狏是各类型犲狓狆的一种选择） 图１６符号断言语言的抽象语法 （１）图１６前一部分是自定义谓词以及这些谓 词之间性质定理的语法，后一部分是断言的语法．谓 词应用可出现在布尔表达式中，因而可出现在断 言中．（２）程序员用图１６的文法编写的断言中出现 的变量，若不是程序变量，则称之为逻辑变量． （３）量词约束变元的论域只能是整数域或它的 某个区间，因而禁止使用指针型约束变元．在需要由 存在量词来约束指针型变元的地方，可以用指针型 逻辑变量来代替． 下面用有序单链表来解释为什么需要提供性质 定理．有序单链表的归纳定义如下： ＳｏｒｔｅｄＬｉｓｔ（Ｎｏｄｅ狆） 狆＝＝ＮＵＬＬ∨狆→ｎｘｔ＝＝ＮＵＬＬ∨ 狆→犱＜＝狆→ｎｘｔ→犱∧ＳｏｒｔｅｄＬｉｓｔ（狆→ｎｘｔ） 在一个子句中，若出现以狆为前缀的访问路 径，则默认有断言狆！＝ＮＵＬＬ．ＳｏｒｔｅｄＬｉｓｔ的定义从 表尾向表头方向归纳．但是，在遍历有序单链表时， 例如图１７单链表插入函数中的循环代码（暂且不关 心图１７中的断言），其遍历方向是从表头向表尾，因 此还需要用下述表段谓词和性质定理． ＳｏｒｔｅｄＬｉｓｔＳｅｇ（Ｎｏｄｅ狆，Ｎｏｄｅ狇） 狆＝＝狇∧狇！＝ＮＵＬＬ∨ 狆→犱＜＝狆→ｎｘｔ→犱∧ ＳｏｒｔｅｄＬｉｓｔＳｅｇ（狆→ｎｘｔ，狇） 和 ＳｏｒｔｅｄＬｉｓｔＳｅｇ（狆，狇）∧狇→犱＜＝狇→ｎｘｔ→犱 ＳｏｒｔｅｄＬｉｓｔＳｅｇ（狆，狇→ｎｘｔ） 这个性质定理保证已扫描过的表段再加入下一个被 扫描的节点，结果仍然是表段． ＳｏｒｔｅｄＬｉｓｔ和ＳｏｒｔｅｄＬｉｓｔＳｅｇ两个谓词之间的 如下性质定理也是验证时不可缺的： ＳｏｒｔｅｄＬｉｓｔＳｅｇ（狆，狇）∧ＳｏｒｔｅｄＬｉｓｔ（狇） ＳｏｒｔｅｄＬｉｓｔ（狆） 上述２个性质定理都需要程序员提供，因为它们的 证明需要基于表段的长度进行归纳，基于演绎推理 的自动定理证明器难以发现这样的性质． ＳｏｒｔｅｄＬｉｓｔ谓词出现在函数的前后断言中，而 ＳｏｒｔｅｄＬｉｓｔＳｅｇ谓词出现在循环不变式中．后者的定 义只要能支持函数前后条件的证明就足矣，没有必 要选择最一般的定义，即把被验证函数中不会出现 的情况也囊括在内，以免给验证增添不必要的麻烦． 在断言文法及其类型系统的基础上，还要限制 断言中的整型表达式必须是线性表达式． ２４７２ 计 算 机 学 报 ２０１６年