(PVarList)O=●|x,O (Assertion)p.q,r,I::=B I empn I emps I Own(x) (s,i,h)卡aB i证[Bl(s)=t IEHE|p*qlp-®gI (s,i,h)=st emps iff s=0 (Action)a,R,G:=p×g|[pla*a|3X.a|a→d (s,i,h)卡emph iff h=0 I aval... (s,i,h)上Own(x) iff dom(s={x对 (s,i,h)FsaE1→Eif Figure 7.The Assertion Language there exist e and n such that [El(s.i)=t.[E2l(s.)=n, dom(h)=t)and h(t)=n 5.The Assertion Language The assertion language is shown in Fig.7.We use the Separation f1g 些dom(f)dom(g)=0 Logic assertions to specify program states.Following Parkinson (s,i,h)(s',i',h') et al.(2006).we treat program variables as resources,but do not (sus',i,huh')if sLs',hlh',i=i' use fractional permissions,which are orthogonal to our technical undefined otherwise development. iff there exist o and or2 such that Semantics of some assertions are shown in Fig.8.The boolean FsL pl*p2 1世o2=T,o1卡sLp1 and o2卡sp2 expression B holds over a state only if it evaluates to true.It is important to note that,with program variables as resources, r卡sp®q iff there exist o'and o"such that the boolean expression E=E does not always hold.It holds if r"=c世cr','Fs p and o"卡q and only if the store contains the variables needed to evaluate E. The assertions empn and emps specify empty heaps and stores x1,...,,p 5 (Own(x1)*Own(n))A p respectively.Own(x)means the ownership of the variable x.E emp emp A emp E2 specifies a singleton heap with E2 stored at the location E1 It also requires that the store contain variables used to evaluate Ei and E2.The separating conjunction p*q means p and g hold Figure 8.Semantics of Selected Separation Logic Assertions over disjoint part of state.Here we use fLg to mean the two finite partial mappings f and g have disjoint domains.The union of two disjoint states o and o2 is defined as oo2.The septraction p-q,introduced by Vafeiadis and Parkinson (2007).means the (c,)Fp×q iff o.i=o'.i,oFst p and o'Fs q state can be extended with a state satisfying p and the extended (c,)=[p] iff o=o'and o Fstp state satisfies g.The assertions Op and emp are syntactic sugars (o,o')=a*a f whose definitions are also shown in Fig.8.O contains a set of program variables,as defined in Fig.7.We omit other assertions there exist 1,2.and o2 such that i=o. here,which are standard separation logic assertions. o102=o.(01.01)F a.and (o2.02)Fa' ((s,i,h),(s',i,h')3X.a iff As in Separation Logic,the precision of assertions is defined there exist n and i'such that i'=in below.Informally,a predicate p is precise if and only if for any and ((s,i',h),(s',i,h'))a state there is at most one sub-state satisfying p. (or,σ)=a→d iff if (o,')F a,then (o,)=a Definition 5.1 (Precise Assertions)An assertion p is precise,i.e., (o,o')=ava' iff (,o')=aor(,')=a precise(p)holds,if and only if for all s,i,h,s1.s2.h.h2.if ss. s2∈s,h1∈h,h2∈h,(s1,i,h1)FsL p and(s2,i,h2)Fsup,then s1=52 and h=h2. Emp些 empemp Trued true xtrue ld [true] al def (()1(')Hal 5.1 Actions We use actions a to specify state transitions.As shown in Fig.7. Figure 9.Semantics of Actions rely/guarantee conditions of threads are actions.Semantics of ac- tions are defined in Fig.9.The action p means the initial state of the transition satisfies p and the resulting state satisfies g.[p] specifies an identity transition with the states satisfying p.a*a' p→pq→4 means the actions a and a'start from disjoint states and the result- (p*p)×(q*q)台(p×q)*(p'<) p×g→p'× ing states are also disjoint.Emp.True and ld are defined using these primitive actions,which represent empty transitions,arbitrary tran- sitions and arbitrary identity transitions respectively.We use Tal to (pVp)×q台(p×qI)V(p'×q) [p→p×p p]→ld represent the set of transitions satisfying a,and use (o,)a and (o.)la]interchangeably in this paper. p(qvq)(pxq)v(pxq) [empl台Emp a→True In Fig.10,we show some selected proof rules for actions,which are sound with respect to the semantics of actions.Many proof a1→4a2→d a*Emp台a a*d台d*d rules for Separation Logic assertions can also be ported for actions a1*2→41*a5 and are omitted here.Examples of actions are shown below.The following lemma shows the monotonicity of the action a*ld: Figure 10.Selected Proof Rules for Actions(PVarList) O ::= • | x,O (Assertion) p,q,r,I ::= B | emph | emps | Own(x) | E → E | p ∗ q | p−q | ... (Action) a,R,G ::= p  q | [p] | a ∗ a | ∃X.a | a ⇒ a | a∨a | ... Figure 7. The Assertion Language 5. The Assertion Language The assertion language is shown in Fig. 7. We use the Separation Logic assertions to specify program states. Following Parkinson et al. (2006), we treat program variables as resources, but do not use fractional permissions, which are orthogonal to our technical development. Semantics of some assertions are shown in Fig. 8. The boolean expression B holds over a state only if it evaluates to true. It is important to note that, with program variables as resources, the boolean expression E = E does not always hold. It holds if and only if the store contains the variables needed to evaluate E. The assertions emph and emps specify empty heaps and stores respectively. Own(x) means the ownership of the variable x. E1 → E2 specifies a singleton heap with E2 stored at the location E1. It also requires that the store contain variables used to evaluate E1 and E2. The separating conjunction p ∗ q means p and q hold over disjoint part of state. Here we use f ⊥g to mean the two finite partial mappings f and g have disjoint domains. The union of two disjoint states σ1 and σ2 is defined as σ1  σ2. The septraction p −q, introduced by Vafeiadis and Parkinson (2007), means the state can be extended with a state satisfying p and the extended state satisfies q. The assertions O p and emp are syntactic sugars, whose definitions are also shown in Fig. 8. O contains a set of program variables, as defined in Fig. 7. We omit other assertions here, which are standard separation logic assertions. As in Separation Logic, the precision of assertions is defined below. Informally, a predicate p is precise if and only if for any state there is at most one sub-state satisfying p. Definition 5.1 (Precise Assertions) An assertion p is precise, i.e., precise(p) holds, if and only if for all s, i, h, s1, s2, h1, h2, if s1 ⊆ s, s2 ⊆ s, h1 ⊆ h, h2 ⊆ h, (s1,i,h1) |=sl p and (s2,i,h2) |=sl p, then s1 = s2 and h1 = h2. 5.1 Actions We use actions a to specify state transitions. As shown in Fig. 7, rely/guarantee conditions of threads are actions. Semantics of ac￾tions are defined in Fig. 9. The action p  q means the initial state of the transition satisfies p and the resulting state satisfies q. [p] specifies an identity transition with the states satisfying p. a ∗ a means the actions a and a start from disjoint states and the result￾ing states are also disjoint. Emp, True and Id are defined using these primitive actions, which represent empty transitions, arbitrary tran￾sitions and arbitrary identity transitions respectively. We use [[a]] to represent the set of transitions satisfying a, and use (σ,σ ) |= a and (σ,σ ) ∈ [[a]] interchangeably in this paper. In Fig. 10, we show some selected proof rules for actions, which are sound with respect to the semantics of actions. Many proof rules for Separation Logic assertions can also be ported for actions and are omitted here. Examples of actions are shown below. The following lemma shows the monotonicity of the action a ∗ Id: (s,i,h) |=sl B iff [[B]](s,i) = tt (s,i,h) |=sl emps iff s = ∅ (s,i,h) |=sl emph iff h = ∅ (s,i,h) |=sl Own(x) iff dom(s) = {x} (s,i,h) |=sl E1 → E2 iff there exist  and n such that [[E1]](s,i) = ,[[E2]](s,i) = n, dom(h) = {} and h() = n f ⊥g def = dom(f)∩dom(g) = ∅ (s,i,h)(s ,i  ,h ) def = (s∪ s ,i,h∪h ) if s⊥s , h⊥h , i = i  undefined otherwise σ |=sl p1 ∗ p2 iff there exist σ1 and σ2 such that σ1 σ2 = σ,σ1 |=sl p1 and σ2 |=sl p2 σ |=sl p−q iff there exist σ and σ such that σ = σσ ,σ |=sl p and σ |=sl q x1,..., xn,• p def = (Own(x1) ∗···∗Own(xn))∧ p emp def = emps ∧emph Figure 8. Semantics of Selected Separation Logic Assertions (σ,σ ) |= p  q iff σ.i = σ .i, σ |=sl p and σ |=sl q (σ,σ ) |= [p] iff σ = σ and σ |=sl p (σ,σ ) |= a ∗ a iff there exist σ1, σ2, σ 1 and σ 2 such that σ1 σ2 = σ, σ 1 σ 2 = σ ,(σ1,σ 1) |= a, and (σ2,σ 2) |= a ((s,i,h),(s ,i,h )) |= ∃X.a iff there exist n and i  such that i  = i{X n}, and ((s,i  ,h),(s ,i  ,h )) |= a (σ,σ ) |= a ⇒ a iff if (σ,σ ) |= a, then (σ,σ ) |= a (σ,σ ) |= a∨a iff (σ,σ ) |= a or (σ,σ ) |= a ... Emp def = emp  emp True def = true  true Id def = [true] [[a]] def = {(σ,σ ) | (σ,σ ) |= a} Figure 9. Semantics of Actions (p ∗ p )  (q ∗ q ) ⇔ (p  q) ∗ (p  q ) p ⇒ p q ⇒ q p  q ⇒ p  q (p∨ p )  q ⇔ (p  q)∨(p  q) [p] ⇒ p  p [p] ⇒ Id p  (q∨q ) ⇔ (p  q)∨(p  q ) [emp] ⇔ Emp a ⇒ True a1 ⇒ a 1 a2 ⇒ a 2 a1 ∗ a2 ⇒ a 1 ∗ a 2 a ∗Emp ⇔ a a ∗ a ⇔ a ∗ a Figure 10. Selected Proof Rules for Actions 6