420 Journal of Software软件学报Vol.2l,No.3,March2010 (4)测试内存泄漏leak(Sp) 删除集合中的访问路径p时（出现在对p赋值时），若S中所有访问路径都是p的别名或以p的别名为前 缀，则会出现内存泄漏。 leak(Sp)g:S(alias(q.p)v3r:P.(alias(r.p)prefix(r,q))). 下面给出联系到PointerC各种语句的公理和推理规则这些规则体现了相应语句引起访问路径集合的增、 删和替换在下面所有规则中，访问路径上的计算都是基于语句前那个程序点的平，并且Q中能被吸收的布尔 表达式己被吸收， 1)指针类型赋值语句p=q和p=NULL 下面只列举几种情况下的规则，其他情况下的规则类似： (1)p和q都有别名在的同一个集合中 {SA..ASn1ASP4入仄DnQ}P=q{SA.AS-ASg4仄DQ} (2)p的别名在中，q的别名在的某个集合中。 (SiA...ASS9PADnO)p=qSi...(+p)(NP-p)DnO) (3)p的别名在的某个集合中，q的别名在中 (Sin...SISPDnO)p=gi Silpn..S-lpn(s lp-p)n(N Ip+p)nDpnOlp) (若对于赋值前的平，leak(S,p)为假). 其中，Qp的意思也是把Q中以p的别名为前缀的访问路径都用它们不以p的别名为前缀的别名替换， (4)赋值语句是p=WULL的形式且p的别名D冲 (Sin...SMADO)p=NULLISiN...S(N+p)(D-p)o) (S)p的别名和q别名在不同的中 可以把该语句当作dhmm=p,p=NULL:p=dummy,dummy=NULL语句序列来证明，当然也可以设计专门的规 则.每个函数可以看成有一个虚拟局部变量dummy,.初值是NULL,每次遇到这类赋值时都这么处理，在函数结束 时将dumy从中去掉 2)非指针类型的赋值语句x=e 在此用的是正向的赋值公理，其中，FV表示变元中的自由变量集合. (Sin...ASADnO)x=e(Sin..AMADA(3x'.(x=-e[xe-x']nO[V-x]...[nx][xe-x'])), 1…yn是Q中出现的x的所有别名，x'E({UFV(e)UFVO) 3)复合、条件和循环语句的规则 复合、条件和循环语句的规则以及推论规则等仍然使用Hoare逻辑的规则. 4)分配空间语句p=malloc(structt) 其中，1是结构类型，并假设r,厂是1的指针类型的域名.下面只列举两种情况： (1)p的别名在中 (S...ASPADAO)p=malloc(struct t)(SA...Sip)(NP-p)(Drip->r1....p->rO) (2)p的别名在的某个集合中 可以把该语句看成语句序列p=NULL:P=malloc(struct)来进行证明，当然也可以设计专门的规则. 5)释放空间语句ree(p) 只有p在的某个集合中，才能使用fe函数.根据p所指对象的类型可以知道，其所有指针类型域的访问 路径p->r1…p->rm把该语句当成语句序列p->r=NULL,…p->r。=NULL;free(p)来进行证明.这样做的目的是简 化fee(p)的规则. {SA..ASx-AS入仄DO)free(p){SA.An-1A(仁{p->r1,…p->rn})(D4S)nQ(若Q中没有p的别名)， 6)分情况规则 需要增加一条分情况证明规则，因为一个语句前条件的析取范式可能使分成多种情况.该规则如下： ©中国科学院软件研究所htp:wwv.c-s-a.org.cn420 Journal of Software 软件学报 Vol.21, No.3, March 2010 (4) 测试内存泄漏 leak(S,p) 删除Π集合S中的访问路径 p 时(出现在对 p 赋值时),若S中所有访问路径都是 p 的别名或以 p 的别名为前 缀,则会出现内存泄漏. leak(S,p)∀q:S.(alias(q,p)∨∃r:P.(alias(r,p)∧prefix(r,q))). 下面给出联系到 PointerC 各种语句的公理和推理规则.这些规则体现了相应语句引起访问路径集合的增、 删和替换.在下面所有规则中,访问路径上的计算都是基于语句前那个程序点的Ψ,并且 Q 中能被Ψ吸收的布尔 表达式已被吸收. 1) 指针类型赋值语句 p=q 和 p=NULL 下面只列举几种情况下的规则,其他情况下的规则类似: (1) p 和 q 都有别名在Π的同一个集合中. {S1∧…∧Sn−1∧Sp ,q ∧N∧D∧Q}p=q{S1∧…∧Sn−1∧Sp ,q ∧N∧D∧Q}. (2) p 的别名在N中,q 的别名在Π的某个集合中. {S1∧…∧Sn−1∧Sq∧Np∧D∧Q}p=q{S1∧…∧Sn−1∧(Sq +p)∧(Np −p)∧D∧Q}. (3) p 的别名在Π的某个集合中,q 的别名在N中. {S1∧…∧Sn−1∧Sp∧Nq∧D∧Q}p=q{S1/p∧…∧Sn−1/p∧(Sp /p−p)∧(Nq /p+p)∧D/p∧Q/p} (若对于赋值前的Ψ,leak(Sp ,p)为假). 其中,Q/p 的意思也是把 Q 中以 p 的别名为前缀的访问路径都用它们不以 p 的别名为前缀的别名替换. (4) 赋值语句是 p=NULL 的形式且 p 的别名D中. {S1∧…∧Sn∧N∧Dp∧Q}p=NULL{S1∧…∧Sn∧(Np +p)∧(Dp −p)∧Q}. (5) p 的别名和 q 别名在不同的Π中. 可以把该语句当作 dummy=p;p=NULL;p=dummy;dummy=NULL 语句序列来证明,当然也可以设计专门的规 则.每个函数可以看成有一个虚拟局部变量 dummy,初值是 NULL,每次遇到这类赋值时都这么处理,在函数结束 时将 dummy 从N中去掉. 2) 非指针类型的赋值语句 x=e 在此用的是正向的赋值公理,其中,FV 表示变元中的自由变量集合. {S1∧…∧Sn∧N∧D∧Q}x=e{S1∧…∧Sn∧N∧D∧(∃x′.(x==e[x←x′]∧Q[y1←x]…[yn←x][x←x′])), (y1,…,yn 是 Q 中出现的 x 的所有别名,x′∉({x}∪FV(e)∪FV(Q))). 3) 复合、条件和循环语句的规则 复合、条件和循环语句的规则以及推论规则等仍然使用 Hoare 逻辑的规则. 4) 分配空间语句 p=malloc(struct t) 其中,t 是结构类型,并假设 r1,…,rn 是 t 的指针类型的域名.下面只列举两种情况: (1) p 的别名在N中 {S1∧…∧Sn∧Np∧D∧Q}p=malloc(struct t){S1∧…∧Sn∧{p}∧(Np −p)∧(D+{p->r1,…,p->rn})∧Q}. (2) p 的别名在Π的某个集合中 可以把该语句看成语句序列 p=NULL;p=malloc(struct t)来进行证明,当然也可以设计专门的规则. 5) 释放空间语句 free(p) 只有 p 在Π的某个集合中,才能使用 free 函数.根据 p 所指对象的类型可以知道,其所有指针类型域的访问 路径 p->r1,…,p->rn.把该语句当成语句序列 p->r1=NULL;…;p->rn=NULL;free(p)来进行证明.这样做的目的是简 化 free(p)的规则. {S1∧…∧Sn−1∧Sp∧N∧D∧Q}free(p){S1∧…∧Sn−1∧(N−{p->r1,…,p->rn})∧(D+Sp )∧Q}(若 Q 中没有 p 的别名). 6) 分情况规则 需要增加一条分情况证明规则,因为一个语句前条件的析取范式可能使Ψ分成多种情况.该规则如下: