.OX=EAemp=Eemppl (ASSN) OkE1→-→E2=E2 10rE1→-J[E]:=1OrE1→(s xOFx=XAEH刀x=[E]x,OFx=YALXIIE→7D) Edispase(E)O empp (sP) (x,Ox=XAemph)=E1E1 A...AEk Ek (CONs) (x,Ox=X Aempnlx :cons(E1.....Ek)x.x=YA(Y [X/x]E1 +...Y+k-1[X/x]En)] 川skip(skP) (p)Cp)(p')C2 (sE) P→B=BpA卧C1pA-BC2@m {pC1:C2{q} (p)if B then C1 else C2 q) p→B=B{pABC{Pl (WHILE) p→ppC{g1q→g Ip]Clgl (CONSEQ) (FRM) {p)while B do C{p∧-B Ip]C lal (p*r)Clq+r] Ip)Clgl Ip')Clg'] (p)C igl (p')Cl'] Ip)Clgl (CONJ) (DISJ) (EXISTS) ipAp']Clgng'l Ipvp']clqvg'l (3x.p)Cax.gl Figure 12.Inference Rules-Sequential Rules Ip)Cla) Emp:Emp:empC(ENV) R:G:1-(p)C R:G:IC2(-E) R:G:I-(p)C1:C2(r) p→B=B{PAB]C{q}Sta(lp,ql,R*ld)pxq→G*True pvq→I*true I{R,Gl R:G:I(p]atomic(B)(C)q) (ATOMIC) P→B=B1RG:I-ipABCipl(wmE P→(B=B)*/RG:IpAB卧CgRG:IEIPA-C2@-时 R;G:Ip)while B do CpA-B) R:G:I(p]if B then C1 else C2 q) RVG2:G1:IHp1*r)C1 lqi+r)RVG1:G2:I+(p+r)C2g*r rvnvr=I IR -(PAR) R:GIVG2:IHIp1*p2+r)Cillc2(q*2*(r1Ar)) R:G:I-(p)C (q)Sta(r.R'+ld)I'(R',G']rI'*true R+R':G+G':I+I(p]C(g)I(R.G] ·(FRAME) R+R':G*G':I+I'(p*r)Cq*r R:G:1-p)C (q] (HIDE) R:G:I(p)C lg) R:G:IHp)Clgl R:G:IHp)C lgl X not free in R.G.and I R;G;IHp']Clg R:G:I-p')C) R:G:I p C(-Ex) (P-CONJ) R:G:IF(pAp']Clqg'l R:G:I-(pvp']Clgvgl (P-DISJ) p'→pR→RG→G'q→g4R:GI{plC{qlp'vg→'*tue'{R,G R':G':I'(p')C') (cso) Figure 13.Inference Rules for Concurrency (p]C (q)Sta(r,R+ld)I (R.G)rI+true (ENV-SHARE) R:;G:ILp*r}C{q*r川 R:G:I-p)C(g) R:G:I(p)Clql Sta(r,R')I'R',G']rI' R:G;Ih{p*rlC{q*r月 (FR-PRIVATE) (FR-SHARE) R*R';G*G';II'H(p*r)Clg*r (RVG2)*G5:G1*G:I*'上{p1*m*r1C1{q1*叫*了) (RVG1)*G:G2*G2:1I'pmrC21g2*m IR,G1,G2}I'G,C}rvrV→1 mV m Vm→r (PAR-HIDE) R:G1 VG2:I-(p1 *p2+m+r)Cillc2 (q1*q2*(mj Am2)*(r) Figure 14.Useful Derived Rules 9{x,O X = E ∧emph} x := E {x,O x = X ∧emph} (assn) O E1 → ⇒ E2 = E2 {O E1 → } [E1] := E2 {O E1 → E2} (st) {x,O x = X ∧E → Y} x := [E] {x,O x = Y ∧[X/x]E → Y} (ld) {O E → } dispose(E) {O emph} (disp) (x,O x = X ∧emph) ⇒ E1 = E1 ∧···∧Ek = Ek {x,O x = X ∧emph} x := cons(E1,...,Ek) {x,O x = Y ∧(Y → [X/x]E1 ∗ ...Y+k−1 → [X/x]En)} (cons) {p} skip {p} (skip) {p} C1 {p } {p } C2 {q} {p} C1;C2 {q} (seq) p ⇒ B = B {p∧ B} C1 {q} {p∧ ¬B} C2 {q} {p} if B then C1 else C2 {q} (if) p ⇒ B = B {p∧ B} C {p} {p} while B do C {p∧ ¬B} (while) p ⇒ p {p } C {q } q ⇒ q {p} C {q} (conseq) {p} C {q} {p ∗ r} C {q ∗ r} (frm) {p} C {q} {p } C {q } {p∧ p } C {q∧q } (conj) {p} C {q} {p } C {q } {p∨ p } C {q∨q } (disj) {p} C {q} {∃X.p} C {∃X.q} (exists) Figure 12. Inference Rules — Sequential Rules {p} C {q} Emp; Emp; emp  {p} C {q} (env) R; G; I  {p} C1 {q} R; G; I  {q} C2 {r} R; G; I  {p} C1;C2 {r} (p-seq) p ⇒ B = B {p∧ B} C {q} Sta({p,q},R∗ Id) p  q ⇒ G ∗True p∨q ⇒ I ∗ true I {R,G} R; G; I  {p} atomic(B){C} {q} (atomic) p ⇒ (B = B) ∗ I R; G; I  {p∧ B} C {p} R; G; I  {p} while B do C {p∧ ¬B} (p-while) p ⇒ (B = B) ∗ I R; G; I  {p∧ B} C1 {q} R; G; I  {p∧ ¬B} C2 {q} R; G; I  {p} if B then C1 else C2 {q} (p-if) R∨G2; G1; I  {p1 ∗ r} C1 {q1 ∗ r1} R∨G1; G2; I  {p2 ∗ r} C2 {q2 ∗ r2} r∨r1 ∨r2 ⇒ I I R R; G1 ∨G2; I  {p1 ∗ p2 ∗ r} C1 C2 {q1 ∗ q2 ∗ (r1 ∧r2)} (par) R; G; I  {p} C {q} Sta(r,R ∗ Id) I {R ,G } r ⇒ I ∗ true R∗R ; G ∗G ; I ∗ I  {p ∗ r} C {q ∗ r} (frame) R∗R ; G ∗G ; I ∗ I  {p} C {q} I {R,G} R; G; I  {p} C {q} (hide) R; G; I  {p} C {q} X not free in R,G, and I R; G; I  {∃X. p} C {∃X. q} (p-ex) R; G; I  {p} C {q} R; G; I  {p } C {q } R; G; I  {p∧ p } C {q∧q } (p-conj) R; G; I  {p} C {q} R; G; I  {p } C {q } R; G; I  {p∨ p } C {q∨q } (p-disj) p ⇒ p R ⇒ R G ⇒ G q ⇒ q R; G; I  {p} C {q} p ∨q ⇒ I ∗ true I {R ,G } R ; G ; I  {p } C {q } (csq) Figure 13. Inference Rules for Concurrency {p} C {q} Sta(r,R∗ Id) I {R,G} r ⇒ I ∗ true R; G; I  {p ∗ r} C {q ∗ r} (env-share) R; G; I  {p} C {q} R; G; I  {p ∗ r} C {q ∗ r} (fr-private) R; G; I  {p} C {q} Sta(r,R ) I {R ,G } r ⇒ I R∗R ; G ∗G ; I ∗ I  {p ∗ r} C {q ∗ r} (fr-share) (R∨G2) ∗G 2; G1 ∗G 1; I ∗ I  {p1 ∗m∗ r} C1 {q1 ∗m 1 ∗ r 1} (R∨G1) ∗G 1; G2 ∗G 2; I ∗ I  {p2 ∗m∗ r} C2 {q2 ∗m 2 ∗ r 2} I {R,G1,G2} I {G 1,G 2} r∨r 1 ∨r 2 ⇒ I m∨m 1 ∨m 2 ⇒ I R; G1 ∨G2; I  {p1 ∗ p2 ∗m∗ r} C1 C2 {q1 ∗ q2 ∗ (m 1 ∧m 2) ∗ (r 1 ∧r 2)} (par-hide) Figure 14. Useful Derived Rules 9