3期 陈意云等：一种用于指针程序安全性证明的指针逻辑 377 3.3公理和推理规则 (4)复合、条件和循环语句的规则以及推论规 下面给出联系到PointerC各种语句的公理和 则等仍然使用Hoare逻辑的规则， 推理规则.这些规则体现了相应语句引起的指针集 (5)分配空间语句p=malloc(T),其中T是类 合的增、减和替换.在下面的所有规则中，其前提中的 型.若T是结构类型，r1,r2,…,rn是其中的指针域 断言都是基于语句前的那个程序点的亚来计算的， 在该类型中的访问路径， (1)指针之间的赋值语句p=q(包括q是常量 (a)p是NULL指针 NULL的情况，略去了g是悬空指针的规则)； <:N 不同情况的指针赋值用不同的规则， {ⅡANND}p=malloc(T){(Ⅱ+p)∧N/pA (a)p和q是相等的有效指针，或都等于NULL (DU{p->r,…,p>r})》 3S:Ⅱ.(p<:S∧q<:S)V (b)p是悬空指针的规则和(a)类似. (p<:NA(g<:NV=NULL)) (c)p是有效指针.把该语句看成语句序列p= {ⅡANAD}p=qⅡANAD} NULL:p=malloc(T),并将相应的规则用于证明， (b)p和q是不相等的有效指针 (6)释放空间语句free(p) 3S1:Ⅱ.S2:Ⅱ.(S1！=S2A p<:SiAq<:S2)A-leak(p) 下面的规则用于p所指向对象不含有效指针的场 {Ⅱ八N八D}p= 合.若从Ⅱ知道p所指向的对象中含有有效指针p-> q{((Ⅱ/p)add p to q)∧W\pAD叭p} 方，…，p>r。,则可把该语句看成语句序列 (c)p是NULL指针，q是有效指针 p->r=NULL;…;p->rm=NULL;free(p)来 p<:WAq<:Ⅱ 进行证明.这样做的目的是简化free(p)的规则. {ⅡAWAD}p=g{(Ⅱadd p to g)AW/pAD} p<:Ⅱ (d)p是悬空指针，q是有效指针 {ⅡAWAD}free(p){(Ⅱ-p)A p<:D∧q<:Ⅱ (W/{p->r1,…,p->rm}∧(DUequals(p)》 {ⅡANAD}p=q{(Ⅱadd p to q)AN∧D/p} (e)p是有效指针，q等于NULL 4 证明实例 p<:ⅡA(q<:WVg==NULL)A一leak(p) {ⅡAWD}p=q{Ⅱ/pA(W\pU{p})AD叭p} 我们已经用指针逻辑系统证明了单链表、双向 (f)p是悬空指针，q等于NULL 链表和二叉树等数据结构的一些函数.本节以删除 <DA(q<:NVg==NULL) 二叉排序树一个结点并重接它的左或右子树的函数 {ⅡANAD}p=q{ⅡA(WU{p})∧D/p} struct node*DeleteNode(struct node*p)为例. (2)非指针类型的赋值公理 在证明该函数时，参数所指向的树上，有效指针 {Ψ∧(Q[yx]…[ynx][xe])}x=e{ΨAQ} 和NULL指针的布局是不清楚的，但它必须满足 (y1,y2,…,yn构成closure(x)的所有成员)， 树的定义.若树结点定义是struct node{int data; 这是考虑了别名情况后的Hoare逻辑赋值公 struct node*l,r:},那么以p为根结点指针的树 理，它不改变亚.该公理中的断言Q只含整型数据 的定义如下： 的子断言，以下使用的Q也都满足这个限制 tree(p)ApixV(p}Atree(p-l)Atree(p-r)). (3)对于指针类型的赋值，若前条件是亚八Q, 如果p不是空指针，通过下面的演算可以知道p 并且Q中也有访问路径（包括作为Q中访问路径前 是有效指针并且tree(p->l)∧tree(p>r)为真： 缀的情况)，则除了用先前指针赋值的规则外，还需 tree(p)A(p!=NULL) 要用下面的赋值公理。 (p)xV((p)Atree(p-l)Atree(p-r)))A {ΨAQ}p=q{亚∧Q[r←p]》 (!=NULL) (r是closure(p)中的一个其它成员， 台({p}wA(p!=NULL)V 平由(1)的规则从平得到). ((p)Ntree(p-)Ntree(p-r)A(p!=NULL)) 换一种说法是，对指针p赋值时，对p的别名 falseV((p)Atree(p-1)Atree(p-r)) 替换还需要出现在亚以外的断言中.该规则也用在 台{p}∧tree(p->l)A tree(p->r). malloc和free语句场合. 程序设计者只要给出函数前后条件和循环不变３３ 公理和推理规则 下面给出联系到 ＰｏｉｎｔｅｒＣ 各种语句的公理和 推理规则．这些规则体现了相应语句引起的指针集 合的增、减和替换．在下面的所有规则中，其前提中的 断言都是基于语句前的那个程序点的Ψ 来计算的． （１）指针之间的赋值语句狆＝狇（包括狇是常量 ＮＵＬＬ的情况，略去了狇是悬空指针的规则）； 不同情况的指针赋值用不同的规则． （ａ）狆和狇 是相等的有效指针，或都等于 ＮＵＬＬ 犛：Π．（狆＜：犛∧狇＜：犛）∨ （狆＜：!∧（狇＜：! ∨狇≡≡ ＮＵＬＬ）） ｛Π∧!∧"｝狆＝狇｛Π∧!∧"｝ ． （ｂ）狆和狇 是不相等的有效指针 犛１：Π．犛２：Π．（犛１！＝犛２∧ 狆＜：犛１∧狇＜：犛２）∧犾犲犪犽（狆） ｛Π∧!∧"｝狆＝ 狇｛（（Π／狆）ａｄｄ狆ｔｏ狇）∧!＼狆∧"＼狆｝ ． （ｃ）狆是 ＮＵＬＬ指针，狇是有效指针 狆＜：!∧狇＜：Π ｛Π∧!∧"｝狆＝狇｛（Πａｄｄ狆ｔｏ狇）∧!／狆∧"｝． （ｄ）狆是悬空指针，狇是有效指针 狆＜："∧狇＜：Π ｛Π∧!∧"｝狆＝狇｛（Πａｄｄ狆ｔｏ狇）∧!∧"／狆｝． （ｅ）狆是有效指针，狇等于 ＮＵＬＬ 狆＜：Π∧（狇＜：! ∨狇 ≡≡ ＮＵＬＬ）∧犾犲犪犽（狆） ｛Π∧!∧"｝狆＝狇｛Π／狆∧（!＼狆∪｛狆｝）∧"＼狆｝． （ｆ）狆是悬空指针，狇等于 ＮＵＬＬ 狆＜："∧（狇＜：! ∨狇 ≡≡ ＮＵＬＬ） ｛Π∧!∧"｝狆＝狇｛Π∧（! ∪｛狆｝）∧"／狆｝． （２）非指针类型的赋值公理 ｛Ψ∧（犙［狔１←狓］…［狔狀←狓］［狓←犲］）｝狓＝犲｛Ψ∧犙｝ （狔１，狔２，…，狔狀构成犮犾狅狊狌狉犲（狓）的所有成员）． 这是考虑了别名情况后的 Ｈｏａｒｅ逻辑赋值公 理，它不改变 Ψ．该公理中的断言 犙 只含整型数据 的子断言．以下使用的犙 也都满足这个限制． （３）对于指针类型的赋值，若前条件是 Ψ∧犙， 并且犙 中也有访问路径（包括作为犙 中访问路径前 缀的情况），则除了用先前指针赋值的规则外，还需 要用下面的赋值公理． ｛Ψ∧犙｝狆＝狇｛Ψ′∧犙［狉←狆］｝ （狉是犮犾狅狊狌狉犲（狆）中的一个其它成员， Ψ′由（１）的规则从 Ψ 得到）． 换一种说法是，对指针狆 赋值时，对狆 的别名 替换还需要出现在Ψ 以外的断言中．该规则也用在 ｍａｌｌｏｃ和ｆｒｅｅ语句场合． （４）复合、条件和循环语句的规则以及推论规 则等仍然使用 Ｈｏａｒｅ逻辑的规则． （５）分配空间语句狆＝犿犪犾犾狅犮（犜），其中 犜 是类 型．若犜 是结构类型，狉１，狉２，…，狉狀是其中的指针域 在该类型中的访问路径． （ａ）狆是 ＮＵＬＬ指针 狆＜：! ｛Π∧!∧"｝狆＝犿犪犾犾狅犮（犜）｛（Π＋狆）∧!／狆∧ （"∪｛狆－＞狉１，…，狆－＞狉狀｝）｝ ． （ｂ）狆是悬空指针的规则和（ａ）类似． （ｃ）狆是有效指针．把该语句看成语句序列狆＝ ＮＵＬＬ；狆＝犿犪犾犾狅犮（犜），并将相应的规则用于证明． （６）释放空间语句犳狉犲犲（狆） 下面的规则用于狆所指向对象不含有效指针的场 合．若从Π知道狆所指向的对象中含有有效指针狆 －＞ 狉１，…，狆 －＞狉狀，则 可 把 该 语 句 看 成 语 句 序 列 狆 －＞狉１＝ＮＵＬＬ；…；狆 －＞狉狀 ＝ＮＵＬＬ；犳狉犲犲（狆）来 进行证明．这样做的目的是简化犳狉犲犲（狆）的规则． 狆＜：Π ｛Π∧!∧"｝犳狉犲犲（狆）｛（Π－狆）∧ （!／｛狆－＞狉１，…，狆－＞狉狀｝∧（"∪犲狇狌犪犾狊（狆）｝ ． ４ 证明实例 我们已经用指针逻辑系统证明了单链表、双向 链表和二叉树等数据结构的一些函数．本节以删除 二叉排序树一个结点并重接它的左或右子树的函数 ｓｔｒｕｃｔｎｏｄｅ犇犲犾犲狋犲犖狅犱犲（狊狋狉狌犮狋狀狅犱犲 狆）为例． 在证明该函数时，参数所指向的树上，有效指针 和 ＮＵＬＬ 指针的布局是不清楚的，但它必须满足 树的定义．若树结点定义是ｓｔｒｕｃｔｎｏｄｅ｛ｉｎｔ犱犪狋犪； ｓｔｒｕｃｔｎｏｄｅ犾，狉；｝，那么以狆 为根结点指针的树 的定义如下： 狋狉犲犲（狆）｛狆｝犖∨（｛狆｝∧狋狉犲犲（狆－＞犾）∧狋狉犲犲（狆－＞狉））． 如果狆不是空指针，通过下面的演算可以知道狆 是有效指针并且狋狉犲犲（狆－＞犾）∧狋狉犲犲（狆－＞狉）为真： 狋狉犲犲（狆）∧（狆！＝ＮＵＬＬ） ≡（｛狆｝犖∨（｛狆｝∧狋狉犲犲（狆－＞犾）∧狋狉犲犲（狆－＞狉）））∧ （狆！＝ＮＵＬＬ） （｛狆｝犖 ∧（狆！＝ＮＵＬＬ））∨ （｛狆｝∧狋狉犲犲（狆－＞犾）∧狋狉犲犲（狆－＞狉）∧（狆！＝ＮＵＬＬ）） 犳犪犾狊犲∨（｛狆｝∧狋狉犲犲（狆 －＞犾）∧狋狉犲犲（狆 －＞狉）） ｛狆｝∧狋狉犲犲（狆 －＞犾）∧狋狉犲犲（狆 －＞狉）． 程序设计者只要给出函数前后条件和循环不变 ３ 期 陈意云等：一种用于指针程序安全性证明的指针逻辑 ３７７