A:10 Hongjin Liang et al. 0 B R RMl (a)a-Related Transitions (b)The Side Condition of TRANS Fig.4.Related Transitions 4.1.The Definition Our co-inductively defined RGSim relation is in the form of (C,o,R,9) (C,E,R,G),which is a simulation between program configurations(C,o)and(C,>)It is parametrized with the rely and guarantee conditions at the low level and the high level,which are binary relations over states: R,gE P(LState x LState),R,G E P(HState x HState). The simulation also takes two additional parameters:the step invariant a and the post- condition y,which are both relations between the low-level and the high-level states. a,Y E P(LState x HState). Before we formally define RGSim in Definition 4.2,we first introduce the a-related transitions as follows. Definition 4.1 (a-Related Transitions). (R,)a{(a,σ)，(E,)|(o,σ)∈RA(E,)∈RA(o,)∈aA(σ，)∈a}. (R,R)represents a set of the a-related transitions in R and R,putting together the corresponding transitions in R and R that can be related by a,as illustrated in Fig- ure 4(a).(g,G)is defined in the same way. Definition 4.2 (RGSim).Whenever (C,o,R,g):(C,,R,G),then (o,>)Ea and the following are true: (1)if (C,)>(C,'),then there exist C'and >such that (C,)-→*(C,),(a,o),(②，)∈(g,G）aand(C,o,R,g)≤an(C,y,R,G (2)if (C,)(C,o'),then there exist C'and such that (C,)e,*(C','),(o,o),(E,)∈(G,G）aand(C,o',R,g)≤ay(C,',R,G； (3)if C=skip,then there exists >such that (C,)-→*(skip,),(a,o),(,)∈(g,G*〉a,(a,)∈y andy≤a; (4)if(C,o)-→abort,then(C,)-→*abort; (⑤)if(o,a),(∑，)∈(R,R*)a,then(C,o',R,g)≤a(C,',R,G). Then,(C,R,g):(C,R,G)iff for all o and if (,)then (C.,R,g)(C.,R.G).Here the precondition E P(LState x HState)is used to relate the initial states o and > Informally,(C,a,R,g)(C,R,G)says the low-level configuration (C,o)is sim- ulated by the high-level configuration(C,>)with behaviors g and G respectively,no matter how their environments R and R interfere with them.It requires the following hold for every execution of C: ACM Transactions on Programming Languages and Systems,Vol.V,No.N,Article A,Publication date:January YYYY.A:10 Hongjin Liang et al. σ σ ′ Σ Σ ′ α ❄ R α ❄ R σ σ ′ θ θ ′ Σ Σ ′ α β ❄ R ❄ RM ❄ R ∗ α β (a) α-Related Transitions (b) The Side Condition of TRANS Fig. 4. Related Transitions 4.1. The Definition Our co-inductively defined RGSim relation is in the form of (C, σ, R, G) ≼α;γ (C, Σ, R, G), which is a simulation between program configurations (C, σ) and (C, Σ). It is parametrized with the rely and guarantee conditions at the low level and the high level, which are binary relations over states: R, G ∈ P(LState × LState), R, G ∈ P(HState × HState). The simulation also takes two additional parameters: the step invariant α and the post￾condition γ, which are both relations between the low-level and the high-level states. α, γ ∈ P(LState × HState). Before we formally define RGSim in Definition 4.2, we first introduce the α-related transitions as follows. Definition 4.1 (α-Related Transitions). ⟨R, R⟩α , {((σ, σ′ ),(Σ, Σ ′ )) | (σ, σ′ ) ∈ R ∧ (Σ, Σ ′ ) ∈ R ∧ (σ, Σ) ∈ α ∧ (σ ′ , Σ ′ ) ∈ α} . ⟨R, R⟩α represents a set of the α-related transitions in R and R, putting together the corresponding transitions in R and R that can be related by α, as illustrated in Fig￾ure 4(a). ⟨G, G⟩α is defined in the same way. Definition 4.2 (RGSim). Whenever (C, σ, R, G) ≼α;γ (C, Σ, R, G), then (σ, Σ) ∈ α and the following are true: (1) if (C, σ) −→ (C ′ , σ′ ), then there exist C ′ and Σ ′ such that (C, Σ) −→∗ (C ′ , Σ ′ ), ((σ, σ′ ),(Σ, Σ ′ )) ∈ ⟨G, G∗ ⟩α and (C ′ , σ′ , R, G) ≼α;γ (C ′ , Σ ′ , R, G); (2) if (C, σ) e −→ (C ′ , σ′ ), then there exist C ′ and Σ ′ such that (C, Σ) e −→∗ (C ′ , Σ ′ ), ((σ, σ′ ),(Σ, Σ ′ )) ∈ ⟨G, G∗ ⟩α and (C ′ , σ′ , R, G) ≼α;γ (C ′ , Σ ′ , R, G); (3) if C = skip, then there exists Σ ′ such that (C, Σ) −→∗ (skip, Σ ′ ), ((σ, σ),(Σ, Σ ′ )) ∈ ⟨G, G∗ ⟩α, (σ, Σ ′ ) ∈ γ and γ ⊆ α; (4) if (C, σ) −→ abort, then (C, Σ) −→∗ abort; (5) if ((σ, σ′ ),(Σ, Σ ′ )) ∈ ⟨R, R ∗ ⟩α, then (C, σ′ , R, G) ≼α;γ (C, Σ ′ , R, G). Then, (C, R, G) ≼α;ζnγ (C, R, G) iff for all σ and Σ, if (σ, Σ) ∈ ζ, then (C, σ, R, G) ≼α;γ (C, Σ, R, G). Here the precondition ζ ∈ P(LState × HState) is used to relate the initial states σ and Σ. Informally, (C, σ, R, G) ≼α;γ (C, Σ, R, G) says the low-level configuration (C, σ) is sim￾ulated by the high-level configuration (C, Σ) with behaviors G and G respectively, no matter how their environments R and R interfere with them. It requires the following hold for every execution of C: ACM Transactions on Programming Languages and Systems, Vol. V, No. N, Article A, Publication date: January YYYY