336 Journal of Software软件学报Vol.2l,No.2,February2010 足安全程序的最基本要求，例如，malloc任何一次调用都能成功并且所分配空间同尚未释放空间无任何重叠.另 外，PointerC中允许布尔表达式，但不采用短路计算，以方便它们出现在断言中，因为短路的“与”和“或”运算都不 是可交换运算 在原有的为PointerC语言设计的指针逻辑中，使用指针集合表示内存状态.我们设计了3种指针类型访问 路径的集合：表示NULL指针集合的W、表示悬空指针集合的D以及表示一组有效指针集合的7.I中的每个 集合表示在某程序点处一组指向同一个对象的指针（即右值相等的指针类型访问路径），并且，Ⅱ中不同集合的 指针指向不同对象 我们可以用指针逻辑所定义的访问路径集合实现数据结构的归纳定义.例如，二叉树可以如下定义： tree(s)s(siAtree(s->DAtree(s->r)). 其中，s是指向struct BTNode{struct BTNode*r,*l,}类型的指针，{s}w表示空树.另一种情况{s}Aree(s->)A te(s->r)表示非空树，并且表达出该树上的指针都不相等.因为若把归纳定义的引用展开，则代表有效指针的各 访问路径都在的不同集合中 1.2相等关系不确定的访问路径集合 在图等数据结构中，指针相等与否并无规律，即有效指针的相等关系存在不确定的情况.原有的指针逻辑难 以描述这种指针相等关系不确定的数据结构，因此，我们在原有的指针逻辑的基础上增加相等关系不确定的指 针类型访问路径的一组集合，用以表示在语义模型上，以中的每个集合表示在某程序点处一组指向同一个对象 的指针，但是与Ⅱ不同的是，∥中不同集合的指针可能指向同一对象.Ⅱ和∥中各集合内的指针都称为有效指 针.用平作为W,D,Π，∥的总称注意，虽然我们称其为相等关系不确定的访问路径集合，但是所谓的不确定性仅 存在于这种集合之间，而每个集合内的指针都是确定相等的这种做法可以理解为放宽了原先对Ⅱ集合的要求. 并非任意一组指针类型访问路径经随意划分形成的都能表达上面的意思因此，我们需要定义能够描述 数据结构的合法的平.引入∥集合后，需要在原有的合法的定义的基础上，考虑∥中访问路径的特点，如∥中 访问路径以Π或以中的访问路径为前缀等，以及以中的集合与其他集合之间的关系，如Π中访问路径的前缀不 会在∥中等 首先需要扩展访问路径的别名的定义，以处理增加的∥集合.出现在Ⅱ或∥的同一个集合中的各访问路径 加上同一后缀形成的访问路径互为别名按此定义，判断两条访问路径是否互为别名的谓词如下： aliast(p,q)兰p=qv3s.3r.31.(s不是空串r和1属于或∥中的同一集合p=(p's)Aq=(gs)Kalias(p,r)Kalias(g,). 其中，=表示语法上相同，“”表示串并置该定义是说，若p和q不相同，则忽略相同后缀s之后，判断它们的别名是 否出现在Ⅱ或∥中的同一个集合中若递归计算时出现再次判断p和q是否为别名，则计算不终止，这时也认为 p和q不是别名.该谓词和文献[5]中的谓词有不同的表现：由于∥中指针相等关系不确定，∥中不同集合的指针 也可能互为别名因此，该谓词可靠但不完备，不过它不影响下面的合法的定义 扩展后的合法需要满足下面几个条件： (1)所有声明为指针类型的变量都在中 (2)对Ⅱ中的任何访问路径p,若p所指向的结构类型有指针类型域r,则p->r的某个别名在中. (3)对Π，W和D中的任何访问路径，Ⅱ，W和D中的任何其他访问路径都不是它的别名. (4)若访问路径p在中，则对p的每个前缀，它的一个别名在Π或∥中 (⑤)对M中的任何访问路径p,若p所指向的结构类型有指针类型域r,则p->r的某个别名在∥，W或D中 1.3断言语言的扩展 我们在原有的指针逻辑1的断言语言基础上作出扩展，以支持引入从集合.另外，还需要在允许描述两个指 针相等或不相等关系基础上，增加表达∥中的一个指针不从属其他∥集合的断言，以表达己知的∥中不同集合 的指针之间的不相等关系， 扩展后的断言语言如下： ©中国科学院软件研究所 http://www.c-s-a.org.cn336 Journal of Software 软件学报 Vol.21, No.2, February 2010 足安全程序的最基本要求,例如,malloc 任何一次调用都能成功并且所分配空间同尚未释放空间无任何重叠.另 外,PointerC 中允许布尔表达式,但不采用短路计算,以方便它们出现在断言中,因为短路的“与”和“或”运算都不 是可交换运算. 在原有的为PointerC语言设计的指针逻辑[5]中,使用指针集合表示内存状态.我们设计了 3 种指针类型访问 路径的集合:表示 NULL 指针集合的N 、表示悬空指针集合的D以及表示一组有效指针集合的Π .Π 中的每个 集合表示在某程序点处一组指向同一个对象的指针(即右值相等的指针类型访问路径),并且,Π 中不同集合的 指针指向不同对象. 我们可以用指针逻辑所定义的访问路径集合实现数据结构的归纳定义.例如,二叉树可以如下定义: tree(s){s}N∨({s}∧tree(s->l)∧tree(s->r)), 其中,s是指向struct BTNode{struct BTNode *r,*l;}类型的指针,{s}N表示空树.另一种情况{s}∧tree(s->l)∧ tree(s->r)表示非空树,并且表达出该树上的指针都不相等.因为若把归纳定义的引用展开,则代表有效指针的各 访问路径都在Π的不同集合中. 1.2 相等关系不确定的访问路径集合 在图等数据结构中,指针相等与否并无规律,即有效指针的相等关系存在不确定的情况.原有的指针逻辑难 以描述这种指针相等关系不确定的数据结构,因此,我们在原有的指针逻辑的基础上增加相等关系不确定的指 针类型访问路径的一组集合,用U 表示.在语义模型上,U 中的每个集合表示在某程序点处一组指向同一个对象 的指针,但是与Π 不同的是,U 中不同集合的指针可能指向同一对象.Π 和U 中各集合内的指针都称为有效指 针.用Ψ作为N ,D ,Π ,U 的总称.注意,虽然我们称其为相等关系不确定的访问路径集合,但是所谓的不确定性仅 存在于这种集合之间,而每个集合内的指针都是确定相等的.这种做法可以理解为放宽了原先对Π 集合的要求. 并非任意一组指针类型访问路径经随意划分形成的Ψ都能表达上面的意思.因此,我们需要定义能够描述 数据结构的合法的Ψ.引入U 集合后,需要在原有的合法Ψ的定义[5]的基础上,考虑U 中访问路径的特点,如U 中 访问路径以Π 或U 中的访问路径为前缀等,以及U 中的集合与其他集合之间的关系,如Π 中访问路径的前缀不 会在U 中等. 首先需要扩展访问路径的别名的定义,以处理增加的U 集合.出现在Π 或U 的同一个集合中的各访问路径 加上同一后缀形成的访问路径互为别名.按此定义,判断两条访问路径是否互为别名的谓词如下: alias(p,q)p≡q∨∃s.∃r.∃t.(s 不是空串∧r 和 t 属于Π或U 中的同一集合∧p≡(p′⋅s)∧q≡(q′⋅s)∧alias(p′,r)∧alias(q′,t)). 其中,≡表示语法上相同,“⋅”表示串并置.该定义是说,若 p 和 q 不相同,则忽略相同后缀 s 之后,判断它们的别名是 否出现在Π 或U 中的同一个集合中.若递归计算时出现再次判断 p 和 q 是否为别名,则计算不终止,这时也认为 p 和 q 不是别名.该谓词和文献[5]中的谓词有不同的表现:由于U 中指针相等关系不确定,U 中不同集合的指针 也可能互为别名.因此,该谓词可靠但不完备,不过它不影响下面的合法Ψ的定义. 扩展后的合法Ψ需要满足下面几个条件: (1) 所有声明为指针类型的变量都在Ψ中. (2) 对Π 中的任何访问路径 p,若 p 所指向的结构类型有指针类型域 r,则 p->r 的某个别名在Ψ中. (3) 对Π ,N 和D 中的任何访问路径,Π ,N 和D 中的任何其他访问路径都不是它的别名. (4) 若访问路径 p 在Ψ中,则对 p 的每个前缀,它的一个别名在Π 或U 中. (5) 对U 中的任何访问路径 p,若 p 所指向的结构类型有指针类型域 r,则 p->r 的某个别名在U ,N 或D 中. 1.3 断言语言的扩展 我们在原有的指针逻辑[5]的断言语言基础上作出扩展,以支持引入U 集合.另外,还需要在允许描述两个指 针相等或不相等关系基础上,增加表达U 中的一个指针不从属其他U 集合的断言,以表达已知的U 中不同集合 的指针之间的不相等关系. 扩展后的断言语言如下: