340 Journal of Software软件学报Vol.2l,No.2,February2010 void schorr_waite(node *roor){ node *1,*p,*q, (graph(root)(1p,q)p) F=root,p=NULL;q=NULL;rooF=NULL; (graph(t)(root.p.q) {graph(I)Ngraph(p)A{oo1,q}N}/体循环不变式*/ while (p!=NULLV(p==NULLAf!=NULLA-t->m)){ ((graph(t)ngraph(p->Dngraph(p->r)lpfroot,q N)v (graph(t->D)Agraph(t->r)[t](p,root,q-t->m)) if (==NULLV(t!=NULLAL->m)){ ((graph(p->D)graph(p->r)Alp](t,root,q)N)v (graph(p->D)ngraph(p->r)A[plngraph(t->D)ngraph(t->r)t(root,qN) if (p->c){/*pop * q=t;Fp;p=p->r,t->r-g;g-NULL; ((graph(t->DA[tIgraph(p)froot.q,t->rN)v (graph(t->DA[I]graph(p)ngraph(t->r->DAgraph(t->r->r)[t->r]{root,q)N)) else/序swing*/ q=t;Fp->r,p->r=p->l;p->Fq;p->c-true;q=NULL; ((graph(p->r)ngraph(1)A[p(root,q.p->lNv (graph(p->r)ngraph(t)[p]ngraph(p->1->D)ngraph(p->1->r)[p->(root,qN)) {graph()Ngraph(p)n{rool,q}v}/伟循环不变式*/ else{/push,t!=NULLA-t->m * (graph(p->DAgraph(p->r)p Agraph(t->D)Agraph(t->r)t root,qiN-t->m)v (graph(t->1)ngraph(t->r)A[t](p,root,q)x-t->m)) q=p;p=t,=1->I;p->l=q;p->m=true;p->c=false;q=NULL; ((graph(p->1->Dngraph(p->1->r)A[p->Ingraph(t)ngraph(p->r)Alpl(root,q)N)v (graph(t)ngraph(p->r)lp(root,q.p->I) {graph(t)graph(p)A{roo1,q}w}*循环不变式*/ } }/p=NULLA(F=NULLV(tl=NULLAL->m))*/ (graph(t)(root.p.qx) 2.2 Glibe中异步1/O删除请求函数 在以往的工作中，我们仅使用指针逻辑完成了典型数据结构（如单链表、二叉树等）上的典型操作（如插入节 点等)的验证，尚未真正验证实际程序中使用共享易变数据结构的例子通过调查实际程序发现，虽然程序中使 用一般图和有向无环图时都是用邻接矩阵等方式来表示这样的数据结构，似乎指针逻辑该扩展的用处不大，但 是在实际使用链表、二叉树的程序中，常常会针对特定问题设计特殊的数据结构以及其上的实现特定功能的操 作，它们体现出对指针逻辑扩展的需求.本节以GNU C Library中的一段源码为例，展示指针逻辑在实际中的 应用. ©中国科学院软件研究所htp:www.c-s-a.org.cn340 Journal of Software 软件学报 Vol.21, No.2, February 2010 void schorr_waite (node *root){ node *t, *p, *q; {graph(root)∧{t,p,q}D} t=root; p=NULL; q=NULL; root=NULL; {graph(t)∧{root,p,q}N} {graph(t)∧graph(p)∧{root,q}N} /*循环不变式*/ while (p!=NULL∨(p==NULL∧t!=NULL∧¬t->m)){ {(graph(t)∧graph(p->l)∧graph(p->r)∧[p]∧{root,q}N)∨ (graph(t->l)∧graph(t->r)∧[t]∧{p,root,q}N∧¬t->m)} if (t==NULL∨(t!=NULL∧t->m)){ {(graph(p->l)∧graph(p->r)∧[p]∧{t,root,q}N)∨ (graph(p->l)∧graph(p->r)∧[p]∧graph(t->l)∧graph(t->r)∧[t]∧{root,q}N)} if (p->c){ /* pop */ q=t; t=p; p=p->r; t->r=q; q=NULL; {(graph(t->l)∧[t]∧graph(p)∧{root,q,t->r}N)∨ (graph(t->l)∧[t]∧graph(p)∧graph(t->r->l)∧graph(t->r->r)∧[t->r]∧{root,q}N)} } else { /* swing */ q=t; t=p->r; p->r=p->l; p->l=q; p->c=true; q=NULL; {(graph(p->r)∧graph(t)∧[p]∧{root,q,p->l}N)∨ (graph(p->r)∧graph(t)∧[p]∧graph(p->l->l)∧graph(p->l->r)∧[p->l]∧{root,q}N)} } {graph(t)∧graph(p)∧{root,q}N} /*循环不变式*/ } else { /* push, t!=NULL∧¬t->m */ {(graph(p->l)∧graph(p->r)∧[p]∧graph(t->l)∧graph(t->r)∧[t]∧{root,q}N∧¬t->m)∨ (graph(t->l)∧graph(t->r)∧[t]∧{p,root,q}N∧¬t->m)} q=p; p=t; t=t->l; p->l=q; p->m=true; p->c=false; q=NULL; {(graph(p->l->l)∧graph(p->l->r)∧[p->l]∧graph(t)∧graph(p->r)∧[p]∧{root,q}N)∨ (graph(t)∧graph(p->r)∧[p]∧{root,q,p->l}N)} {graph(t)∧graph(p)∧{root,q}N} /*循环不变式*/ } } /* p==NULL∧(t==NULL∨(t!=NULL∧t->m)) */ {graph(t)∧{root,p,q}N} } 2.2 Glibc中异步I/O删除请求函数 在以往的工作中,我们仅使用指针逻辑完成了典型数据结构(如单链表、二叉树等)上的典型操作(如插入节 点等)的验证,尚未真正验证实际程序中使用共享易变数据结构的例子.通过调查实际程序发现,虽然程序中使 用一般图和有向无环图时都是用邻接矩阵等方式来表示这样的数据结构,似乎指针逻辑该扩展的用处不大,但 是在实际使用链表、二叉树的程序中,常常会针对特定问题设计特殊的数据结构以及其上的实现特定功能的操 作,它们体现出对指针逻辑扩展的需求.本节以GNU C Library[11]中的一段源码为例,展示指针逻辑在实际中的 应用