418 Journal of Software软件学报Vol.2l,No.3,March2010 (I)domain中的N和N分别是指自然数集和正整数集，exp.exp中的exp和作为访问路径上角标的exp 限制为最多含一个约束变元n的整型表达式壮b或b,其中，b可以是含程序变量和常量的只有加减 运算的表达式； (2)当访问路径集合受多个量词约束时，存在量词约束出现在最左边： (3)访问路径集合之前不可以出现. 例如，i0.n-1.{s->(->r片是指{s->}A{s->->rA..A{s->(->r)-1},这些访问路径集合都是中☑的一个集 合有了量词和带上角标的访问路径，图4中带头结点的双向循环链表用断言定义如下： dlist(s,n)e(k1.n.{s(->r)(->r)+1->)n{s,s(->r)1s->r->. 其中，s是struct ListNode{struct ListNode*r,*I,}类型的指针，n表示除头结点以外的结点数（非负整数）.全称量词 所辖的最后一个集合可以写成{s(->r”,5->,以删掉s(>)+1>1中的环（这时k为n),上式是为了把它统一到全称 量词辖域中因此，断言中的访问路径允许带环该定义的+1个访问路径集合将图2中2n+3个指针的相等关系 表达得一清二楚.并且对图4的每个指针，该定义都从能够表示它的互为别名的访问路径中选择一条访问路径 来表示它.注意，dis1定义中最后一个集合改写成{s,s->->r,s(>)时1}看上去是合理的，但这时该定义式不是一个 合法的平因为{s,s->->r,(>)}中除了s以外，访问路径都是s->1..的形式，而其他有效指针集合中的访问路径 都是s->r..的形式在>0时，在这些集合中找不到s->1->r的前缀s>1的别名 (Assertion)assertion::=-assertion assertionnassertion assertionvassertionVid:domain.assertion id:domain.assertion(assertion)id lval) boolexplvalsetalsetlvalsetp (Domain) domain:=NNl门exp.ep (L-value Set)lvalser::=hvalset.Ivalllyal 白江双 (L-value) lval::=...val->idy Fig.3 Syntax of assertion language Fig.4 Cyclic doubly-linked list 图3断言语言语法 图4双向循环链表 有些数据结构的断言定义需要引入归纳，例如二叉树的定义如下(s仍然是ListNode类型的指针)： tree(s)(s)((s)Atree(s->I)Iree(s->r)), 其中，{s}w表示空树，另一种情况{s}Aee(s->)nee(s->r)表示非空树，并且表达出该树上的指针都不相等，因为 若把归纳定义的引用展开，代表有效指针的各访问路径都在的不同集合中， 2.2断言演算 利用经典逻辑中有关入和的等价公理，可以把含访问路径集合的断言变换成析取范式，在变换过程中，每个 访问路径集合看成一个逻辑常元在断言的析取范式中，每个子句中的访问路径集合部分构成一个平例如，上面 二叉树归纳定义右部的断言就是一个析取范式，两个子句中的代表两种不同情况.注意，子句中可能还有其他 断言，有些断言甚至和判断的合法性有关例如，数据结构归纳定义的引用，涉及访问路径上角标的断言。 依据不丢失访问路径信息的原则，经典逻辑的蕴涵公理A入B一A在B含访问路径集合或归纳定义的引用时 不可使用，因为使用它会导致访问路径信息的丢失，逻辑蕴涵公理A入B一B的情况类似 我们还需要增加一些与有关的逻辑等价或蕴涵公理， 1)W和D的等价公理 MM台W(若(=MU2n(n=0), DAD3台D(若(D-=DUD)(DnD=) 这些等价性存在的依据是等价式两边包含同样的信息 2)非合法平公理 引入量词和数据结构的归纳定义后，需要将先前合法的条件加以补充， (1)合法的检查是对析取范式的各子句分别进行， ©中国科学院软件研究所htp:wwv.c-s-a.org.cn418 Journal of Software 软件学报 Vol.21, No.3, March 2010 (1) domain 中的 N 和 N+ 分别是指自然数集和正整数集,exp..exp 中的 exp 和作为访问路径上角标的 exp 限制为最多含一个约束变元 n 的整型表达式 n±b 或 b,其中,b 可以是含程序变量和常量的只有加减 运算的表达式; (2) 当访问路径集合受多个量词约束时,存在量词约束出现在最左边; (3) 访问路径集合之前不可以出现¬. 例如,∀i:0..n−1.{s->l(->r) i }是指{s->l}∧{s->l->r}∧…∧{s->l(->r) n−1 },这些访问路径集合都是Ψ中Π的一个集 合.有了量词和带上角标的访问路径,图 4 中带头结点的双向循环链表用断言定义如下: dlist(s,n)(∀k:1..n.{s(->r) k ,s(->r) k+1->l})∧{s,s(->r) n+1,s->r->l}. 其中,s 是 struct ListNode{struct ListNode*r,*l;}类型的指针,n 表示除头结点以外的结点数(非负整数).全称量词 所辖的最后一个集合可以写成{s(->r) n ,s->l},以删掉 s(->r) k+1->l 中的环(这时 k 为 n),上式是为了把它统一到全称 量词辖域中.因此,断言中的访问路径允许带环.该定义的 n+1 个访问路径集合将图 2 中 2n+3 个指针的相等关系 表达得一清二楚.并且对图 4 的每个指针,该定义都从能够表示它的互为别名的访问路径中选择一条访问路径 来表示它.注意,dlist 定义中最后一个集合改写成{s,s->l->r,s(->l) n+1}看上去是合理的,但这时该定义式不是一个 合法的Ψ.因为{s,s->l->r,s(->l) n+1}中除了 s 以外,访问路径都是 s->l…的形式,而其他有效指针集合中的访问路径 都是 s->r…的形式.在 n>0 时,在这些集合中找不到 s->l->r 的前缀 s->l 的别名. Fig.3 Syntax of assertion language Fig.4 Cyclic doubly-linked list 图 3 断言语言语法 图 4 双向循环链表 有些数据结构的断言定义需要引入归纳,例如二叉树的定义如下(s 仍然是 ListNode 类型的指针): tree(s){s}N∨({s}∧tree(s->l)∧tree(s->r)), 其中,{s}N 表示空树,另一种情况{s}∧tree(s->l)∧tree(s->r)表示非空树,并且表达出该树上的指针都不相等,因为 若把归纳定义的引用展开,代表有效指针的各访问路径都在Π的不同集合中. 2.2 断言演算 利用经典逻辑中有关∧和∨的等价公理,可以把含访问路径集合的断言变换成析取范式.在变换过程中,每个 访问路径集合看成一个逻辑常元.在断言的析取范式中,每个子句中的访问路径集合部分构成一个Ψ.例如,上面 二叉树归纳定义右部的断言就是一个析取范式,两个子句中的Ψ代表两种不同情况.注意,子句中可能还有其他 断言,有些断言甚至和判断Ψ的合法性有关.例如,数据结构归纳定义的引用,涉及访问路径上角标的断言. 依据不丢失访问路径信息的原则,经典逻辑的蕴涵公理 A∧B⇒A 在 B 含访问路径集合或归纳定义的引用时 不可使用,因为使用它会导致访问路径信息的丢失,逻辑蕴涵公理 A∧B⇒B 的情况类似. 我们还需要增加一些与Ψ有关的逻辑等价或蕴涵公理. 1) N和D的等价公理 N1∧N2⇔N (若(N==N1∪N2)∧(N1∩N2==∅)), D1∧D2⇔D (若(D==D1∪D2)∧(D1∩D2==∅)). 这些等价性存在的依据是等价式两边包含同样的信息. 2) 非合法Ψ公理 引入量词和数据结构的归纳定义后,需要将先前合法Ψ的条件加以补充. (1) 合法Ψ的检查是对析取范式的各子句分别进行; (Assertion)assertion::= ¬assertion|assertion∧assertion |assertion∨assertion|∀id:domain.assertion |∃id:domain.assertion|(assertion)|id(lval) | boolexp|{lvalset}|{lvalset}N|{lvalset}D (Domain) domain::=N| N+ |exp..exp (L-value Set) lvalset::=lvalset,lval|lval (L-value) lval::=…|lval(->id) exp … s …