Front.Comput.Sci.China(2007),Research Article 7 expansion(S) if 3s':(IIUNUD)).(Sns'!=0) then let [p1,...Pn}=S-S where S'∈（ⅡU{W}U{D})ASnS'I=0 in SUclosure(p)U...Uclosure(pn) else 0. Function compression(S)deletes all the cyclic access paths from the alias set S,and its formal definition is: compression(S)≌S-S' where (S'CS)A ((s1lls2lls3)ES' f(s1！=e)∧(s2!=e)∧(s多！=e)Λ(sls3)∈S)A(sls2=s1) For brevity,the above function closure is a definition,not a computing al- gorithm.For example,it does not consider the termination of the calculation concerning cyclic data structures,such as doubly-linked cyclic list.But,in the implementation of closure,it is easy to solve the problem of termination.And given the closure function,it is also simple to delete cycles from the access paths. So for convenience,it is assumed that all access paths in programs have the sim- plest form. 2)Function alias(p,q)gets an alias of p from the closure of access path p.The alias it gets must not use any alias of effective pointer q as a prefix.If there is no such an alias,it returns p. alias(p,q) let S=[p'closure(p)I Vq'closure(q).-prefix(q',p)} in if S==0 then p else p'where p'S 3)Function equals(p)gets the equivalent set of p.If one of the aliases of p appears in an equivalent set,the function returns the set,or else it returns empty set. equals(p)≌ if3S:Ⅱ.(Snclosure(p)！=0) then S where S∈ⅡA Sn closure(p)！=0else0 Next,we introduce the operations and predicates directly used in inference rules. These operations show how to get the in a postcondition based on the in the corresponding precondition. 4)Suppose S is an equivalent set in I7,and p is an effective pointer.For each pointer q in S which uses one of p's aliases as its prefix,S/p finds an alias of q using alias(q,p),substitutes the alias for q in S,and then deletes p's aliases and any other pointers which use p's aliases as their prefixes from S. S/p≌ let S'={q:S Vp'closure(p).-prefix(p',q) [3q:S.3p closure(p).(prefix(p',q)=alias(q,p))} in {q:S'(qE closure(p))AVp':closure(p).-prefix(p',q)}Front. Comput. Sci. China (2007), Research Article 7 expansion(S) , if ∃S0 : (Π ∪ {N } ∪ {D}).(S ∩ S0!=∅) then let {p1 , . . . , pn} = S 0 − S where S 0 ∈ (Π ∪ {N } ∪ {D}) ∧ S ∩ S0!=∅ in S ∪ closure(p1 ) ∪ . . . ∪ closure(pn) else ∅. Function compression(S) deletes all the cyclic access paths from the alias set S, and its formal definition is: compression(S) , S − S0 where (S 0 ⊂ S) ∧ ((s1||s2||s3) ∈ S0 iff (s1!=²) ∧ (s2!=²) ∧ (s3!=²) ∧ ((s1||s3) ∈ S) ∧ (s1||s2 = s1)) For brevity, the above function closure is a definition, not a computing al￾gorithm. For example, it does not consider the termination of the calculation concerning cyclic data structures, such as doubly-linked cyclic list. But, in the implementation of closure, it is easy to solve the problem of termination. And given the closure function, it is also simple to delete cycles from the access paths. So for convenience, it is assumed that all access paths in programs have the sim￾plest form. 2) Function alias(p, q) gets an alias of p from the closure of access path p. The alias it gets must not use any alias of effective pointer q as a prefix. If there is no such an alias, it returns p. alias(p, q) , let S = {p 0 : closure(p) | ∀q 0 : closure(q).¬prefix(q 0 , p 0 )} in if S == ∅ then p else p 0 where p 0 ∈ S 3) Function equals(p) gets the equivalent set of p. If one of the aliases of p appears in an equivalent set, the function returns the set, or else it returns empty set. equals(p) , if ∃S : Π.(S ∩ closure(p)!=∅) then S where S ∈ Π ∧ S ∩ closure(p)!=∅ else ∅ Next, we introduce the operations and predicates directly used in inference rules. These operations show how to get the Ψ in a postcondition based on the Ψ in the corresponding precondition. 4) Suppose S is an equivalent set in Π, and p is an effective pointer. For each pointer q in S which uses one of p’s aliases as its prefix, S/p finds an alias of q using alias(q,p), substitutes the alias for q in S, and then deletes p’s aliases and any other pointers which use p’s aliases as their prefixes from S. S/p , let S 0 = {q : S | ∀p 0 : closure(p).¬prefix(p 0 , q)}∪ {q 0 | ∃q : S.∃p 0 : closure(p).(prefix(p 0 , q) ∧ q 0 ≡ alias(q, p))} in {q : S 0 | ¬(q ∈ closure(p)) ∧ ∀p 0 : closure(p).¬prefix(p 0 , q)}