Front.Comput.Sci.China (2007),Research Article 9 In each of the following rules,the premises of the rule should be computed based on the y before the statement. 1)Pointer assignment:p=q. Here different inference rules are used in different cases. a)Both p and q are effective pointers or null pointers,and they are equal(in- cluding the case where p is a null pointer and g is constant NULL). (p.eq!=0A p==q)V(p==NULL A q==NULL) (RULE 1) [IIANAD}P=q(IIANAD) b)Both p and q are effective pointers,and they are not equal. (p.eq!=0∧q.eq!=0∧p！=q)∧no_leak(p) [IIANAD}p=q {((II-{q.eq})/pu{q.eq/pu(p)})ANpAD\p} (RULE2)】 c)p is a null pointer and q is an effective pointer. p==NULL∧q.eq！=0 [IAN A D}p=q{((II-{q.eq})ufq.equ(p)))AN/p D] (RULE3) d)p is a dangling pointer and q is an effective pointer. The rule for this case is similar to(RULE 3). e)p is an effective pointer and q equals NULL (including the case where q is constant NULL). p.eq!=0A q==NULL A no_leak(p) (RULE 4) (IIANAD}p=q {I/PA(NPU(p))AD\p} f)p is a dangling pointer and q equals NULL (including the case where q is constant NULL). p:DA q==NULL (RULE 5) IIANAD)p=q (II(NUp))AD/p} where p:D represents that an alias of p is in D 2)The assignment axiom for non-pointer-type data is as follows.It is an exten- sion of Hoare logic assignment axiom,and aliasing has been considered in this axiom.The axiom does not interfere with {(亚AQ)y1-.[yn←-xx←}x=e{亚AQ}(AXIOM6-1) where y1,...,yn represent all the members of closure(x).Front. Comput. Sci. China (2007), Research Article 9 In each of the following rules, the premises of the rule should be computed based on the Ψ before the statement. 1) Pointer assignment: p=q. Here different inference rules are used in different cases. a) Both p and q are effective pointers or null pointers, and they are equal (in￾cluding the case where p is a null pointer and q is constant NULL). (p.eq!=∅ ∧ p==q) ∨ (p==NULL ∧ q==NULL) {Π ∧ N ∧ D} p=q {Π ∧ N ∧ D} (rule 1) b) Both p and q are effective pointers, and they are not equal. (p.eq!=∅ ∧ q.eq!=∅ ∧ p!=q) ∧ no leak(p) {Π ∧ N ∧ D} p=q {((Π − {q.eq})/p ∪ {q.eq/p ∪ {p}}) ∧ N \p ∧ D\p} (rule 2) c) p is a null pointer and q is an effective pointer. p==NULL ∧ q.eq!=∅ {Π ∧ N ∧ D} p=q {((Π − {q.eq}) ∪ {q.eq ∪ {p}}) ∧ N /p ∧ D} (rule 3) d) p is a dangling pointer and q is an effective pointer. The rule for this case is similar to (RULE 3). e) p is an effective pointer and q equals NULL (including the case where q is constant NULL). p.eq!=∅ ∧ q==NULL ∧ no leak(p) {Π ∧ N ∧ D} p=q {Π/p ∧ (N \p ∪ {p}) ∧ D\p} (rule 4) f) p is a dangling pointer and q equals NULL (including the case where q is constant NULL). p : D ∧ q==NULL {Π ∧ N ∧ D} p=q {Π ∧ (N ∪ {p}) ∧ D/p} (rule 5) where p : D represents that an alias of p is in D 2) The assignment axiom for non-pointer-type data is as follows. It is an exten￾sion of Hoare logic assignment axiom, and aliasing has been considered in this axiom. The axiom does not interfere with Ψ. {(Ψ ∧ Q)[y1 ← x] . . . [yn ← x][x ← e]} x=e {Ψ ∧ Q} (axiom 6-1) where y1, . . . , yn represent all the members of closure(x)