陈意云等：一种用于指针程序验证的指针逻辑 423 (pp(->r)"p->r->In(s)A{s->r)DN>=OnI<ini<n+1)v.... q->1->=S /q->1->r和p(->r)互为别名，于是一些访问路径需要用它们的别名代替/ 【k1.i-2.{p->ryp->r1->l}{s->l,p->r,q->{q,q->r->}n k:itl.n.{q(->r,q(>r）-1>}{p,q(->r-p->r->} (p(->r),s)A(s->r)oNn>=0AI<ini<n+1)v...) 8->=q 【.v(k:l.i-2.{p->r,p->r）)+1->}A{s->l,p->r,q->}A{s->r,9,9->r->}n ki+1.n.{q(->r)-,q(->r)-1->}A{p,q(->r）-1p->r->}n (p(->r),s)Nn>=0AI<ini<n+1)v...) q->1=s, 【vk1.i-2.p(->r）,p->+1->{s->lp->r}{s->r,qqr>r->0} kit1n.{q(->r)-,q(->r）-1->A{p,q->ry-p->r->} ip(->r),g->I.s)Nn>=0AI<ini<n+1)v...] S=NULL;q=NULL; 【(kl.i-2.p->r'p->r+1>}{p->r)p->r->Ap(->rp(->r2>A kit1.n.p->r）1p(->r）+2>{p,p(->ryt2p->r->}A fp(->r)p(->r)>fg.sivn>=001<ini<n+l)v... {dlis(p,n+1)>=0} return p; 如果语句=insert(s,)的前断言是dis1(s,n)A{r}Nw>=OAl<=jy<=n+l,则用函数调用规则得到该语句的后 断言是dlist(,n+1)w>=0. 4与分离逻辑的比较 指针逻辑和分离逻辑I都是Hoare逻辑的一种扩展，都可用来对使用共享可变数据结构(shared mutable data structure)的命令式程序进行推理.分离逻辑在汇编语言级程序验证中得到广泛应用，但是它不适于对高级 语言编写的程序进行推理在分离逻辑中，分离合取断言P*Q中的P和Q分别对可访问存储的不相交部分成立， 这导致在与分离逻辑相关联的编程语言中，脱引用(dereference)操作序列不能出现在表达式中，而这样的操作在 高级语言程序中经常出现例如，下面的C程序段取自删除单链表元素的函数： s=1->next,1->next=1->next->next,free(s); 其中的表达式1->nex1->nex!关联到两个分离的堆块.分离逻辑没有应用到这种表达式的推理规则.虽然把该程 序段变换成s=1->next,=s->nert,->nex=r:free(s;后能被分离逻辑接受.但是若想对一般程序完成这种变换，则需 要对程序进行别名分析」 分离逻辑的断言语言不太适合于描述带环的数据结构.本文用指针逻辑给出图4双向循环链表的清晰定 义.而Reynolds用分离逻辑定义双向循环链表时1，首先引入带4个参数（头结点指针1、尾结点指针s,1->1和 s>)的双向链表段的归纳定义.在该定义中，->1和s>r同表段中其他结点的联系没有定义，以便于规范在表段 上的插入和删除操作进一步定义双向循环链表时，还需要加入==>r和==1->1两个断言显然，这种定义双向 循环链表的方式不是很直观.另外，在分离逻辑中，二叉树的定义需要借助Ls即语言首先采用的S表达式， 在扩展Hoa逻辑时，分离逻辑的策略可以这样理解：所有指针被假定有可能指向同一个对象，除非它们显 式地表达为指向不同对象.于是，分离逻辑需要引入像分离合取“*”这样的连接词我们认为，在对指针程序进行 推理时，最重要的是掌握每个程序点的有效指针相等信息，基于这些信息可以推导出两条访问路径是否互为别 ©中国科学院软件研究所htp:wwv.c-s-a.org.cm陈意云 等:一种用于指针程序验证的指针逻辑 423 {p,p(->r) n+1,p->r->l}∧{s}∧{s->r}D∧n>=0∧1<i∧i<n+1)∨…} q->l->r=s; /*q->l->r 和 p(->r) i 互为别名,于是一些访问路径需要用它们的别名代替*/ {…∨(∀k:1..i−2.{p(->r) k ,p(->r) k+1->l}∧{s->l,p(->r) i−1 ,q->l}∧{q,q->r->l}∧ ∀k:i+1..n.{q(->r) k−i ,q(->r) k−i+1->l}∧{p,q(->r) n−i+1,p->r->l}∧ {p(->r) i ,s}∧{s->r}D∧n>=0∧1<i∧i<n+1)∨…} s->r=q; {…∨(∀k:1..i−2.{p(->r) k ,p(->r) k+1->l}∧{s->l,p(->r) i−1 ,q->l}∧{s->r,q,q->r->l}∧ ∀k:i+1..n.{q(->r) k−i ,q(->r) k−i+1->l}∧{p,q(->r) n−i+1,p->r->l}∧ {p(->r) i ,s}∧n>=0∧1<i∧i<n+1)∨…} q->l=s; {…∨(∀k:1..i−2.{p(->r) k ,p(->r) k+1->l}∧{s->l,p(->r) i−1 }∧{s->r,q,q->r->l}∧ ∀k:i+1..n.{q(->r) k−i ,q(->r) k−i+1->l}∧{p,q(->r) n−i+1,p->r->l}∧ {p(->r) i ,q->l,s}∧n>=0∧1<i∧i<n+1)∨…} s=NULL;q=NULL; {…∨(∀k:1..i−2.{p(->r) k ,p(->r) k+1->l}∧{p(->r) i−1 ,p(->r) i ->l}∧{p(->r) i+1,p(->r) i+2->l}∧ ∀k:i+1..n.{p(->r) k+1,p(->r) k+2->l}∧{p,p(->r) n+2,p->r->l}∧ {p(->r) i ,p(->r) i+1->l}∧{q,s}N∧n>=0∧1<i∧i<n+1)∨…} ⇒ {dlist(p,n+1)∧n>=0} return p; } 如果语句 r=insert(s,j)的前断言是 dlist(s,n)∧{r}N∧n>=0∧1<=j∧j<=n+1,则用函数调用规则得到该语句的后 断言是 dlist(r,n+1)∧n>=0. 4 与分离逻辑的比较 指针逻辑和分离逻辑[15]都是 Hoare 逻辑的一种扩展,都可用来对使用共享可变数据结构(shared mutable data structure)的命令式程序进行推理.分离逻辑在汇编语言级程序验证中得到广泛应用,但是它不适于对高级 语言编写的程序进行推理.在分离逻辑中,分离合取断言 P*Q 中的 P 和 Q 分别对可访问存储的不相交部分成立, 这导致在与分离逻辑相关联的编程语言中,脱引用(dereference)操作序列不能出现在表达式中,而这样的操作在 高级语言程序中经常出现.例如,下面的 C 程序段取自删除单链表元素的函数: s=t->next; t->next=t->next->next; free(s); 其中的表达式 t->next->next 关联到两个分离的堆块.分离逻辑没有应用到这种表达式的推理规则.虽然把该程 序段变换成 s=t->next;r=s->next;t->next=r;free(s);后能被分离逻辑接受.但是若想对一般程序完成这种变换,则需 要对程序进行别名分析. 分离逻辑的断言语言不太适合于描述带环的数据结构.本文用指针逻辑给出图 4 双向循环链表的清晰定 义.而 Reynolds 用分离逻辑定义双向循环链表时[15],首先引入带 4 个参数(头结点指针 t、尾结点指针 s,t->l 和 s->r)的双向链表段的归纳定义.在该定义中,t->l 和 s->r 同表段中其他结点的联系没有定义,以便于规范在表段 上的插入和删除操作.进一步定义双向循环链表时,还需要加入 t==s->r 和 s==t->l 两个断言.显然,这种定义双向 循环链表的方式不是很直观.另外,在分离逻辑中,二叉树的定义需要借助 Lisp 语言首先采用的 S 表达式. 在扩展 Hoare 逻辑时,分离逻辑的策略可以这样理解:所有指针被假定有可能指向同一个对象,除非它们显 式地表达为指向不同对象.于是,分离逻辑需要引入像分离合取“*”这样的连接词.我们认为,在对指针程序进行 推理时,最重要的是掌握每个程序点的有效指针相等信息,基于这些信息可以推导出两条访问路径是否互为别