陈意云等：一种用于指针程序验证的指针逻撰 421 出A9SΨAQ}A9SΨA2,} {AgV平2A22S3AQ3V平：AQ} 其中，S表示PointerC的程序段.Hoare逻辑原本没有这样的规则，因为{x=Ivax==2}这样的前条件虽然也可以看 成两种不同情况，但Hoae逻辑赋值公理可以同时对该析取范式的两个子句进行语法代换， 7)结构规则(frame rule) 为了获得更有效的推理方法，有时需要拆分或合并合法平，若合法乎是SA.ASA人D,H和华分别是 SA..AS入AD和S+1A..AS人M5D,并且一，DAD一D若出对一部分指针类型声明变量来说是合 法的，华对剩余的指针类型声明变量来说是合法的，则称阿拆分成出和华，出和华可合并成平显然，这时有 一平A华.用于局部推理的规则如下： 出AO)SIO HA平2AgΛQ2}SA平2AgAQ2} 其中，出AQ1和AQ2分别都是合法的 例如，在函数调用点，H八Q1和八Q2分别可用来表示和被调用函数有关和无关的部分 2.4函数构造的推理规则 PointerC在第1节的文法基础上还有函数构造，本节讨论指针逻辑有关函数构造的规则.为突出重点并简化 讨论，我们做如下限制或约定： (I)函数∫的声明形式是arg){vardeclist stmtlist),ag是∫唯一的并且是指针类型的参数，vardeclist和 stmtlist是∫的变量声明表和语句表.函数调用语句的形式是re=ac),act是实参.在下面的规则中，y1,,yk表示 函数「声明的所有指针类型局部变量： (2)假定函数体中有一个局部变量res,它和用户声明的任何局部变量都不同名，函数体中的语句return e都 变换成es=e,return res来进行推理，以使return的规则简单 有了函数构造后，合法的检查以按作用域规则可见的全局和局部的指针类型声明变量为基础. 下面仅给出参数和返回值都是指针类型的推理规则，其他情况的规则比这些规则简单递归函数、过程和 递归过程的规则都不难在此基础上得出 1)函数声明 ΨA{y,,k,resinO}stmtlistΨ'AQ {ΨAQ}f(arg){ardeclist stmtlist{Ψ'入Q'} 在%Q的基础上添加{v1·,Vk,es}作为函数语句表的前断言，这是因为这些指针类型局部变量和s在函 数体执行前都被看成悬空指针」 2)函数调用语句 PargO)arg =act))f(arg)vardeclist stmtlistO') A{rei.Oret=f(ac)H(Ψ'Ag)res←re]} 参数为指针类型的函数调用必须体现进入被调用函数时，形参和实参在同一个指针集合中，这是通过在该 规则的前提中显式增加一个指针赋值语句ag:=ac1来体现的对于返回值，也可以用类似的方法来解决在这里 是调用前限制e1为NULL指针，调用后通过代换来使e1出现在断言中 3)return语句 )=NULL()...-=NULLO arg =NULL) oCoreturn res(N+-(v....varg) 函数终止时，指针类型局部变量1，，和形参ag不再能访问，因此应把中有关它们的信息删去 2.5指针逻辑的可靠性 我们己经完成PointerC语言安全性的证明和指针逻辑早先版本对PointerC语言操作语义可靠的证明l], 本文对指针逻辑的完善只影响指针逻辑可靠的证明细节这里概述指针逻辑可靠的证明框架： ©中国科学院软件研究所htp:wwv.c-s-a.org.cn陈意云 等:一种用于指针程序验证的指针逻辑 421 11 3 32 2 4 4 112 2 3 3 4 4 { } { }{ } { } { }{ } QS Q QS Q Q QS Q Q Ψ ΨΨ Ψ ΨΨ Ψ Ψ ∧ ∧∧ ∧ ∧∨ ∧ ∧∨ ∧ , 其中,S 表示 PointerC 的程序段.Hoare 逻辑原本没有这样的规则,因为{x==1∨x==2}这样的前条件虽然也可以看 成两种不同情况,但 Hoare 逻辑赋值公理可以同时对该析取范式的两个子句进行语法代换. 7) 结构规则(frame rule) 为了获得更有效的推理方法,有时需要拆分或合并合法Ψ.若合法Ψ是S1∧…∧Sn∧N∧D,Ψ1 和Ψ2 分别是 S1∧…∧Si∧N1∧D1 和Si+1∧…∧Sn∧N2∧D2,并且N1∧N2⇔N,D1∧D2⇔D,若Ψ1 对一部分指针类型声明变量来说是合 法的,Ψ2 对剩余的指针类型声明变量来说是合法的,则称Ψ可拆分成Ψ1 和Ψ2,Ψ1 和Ψ2 可合并成Ψ.显然,这时有 Ψ⇔Ψ1∧Ψ2.用于局部推理的规则如下: 1 11 1212 1212 { }{ } { }{ } QS Q Q QS Q Q Ψ Ψ ΨΨ ΨΨ ∧ ∧′ ′ ∧∧∧ ∧∧∧ ′ ′ , 其中,Ψ1∧Q1 和Ψ2∧Q2 分别都是合法的. 例如,在函数调用点,Ψ1∧Q1 和Ψ2∧Q2 分别可用来表示和被调用函数有关和无关的部分. 2.4 函数构造的推理规则 PointerC在第 1 节的文法基础上还有函数构造,本节讨论指针逻辑有关函数构造的规则.为突出重点并简化 讨论,我们做如下限制或约定: (1) 函数 f 的声明形式是 f(arg){vardeclist stmtlist},arg 是 f 唯一的并且是指针类型的参数,vardeclist 和 stmtlist 是 f 的变量声明表和语句表.函数调用语句的形式是 ret=f(act),act 是实参.在下面的规则中,v1,…,vk 表示 函数 f 声明的所有指针类型局部变量; (2) 假定函数体中有一个局部变量 res,它和用户声明的任何局部变量都不同名,函数体中的语句 return e 都 变换成 res=e;return res 来进行推理,以使 return 的规则简单. 有了函数构造后,合法Ψ的检查以按作用域规则可见的全局和局部的指针类型声明变量为基础. 下面仅给出参数和返回值都是指针类型的推理规则,其他情况的规则比这些规则简单.递归函数、过程和 递归过程的规则都不难在此基础上得出. 1) 函数声明 1 { { ,..., , } } { } { } (arg){ }{ } k v v res Q stmtlist Q Q f vardeclist stmtlist Q Ψ Ψ Ψ Ψ ∧ ∧∧′ ′ ∧ ∧′ ′ D . 在Ψ∧Q 的基础上添加{v1,…,vk,res}D作为函数语句表的前断言,这是因为这些指针类型局部变量和 res 在函 数体执行前都被看成悬空指针. 2) 函数调用语句 { {arg} }arg : { } { } (arg){ }{ } . { { } } ( ){( [ } ) ] D Q act Q Q f vardeclist stmtlist Q ret Q ret f act Q res ret Ψ Ψ Ψ Ψ Ψ Ψ 11 11 ∧∧=∧ ∧ ∧′ ′ ∧ ∧= ∧ ← ′ ′ N 参数为指针类型的函数调用必须体现进入被调用函数时,形参和实参在同一个指针集合中,这是通过在该 规则的前提中显式增加一个指针赋值语句 arg:=act 来体现的.对于返回值,也可以用类似的方法来解决.在这里 是调用前限制 ret 为 NULL 指针,调用后通过代换来使 ret 出现在断言中. 3) return 语句 0 01 1 1 1 1 1 1 00 1 11 1 1 { } { }...{ } { } { } { } { ( { ,..., , }) } k kk k k k k k k k kk Q v NULL Q Q v NULL Q arg NULL Q Q return res v v arg Q Ψ ΨΨ Ψ Ψ Ψ Π −− ++ + + ++ ∧= ∧ ∧ = ∧ = ∧ ∧ ∧ − ∧∧ N D . 函数终止时,指针类型局部变量 v1,…,vk 和形参 arg 不再能访问,因此应把Ψ中有关它们的信息删去. 2.5 指针逻辑的可靠性 我们已经完成 PointerC 语言安全性的证明和指针逻辑早先版本对 PointerC 语言操作语义可靠的证明[13], 本文对指针逻辑的完善只影响指针逻辑可靠的证明细节.这里概述指针逻辑可靠的证明框架: