422 Journal of Software软件学报Vol.21,No.3,March2010 (I)建立基于栈和堆的抽象机器模型，定义PointerC语言的操作语义： (2)给出断言语言在模型上的解释，包括几种访问路径集合的含义.并证明有关访问路径集合的蕴涵和 等价公理在该模型上是可靠的： (3)证明指针逻辑的每条推理规则对该模型及操作语义可靠， 3证明实例 利用PointerC语言出具证明编译器的初步实现l2,1,我们证明了单链表、双向链表和二叉树等数据结构的 一些函数的安全性或正确性.本节以带头结点的双向循环链表（图4）的结点插入函数insr1(p,i)的安全性证明为 例，展示指针逻辑的应用.其中，p是链表的指针，i是插入位置，链表的长度为. 该函数对空表和非空表采用统一的代码，但是下面的证明一开始就分成两种情况，然后每种情况又分成两 种子情况，这是因为不同情况的访问路径集合不一样，很难用统一的方式来表达它们. (1)插在表的非尾部(1<=i八i<n+1).两种子情况分别是：插在头部(=1i<n+1)和其他位置(1<ii<+1) (2)插在表的尾部(=+1).两种子情况分别是：空表(n==0i=1)和非空表(n>0Λ==+1). 限于篇幅，下面程序中某些程序点的断言被忽略 在所列出的断言中，很多地方只给出析取范式的一种情况， 【dlis(p,n)）An>=0Al<=ii=n+l} struct ListNode*insert(struct ListNodep;int i) struct ListNode*g,*s; intJ, k:1.n.{p->r),p(->r)1->l}A{p,p(->rt1p->r->}A{g,s}DM>=0n1<=ini=n+1】 j=1;q=p->r, k1.j-1.{p(->rp(->r)+1->A{q,p->ryp->ryl->Akjt1n.{p->r)p(->r)+1->n (p.p(->r)"p->r->IAis)pN>=0A1<=jN<n+1)v(Vk:1..n.(p(->r)p(->r)> {qP,p(->r)1p->r->}A{sDAn>-0y=+1)》 /体循环不变式，分成1<=y+1和=+1两种情况/ while (j<i) q=q->r; 《k1.j.{p->r),p(->r1->{qp->r',0p->rY2>Akjt2…n.p(->r）p->r）1>乃A (pp(->r)"p->r->IA(s)DN=0nI<=jnj<n+1)v...] =+1的情况被忽略*/ jj+1, ((Vk:1.j-1.(p(->r)p(->r)>gp(->rY.(p->r kjt1.n.{p->r)p->r)+1->}A{p,p(->r)p->r->}A{s}Dwn>=0A1<=jyn+1)n} k:l.i-l.{p(->rp->r）+1->A{gp(->r/,p->r1->n ki+l.n.{p(->r)p(->r)1->}A{p,p(->r)Hp->r->A{sDw>=0A1<=ii+1)N s=malloc(ListNode); {k:1.i-1.{p(->r)p(->r)+1->0{g,p->r,p->r)1->}Akit1n.{p->r)p(->r）+1->l}n (pp(->r)"p->r->(si(s->r,s->lDAn>=0A1<=ini<n+1)v...) s->=q-> /体下面仅给出1<i八<+1这种子情况的断言*/ 【.vk:1.i-2.{p(->rp->r)1->A{s->l,p(->rp(->r->n {q,p(->rp->r)H1->}kit1n.{p->r)p(->r)+1->l}n ©中国科学院软件研究所htp:wwv.c-s-a.org.cn422 Journal of Software 软件学报 Vol.21, No.3, March 2010 (1) 建立基于栈和堆的抽象机器模型,定义 PointerC 语言的操作语义; (2) 给出断言语言在模型上的解释,包括几种访问路径集合的含义.并证明有关访问路径集合的蕴涵和 等价公理在该模型上是可靠的; (3) 证明指针逻辑的每条推理规则对该模型及操作语义可靠. 3 证明实例 利用 PointerC 语言出具证明编译器的初步实现[12,14],我们证明了单链表、双向链表和二叉树等数据结构的 一些函数的安全性或正确性.本节以带头结点的双向循环链表(图 4)的结点插入函数 insert(p,i)的安全性证明为 例,展示指针逻辑的应用.其中,p 是链表的指针,i 是插入位置,链表的长度为 n. 该函数对空表和非空表采用统一的代码,但是下面的证明一开始就分成两种情况,然后每种情况又分成两 种子情况,这是因为不同情况的访问路径集合不一样,很难用统一的方式来表达它们. (1) 插在表的非尾部(1<=i∧i<n+1).两种子情况分别是:插在头部(i==1∧i<n+1)和其他位置(1<i∧i<n+1). (2) 插在表的尾部(i==n+1).两种子情况分别是:空表(n==0∧i==1)和非空表(n>0∧i==n+1). 限于篇幅,下面程序中某些程序点的断言被忽略. 在所列出的断言中,很多地方只给出析取范式的一种情况. {dlist(p,n)∧n>=0∧1<=i∧i<=n+1} struct ListNode*insert(struct ListNode*p;int i) { struct ListNode*q,*s; int j; {∀k:1..n.{p(->r) k ,p(->r) k+1->l}∧{p,p(->r) n+1,p->r->l}∧{q,s}D∧n>=0∧1<=i∧i<=n+1} j=1; q=p->r; {(∀k:1..j−1.{p(->r) k ,p(->r) k+1->l}∧{q,p(->r) j ,p(->r) j+1->l}∧∀k:j+1..n.{p(->r) k ,p(->r) k+1->l}∧ {p,p(->r) n+1,p->r->l}∧{s}D∧n>=0∧1<=j∧j<n+1)∨(∀k:1..n.{p(->r) k ,p(->r) k+1->l}∧ {q,p,p(->r) n+1,p->r->l}∧{s}D∧n>=0∧j==n+1)} /*循环不变式,分成 1<=j∧j<n+1 和 j==n+1 两种情况*/ while (j<i) { q=q->r; {(∀k:1..j.{p(->r) k ,p(->r) k+1->l}∧{q,p(->r) j+1,(p->r) j+2->l}∧∀k:j+2...n.{p(->r) k ,p(->r) k+1->l}∧ {p,p(->r) n+1,p->r->l}∧{s}D∧n>=0∧1<=j∧j<n+1)∨…} /*j==n+1 的情况被忽略*/ j=j+1; {(∀k:1..j−1.{p(->r) k ,p(->r) k+1->l}∧{q,p(->r) j ,(p->r) j+1->l}∧ ∀k:j+1...n.{p(->r) k ,p(->r) k+1->l}∧{p,p(->r) n+1,p->r->l}∧{s}D∧n>=0∧1<=j∧j<n+1)∨…} } {(∀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.{p(->r) k ,p(->r) k+1->l}∧{p,p(->r) n+1,p->r->l}∧{s}D∧n>=0∧1<=i∧i<n+1)∨…} s=malloc(ListNode); {(∀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.{p(->r) k ,p(->r) k+1->l}∧ {p,p(->r) n+1,p->r->l}∧{s}∧{s->r,s->l}D∧n>=0∧1<=i∧i<n+1)∨…} s->l=q->l; /*下面仅给出 1<i∧i<n+1 这种子情况的断言*/ {…∨(∀k:1..i−2.{p(->r) k ,p(->r) k+1->l}∧{s->l,p(->r) i−1 ,p(->r) i ->l}∧ {q,p(->r) i ,p(->r) i+1->l}∧∀k:i+1..n.{p(->r) k ,p(->r) k+1->l}∧