32 CHAPTER 1.AN OVERVIEW with appropriate restrictions on variable occurrences
32 CHAPTER 1. AN OVERVIEW with appropriate restrictions on variable occurrences
An Introduction to Separation Logic 2008 John C.Reynolds October 23.2008 Chapter 2 Assertions In this chapter,we give a more detailed exposition of the assertions of First,we discuss some general properties that are shared among assertions and other phrases occurring in both our programming language and its logic. In all cases,variable binding behaves in the standard manner.In expres- sions there are no binding constructions,in assertions quantifiers are binding constructions,and in commands declarations are bindi ing constructions.In ach case the e of the variable bei bo und is the ediately follov wing subphrase,except that in declaratio 60 f the form newvar v=e in c,or iterated separating conjunctions of the form p(to be introduced in Section 6.1),the initialization e and the bounds co and el are not in the scope of the binder v. We write FV(p)for the set of variables occurring free in p,which is defined way The meaning of any ph ras is independent of the value s that do not occur free in the phrase Substitution is also defined in the standard way.We begin by considering total substitutions that act upon all the free variables of a phrase:For any phrase p such that FV(p),...,n,we write p/1+e1,...,Un→en to denote the phrase obtained from p by simultaneously substituting each expression e;for the variable v,(When there are bound variables in p,they will be renamed to avoid capture.) 33
Chapter 2 Assertions An Introduction to Separation Logic c 2008 John C. Reynolds October 23, 2008 In this chapter, we give a more detailed exposition of the assertions of separation logic: their meaning, illustrations of their usage, inference rules, and several classes of assertions with special properties. First, we discuss some general properties that are shared among assertions and other phrases occurring in both our programming language and its logic. In all cases, variable binding behaves in the standard manner. In expressions there are no binding constructions, in assertions quantifiers are binding constructions, and in commands declarations are binding constructions. In each case, the scope of the variable being bound is the immediately following subphrase, except that in declarations of the form newvar v = e in c, or iterated separating conjunctions of the form Je1 v=e0 p (to be introduced in Section 6.1), the initialization e and the bounds e0 and e1 are not in the scope of the binder v. We write FV(p) for the set of variables occurring free in p, which is defined in the standard way. The meaning of any phrase is independent of the value of those variables that do not occur free in the phrase. Substitution is also defined in the standard way. We begin by considering total substitutions that act upon all the free variables of a phrase: For any phrase p such that FV(p) ⊆ {v1, . . . , vn}, we write p/v1 → e1, . . . , vn → en to denote the phrase obtained from p by simultaneously substituting each expression ei for the variable vi , (When there are bound variables in p, they will be renamed to avoid capture.) 33
CHAPTER 2.ASSERTIONS When expressionsare substituted for variables in an tion p,the effect mimics a change of the store.In the specific case where p is an expression: Proposition 1 (Total Substitution Law for Erpressions)Let 6 abbreviate the substitution h一e1,,n一e let s be a store such that FV(e)U...UFV(en)C doms,and let s=[v1:leiloxps 1...I vn:[enlexps]. If e is an erpression (or boolean expression)such that FV(e)Cv,...,vn, then [e/6loxps [elexps. Here we have introduced a notation for describing stores (and more generally eration: maps each ci into yi. Next,we generalize this result to partial substitutions that need not act upon all the free variables of a phrase:When FV(p)is not a subset of {,, p/→e1,,n一en abbreviates p/u1→e1,,n→e,→，，g→以， where {v,...,}=FV(p)-{v,...,n).Then the above proposition can be generalized to Proposition 2 (Partial Substitution Law for Erpressions)Suppose e is an erpression (or boolean erpression),and let 6 abbreviate the substitution h→e1,,vn一e, Then let s be astore such that (FV(e)-)UFV(eUFV(e) doms,and let =[s I v1:[eilexps 1...I Un:[enlexps ] Then [e/leps [elexps
34 CHAPTER 2. ASSERTIONS When expressions are substituted for variables in an expression or assertion p, the effect mimics a change of the store. In the specific case where p is an expression: Proposition 1 (Total Substitution Law for Expressions) Let δ abbreviate the substitution v1 → e1, . . . , vn → en, let s be a store such that FV(e1) ∪ · · · ∪ FV(en) ⊆ dom s, and let sb = [ v1: [[e1]]exps | . . . | vn: [[en]]exps ]. If e is an expression (or boolean expression) such that FV(e) ⊆ {v1, . . . , vn}, then [[e/δ]]exps = [[e]]exps. b Here we have introduced a notation for describing stores (and more generally, functions with finite domains) by enumeration: We write [ x1: y1 | . . . | xn: yn ] (where x1,. . . , xn are distinct) for the function with domain {x1, . . . , xn} that maps each xi into yi . Next, we generalize this result to partial substitutions that need not act upon all the free variables of a phrase: When FV(p) is not a subset of {v1, . . . , vn}, p/v1 → e1, . . . , vn → en abbreviates p/v1 → e1, . . . , vn → en, v0 1 → v 0 1 , . . . , v0 k → v 0 k , where {v 0 1 , . . . , v0 k} = FV(p) − {v1, . . . , vn}. Then the above proposition can be generalized to Proposition 2 (Partial Substitution Law for Expressions) Suppose e is an expression (or boolean expression), and let δ abbreviate the substitution v1 → e1, . . . , vn → en, Then let s be a store such that (FV(e)− {v1, . . . , vn})∪FV(e1)∪· · ·∪FV(en) ⊆ dom s, and let sb = [ s | v1: [[e1]]exps | . . . | vn: [[en]]exps ]. Then [[e/δ]]exps = [[e]]exps. b
2.1.THE MEANING OF ASSERTIONS 35 Here we have introduced a notation for describing the extension or variation of a function.We write [f r1:y...rn:yn (where r1....,n are distinct)for the function whose domain is the union of the domain of f with 1,....,that maps each into y and all other members r of the domain of f into fr. A si milar result for assertions will be given in the next section.As we will see in the next chapter,however,the situation for commands is more subtle 2.1 The Meaning of Assertions When s is a store,h is a heap,and p is an assertion whose free variables all belong to the domain of s,we write s,hFp to indicate that the state s,h satisfies p,or p is true in s,h,or p holds in s,h. Then the following formulas define this relation by induction on the structure of p.(Here we write ho Lh when ho and h are heaps with disjoint domains andtodenote the uion of heaps with disjoint domains.) s,hb iff [olbexps true s,h上一pifs,h上p is false. s,h=poApiff s,hpo and s,h=p (and similarly for V,→，÷)， s,h上.p iff Vx eZ.[s|:x]，小hFp, s,h3.p iff 3eZ.[s v:],hp, s,h上emp iff domh={, s,hFee iff dom h ={[eleps}and h(leleps)=le'lops, s,hFpo*P iff Tho,h1.ho⊥h1 and ho·h1=hand s,ho上po and s,hFp1, s,hFpo*phi证h.(W'⊥h and s,NFpo)implies s,h.hp
2.1. THE MEANING OF ASSERTIONS 35 Here we have introduced a notation for describing the extension or variation of a function. We write [ f | x1: y1 | . . . | xn: yn ] (where x1,. . . , xn are distinct) for the function whose domain is the union of the domain of f with {x1, . . . , xn}, that maps each xi into yi and all other members x of the domain of f into f x. A similar result for assertions will be given in the next section. As we will see in the next chapter, however, the situation for commands is more subtle. 2.1 The Meaning of Assertions When s is a store, h is a heap, and p is an assertion whose free variables all belong to the domain of s, we write s, h |= p to indicate that the state s, h satisfies p, or p is true in s, h, or p holds in s, h. Then the following formulas define this relation by induction on the structure of p. (Here we write h0 ⊥ h1 when h0 and h1 are heaps with disjoint domains, and h0 · h1 to denote the union of heaps with disjoint domains.) s, h |= b iff [[b]]bexps = true, s, h |= ¬p iff s, h |= p is false, s, h |= p0 ∧ p1 iff s, h |= p0 and s, h |= p1 (and similarly for ∨, ⇒, ⇔), s, h |= ∀v. p iff ∀x ∈ Z. [ s | v: x ], h |= p, s, h |= ∃v. p iff ∃x ∈ Z. [ s | v: x ], h |= p, s, h |= emp iff dom h = {}, s, h |= e 7→ e 0 iff dom h = {[[e]]exps} and h([[e]]exps) = [[e 0 ]]exps, s, h |= p0 ∗ p1 iff ∃h0, h1. h0 ⊥ h1 and h0 · h1 = h and s, h0 |= p0 and s, h1 |= p1, s, h |= p0 −∗ p1 iff ∀h 0 . (h 0 ⊥ h and s, h0 |= p0) implies s, h · h 0 |= p1
6 CHAPTER 2.ASSERTIONS All but the last four formulas coincide with the standard interpretation of predicate logic,with the heap h being carried along without change. When s,h =p holds for all states s,h (such that the domain of s contains the free variables of p),we say that p is valid.When s,h=p holds for some state s.h,we say that p is satisfiable. The following illustrates the use of these formulas to determine the mean- ing of an assertion: s,h上x-0*y1if3ho,h1.ho⊥h1 and ho·h1=h and s,hox0 and s,h Fy1 ifho,h.ho⊥hand hoh=h and dom ho {sx}and ho(sx)=0 and domh={sy}and h(sy)=1 fs×≠sy and domh={sx,sy} and h(sx)=0 and h(sy)=1 iff sx#sy and h=[sx:0 sy:1]. The following illustrate the meaning of and(including the abbre- viations defined in Section 1.4): s,hxy iff domh={sx}and h(sx)=sy s,hx-iff domh ={sx} s,hFx y iff sxe∈dom h and h(sx)=sy s,hxiff sx e dom h s,hxy,z iff h=[sx:sy sx+1:sz] s,hx--,-i证domh={sx,sx+1} s,hF×一y,zi证h2[sxsy|s×+1:sz] s,h上x-,-ff domh2{sx,s×+1}
36 CHAPTER 2. ASSERTIONS All but the last four formulas coincide with the standard interpretation of predicate logic, with the heap h being carried along without change. When s, h |= p holds for all states s, h (such that the domain of s contains the free variables of p), we say that p is valid. When s, h |= p holds for some state s, h, we say that p is satisfiable. The following illustrates the use of these formulas to determine the meaning of an assertion: s, h |= x 7→ 0 ∗ y 7→ 1 iff ∃h0, h1. h0 ⊥ h1 and h0 · h1 = h and s, h0 |= x 7→ 0 and s, h1 |= y 7→ 1 iff ∃h0, h1. h0 ⊥ h1 and h0 · h1 = h and dom h0 = {s x} and h0(s x) = 0 and dom h1 = {s y} and h1(s y) = 1 iff s x 6= s y and dom h = {s x, s y} and h(s x) = 0 and h(s y) = 1 iff s x 6= s y and h = [ s x: 0 | s y: 1 ]. The following illustrate the meaning of 7→ and ,→ (including the abbreviations defined in Section 1.4): s, h |= x 7→ y iff dom h = {s x} and h(s x) = s y s, h |= x 7→ − iff dom h = {s x} s, h |= x ,→ y iff s x ∈ dom h and h(s x) = s y s, h |= x ,→ − iff s x ∈ dom h s, h |= x 7→ y, z iff h = [ s x: s y | s x + 1: s z ] s, h |= x 7→ −, − iff dom h = {s x, s x + 1} s, h |= x ,→ y, z iff h ⊇ [ s x: s y | s x + 1: s z ] s, h |= x ,→ −, − iff dom h ⊇ {s x, s x + 1}