RV G2,G1,H[P*P)C13C1{Q1*Q}RVG1,G2,IH{P2+P)C23C2[Q2+Q2}PVQIVQ2I IDR R,GIVG2,IH(P+P2*P)C1lC23C1C2{Q1+Q2*(Q1AQ2)} (B-PAR) P÷(B÷B)*IR,G,IF{PAB}C<C{P P=(E=E)*I Sta(P,R*ld)IR,G} ·(B-WHLE) .(B-PRT) R,G,IH{P)while (B)C<while (B)CfPA-B) R,G,IFPprint(E)<print(E)P R,G,IF{P}C≤C{Q}Sta(P,*ld)I'p{R,G}P→I'*tueG+→G -(B-FRAME) R*R,G*G,I*IHP*P)C<CIQ*P Figure 7.Selected binary inference rules (compositionality of RGSim-T). Adequacy. RGSim-T ensures the termination-preserving refine- w∈NatD:=Cl● ment by using the metric with a well-founded order.The proof of the following adequacy theorem is in TR [13]. (o,D,D.)=P iff (o,P Theorem 3(Adequacy of RGSim-T).If there exist R.G.I.Q (a,w,D)arem(C')iff D=C and a metric M(with a well-founded order<)such that R.G.IE ((s,h),w,D,wf(E)iff 3n.(Els =n)A (n<w) (C,a,M)(C,)then (C,)(C,). (a,w,D,)卡p fD.(o,w,D,)上p (o,w,D,)p]w if3.(a,w,D,)上p 4.3 Compositionality Rules (o,)Flpll f3u,D.(o,0,D,)乍p RGSim-T is compositional.We show some of the compositionality rules in Fig.7.Here we use R.G.IP)C CO}for the D1⊥D2iff(D1=)V(D2=·) D1出D2些D2ifD1=· D1ifD2=● judgment to emphasize syntactic reasoning,whose semantics is RGSim-T(Def.2).The rules can be viewed as the binary version (o1,w1,D1,1)出(a2,w2,D2,2)警 of those in a traditional rely-guarantee-style logic (e.g.,LRG [3] (a1出2，w1+w2,D1出D2,1世∑2)，ifa1⊥a2,D1⊥D2and∑1⊥∑2 and RGSep [23]). The B-PAR rule shows the compositionality w.r.t.parallel com- Sta(p,R)ifa,u,D,∑，a,,b. positions.To verify CC2 is a refinement of CC2,we ver- (a,D,D,)=p)A((a,),(a,),b)=) ify the refinement of each thread separately.The rely condition of =3w'.(a',w',D,）卡pA(b=fase→w'=w) each thread captures the interference from both the overall envi- p台0qfp÷9 ronment(R)and its sibling thread (GI or G2).The related steps of p司+ qifa,w,D,,F.(a,w,D,)上p)A(②⊥EF) Cll C2 and Cll C2 should satisfy either thread's guarantee.As 3',C,.(D,wF)-→+(C,'uEF)A(a,u',C,)卡q) in LRG [3].P and P2 specify the private (relational)states of the threads C1/C and C2/C2 respectively.The states P are shared by Figure 8.Semantics of assertions (part II). them.When both threads have terminated,their private states sat- isfy Q1 and Q2,and the shared states satisfy both Qi and 2.We require that the shared states are well-formed(P.Qi and 2 imply verification.In this section,we explain the unary rules for verifying refinement units.All the binary and unary rules constitute our novel /and the overall environment transitions are fenced (ID R). rely-guarantee-style logic for modular verification of termination- The B-WHILE rule requires the boolean conditions of both sides preserving refinement. to be evaluated to the same value.The resources needed to evaluate them should be available in the private part of P.The B-FRAME 5.1 Assertions on Source Code and Number of Tokens rule supports local reasoning.The frame p'may contain shared and private parts,so it should be stable w.r.t.R'+Id and imply We first explain the new assertions p and g used in the unary rules I'+true,where I'is the fence for R'and G'(see Fig.6 for the that can specify the source code and metrics in addition to states definitions of fences and stability).We also require G to be closed We define their syntax in Fig.5,and their semantics in Fig.8.A over transitivity.This rule is almost identical to the one in LRG [3] full state assertion p is interpreted on (a,w,D,)Here besides Details are elided here the states o and at the target and source levels,we introduce We provide a few binary rules to reason about the basic program some auxiliary data w and D.w is the number of tokens needed for units when they are almost identical at both sides.For instance, loops (see Sec.2).D is either some source code C,or a special sign the B-PRT rule relates a target print command to a source one, serving as a unit for defining semantics of p*g below. In Fig.8 we lift the relational assertion P as a full state assertion requiring that they always print out the same value.For more general refinement units,as we explained in Sec.2,we reduce to specify the states.The new assertion arem(C)says that the relational verification to unary reasoning (using the U2B rule in remaining source code is C at the current program point.wf(E) Fig.9,which we will explain in the next section).Our TR [13 states that the number of tokens at the current target code is no less contains more rules and the full soundness proofs.The soundness than E.We can see wf(0)always holds,and for any n,wf(n+1) theorem is shown below implies wf(n).We use [p]a and p]w to ignore the descriptions in p about the source code and the number of tokens respectively.p Theorem 4(Soundness of Binary Rules). lifts p back to a relational state assertion. If R,G,IH{P)C<C(Q),then R,G,I(P)C<CIQ) Separating conjunction p *q has the standard meaning as in separation logic,which says p and g hold over disjoint parts of A Rely-Guarantee-Style Logic for (o,w,D,>)respectively (the formal definition elided here).How- Termination-Preserving Refinement ever,it is worth noting the definition of disjoint union over the quadruple states,which is shown in the middle part of Fig.8.The The binary inference rules in Fig.7 allow us to decompose the disjoint union of the numbers of tokens w and w2 is simply the refinement verification of large programs into the refinement units' sum of them.The disjoint union of Di and D2 is defined only ifR ∨ G2, G1, I ⊢ {P1 ∗ P}C1 C1{Q1 ∗ Q′ 1 } R ∨ G1, G2, I ⊢ {P2 ∗ P}C2 C2{Q2 ∗ Q′ 2 } P ∨Q′ 1∨Q′ 2 ⇒ I I ⊲ R R, G1 ∨ G2, I ⊢ {P1 ∗ P2 ∗ P}C1 kC2 C1 kC2{Q1 ∗ Q2 ∗ (Q′ 1 ∧ Q′ 2 )} (B-PAR) P ⇒ (B ⇔ B) ∗ I R, G, I ⊢ {P ∧ B}C C{P} R, G, I ⊢ {P}while (B) C while (B) C{P ∧ ¬B} (B-WHILE) P ⇒ (E = E) ∗ I Sta(P, R ∗ Id) I ⊲ {R, G} R, G, I ⊢ {P}print(E)print(E){P} (B-PRT) R, G, I ⊢ {P}C C{Q} Sta(P ′ , R′ ∗ Id) I ′ ⊲ {R′ , G′} P ′ ⇒ I ′ ∗ true G+ ⇒ G R ∗ R′ , G ∗ G′ , I ∗ I ′ ⊢ {P ∗ P ′}C C{Q ∗ P ′} (B-FRAME) Figure 7. Selected binary inference rules (compositionality of RGSim-T). Adequacy. RGSim-T ensures the termination-preserving refine￾ment by using the metric with a well-founded order. The proof of the following adequacy theorem is in TR [13]. Theorem 3 (Adequacy of RGSim-T). If there exist R, G, I, Q and a metric M (with a well-founded order <) such that R, G, I |= (C, σ, M)Q (C, Σ), then (C, σ) ⊑ (C, Σ). 4.3 Compositionality Rules RGSim-T is compositional. We show some of the compositionality rules in Fig. 7. Here we use R, G, I ⊢ {P}C  C{Q} for the judgment to emphasize syntactic reasoning, whose semantics is RGSim-T (Def. 2). The rules can be viewed as the binary version of those in a traditional rely-guarantee-style logic (e.g., LRG [3] and RGSep [23]). The B-PAR rule shows the compositionality w.r.t. parallel com￾positions. To verify C1 k C2 is a refinement of C1 k C2, we ver￾ify the refinement of each thread separately. The rely condition of each thread captures the interference from both the overall envi￾ronment (R) and its sibling thread (G1 or G2). The related steps of C1 k C2 and C1 k C2 should satisfy either thread’s guarantee. As in LRG [3], P1 and P2 specify the private (relational) states of the threads C1/C1 and C2/C2 respectively. The states P are shared by them. When both threads have terminated, their private states sat￾isfy Q1 and Q2, and the shared states satisfy both Q ′ 1 and Q ′ 2. We require that the shared states are well-formed (P, Q ′ 1 and Q ′ 2 imply I) and the overall environment transitions are fenced (I ⊲ R). The B-WHILE rule requires the boolean conditions of both sides to be evaluated to the same value. The resources needed to evaluate them should be available in the private part of P. The B-FRAME rule supports local reasoning. The frame P ′ may contain shared and private parts, so it should be stable w.r.t. R ′ ∗ Id and imply I ′ ∗ true, where I ′ is the fence for R ′ and G ′ (see Fig. 6 for the definitions of fences and stability). We also require G to be closed over transitivity. This rule is almost identical to the one in LRG [3]. Details are elided here. We provide a few binary rules to reason about the basic program units when they are almost identical at both sides. For instance, the B-PRT rule relates a target print command to a source one, requiring that they always print out the same value. For more general refinement units, as we explained in Sec. 2, we reduce relational verification to unary reasoning (using the U2B rule in Fig. 9, which we will explain in the next section). Our TR [13] contains more rules and the full soundness proofs. The soundness theorem is shown below. Theorem 4 (Soundness of Binary Rules). If R, G, I ⊢ {P}C C{Q}, then R, G, I |={P}C C{Q}. 5. A Rely-Guarantee-Style Logic for Termination-Preserving Refinement The binary inference rules in Fig. 7 allow us to decompose the refinement verification of large programs into the refinement units’ w ∈ Nat D ::= C | • (σ, w, D, Σ) |= P iff (σ, Σ) |= P (σ, w, D, Σ) |= arem(C ′ ) iff D = C ′ ((s, h), w, D, Σ) |= wf(E) iff ∃n. (JEKs = n) ∧ (n ≤ w) (σ, w, D, Σ) |= ⌊p⌋a iff ∃D ′ . (σ, w, D ′ , Σ) |= p (σ, w, D, Σ) |= ⌊p⌋w iff ∃w′ . (σ, w′ , D, Σ) |= p (σ, Σ) |= TpU iff ∃w, D. (σ, w, D, Σ) |= p D1⊥D2 iff (D1 = •) ∨ (D2 = •) D1 ⊎ D2 def =  D2 if D1 = • D1 if D2 = • (σ1, w1, D1, Σ1) ⊎ (σ2, w2, D2, Σ2) def = (σ1⊎σ2, w1+w2, D1⊎D2, Σ1⊎Σ2) , if σ1⊥σ2, D1⊥D2 and Σ1⊥Σ2 Sta(p, R) iff ∀σ, w, D, Σ, σ′ , Σ′ , b. ((σ, w, D, Σ) |= p) ∧ (((σ, Σ), (σ ′ , Σ′ ), b) |= R) =⇒ ∃w′ . (σ ′ , w′ , D, Σ′ ) |= p ∧ (b = false =⇒ w′ = w) p ⇛0 q iff p ⇒ q p ⇛+ q iff ∀σ, w, D, Σ, ΣF . ((σ, w, D, Σ) |= p) ∧ (Σ⊥ΣF ) =⇒ ∃w′ ,C′ ,Σ′ . (D, Σ⊎ΣF ) −→+ (C′ , Σ′⊎ΣF ) ∧ ((σ, w′ , C′ , Σ′ ) |= q) Figure 8. Semantics of assertions (part II). verification. In this section, we explain the unary rules for verifying refinement units. All the binary and unary rules constitute our novel rely-guarantee-style logic for modular verification of termination￾preserving refinement. 5.1 Assertions on Source Code and Number of Tokens We first explain the new assertions p and q used in the unary rules that can specify the source code and metrics in addition to states. We define their syntax in Fig. 5, and their semantics in Fig. 8. A full state assertion p is interpreted on (σ, w, D, Σ). Here besides the states σ and Σ at the target and source levels, we introduce some auxiliary data w and D. w is the number of tokens needed for loops (see Sec. 2). D is either some source code C, or a special sign • serving as a unit for defining semantics of p ∗ q below. In Fig. 8 we lift the relational assertion P as a full state assertion to specify the states. The new assertion arem(C) says that the remaining source code is C at the current program point. wf(E) states that the number of tokens at the current target code is no less than E. We can see wf(0) always holds, and for any n, wf(n + 1) implies wf(n). We use ⌊p⌋a and ⌊p⌋w to ignore the descriptions in p about the source code and the number of tokens respectively. TpU lifts p back to a relational state assertion. Separating conjunction p ∗ q has the standard meaning as in separation logic, which says p and q hold over disjoint parts of (σ, w, D, Σ) respectively (the formal definition elided here). How￾ever, it is worth noting the definition of disjoint union over the quadruple states, which is shown in the middle part of Fig. 8. The disjoint union of the numbers of tokens w1 and w2 is simply the sum of them. The disjoint union of D1 and D2 is defined only if