2.1.THE MEANING OF ASSERTIONS 以 To illustrate the meaning of the separating conjunction,suppose sx and sy are distinct addresses,so that ho=[sx:0] and h=[sy:1] are heaps with disjoint domains.Then If p is: then s,hpif: X→0 h=ho y-1 h=h ×一0*y一1 h=hoh ×一0*一0 false x-0Vy1 h=ho or h=h x-0*(x一0Vy一1) h=hoh (x-0Vy-1)*(x-0Vy-1)h=ho·h1 x0 y1*(0Vy1)false x一0*true ho Ch X→0*一X→0 ho h. Here the behavior of disjunction is slightly surprising. The effect of substitution on the meaning of assertions is similar to that on expressions.We consider only the more general partial case: Proposition 3 (Partial Substitution Law for Assertions)Suppose p is an assertion,and let 6 abbreviate the substitution y一e1,,nen, Then let s be a store such that (FV(p)-{v,...,vn})UFV(e)U...UFV(en) C doms,and let [s I v1:[eileps 1...I Un:[enlems]. Then s,h上(p/)fs,h=p
2.1. THE MEANING OF ASSERTIONS 37 To illustrate the meaning of the separating conjunction, suppose s x and s y are distinct addresses, so that h0 = [ s x: 0 ] and h1 = [ s y: 1 ] are heaps with disjoint domains. Then If p is: then s, h |= p iff: x 7→ 0 h = h0 y 7→ 1 h = h1 x 7→ 0 ∗ y 7→ 1 h = h0 · h1 x 7→ 0 ∗ x 7→ 0 false x 7→ 0 ∨ y 7→ 1 h = h0 or h = h1 x 7→ 0 ∗ (x 7→ 0 ∨ y 7→ 1) h = h0 · h1 (x 7→ 0 ∨ y 7→ 1) ∗ (x 7→ 0 ∨ y 7→ 1) h = h0 · h1 x 7→ 0 ∗ y 7→ 1 ∗ (x 7→ 0 ∨ y 7→ 1) false x 7→ 0 ∗ true h0 ⊆ h x 7→ 0 ∗ ¬ x 7→ 0 h0 ⊆ h. Here the behavior of disjunction is slightly surprising. The effect of substitution on the meaning of assertions is similar to that on expressions. We consider only the more general partial case: Proposition 3 (Partial Substitution Law for Assertions) Suppose p is an assertion, and let δ abbreviate the substitution v1 → e1, . . . , vn → en, Then let s be a store such that (FV(p)− {v1, . . . , vn})∪FV(e1)∪· · ·∪FV(en) ⊆ dom s, and let sb = [ s | v1: [[e1]]exps | . . . | vn: [[en]]exps ]. Then s, h |= (p/δ) iff s, h b |= p
38 CHAPTER 2.ASSERTIONS 2.2 Inference We will reason about assertions using inference rules of the form P …P C. where the zero or more P are called the premisses and the C is called the The premisses and conclusion are schemata,i.e.,they may contain meta- variables,each of which ranges over some set of phrases,such as expressions, variables,or assertions.To avoid confusion,we will use italic (or occasionally Greek)characters for metavariables,but sans serif characters for the object variables of the logic and programming lanugage. An insta each metavariable by a phras in its range.These replacements must satisfy the side conditions (if any)of the rule.(Since this is replacement of metavariables rather than substitution for variables,there is never any renaming.)For instance, Inference Rules Instances P0P0→P1 ×+0=××+0=×→×=×+0 p四 ×=×+0 1=e0→o=e ×+0=×→×=×+0 ×+0=× x+0=× An inference rule is sound iff,for all instances,if the premisses of the instance are all valid.then the conclusion is valid. of assertions,each of whicl occur earlier in the sequence.For example, X+0=X x+0=×→=×+0 ×=×+0
38 CHAPTER 2. ASSERTIONS 2.2 Inference We will reason about assertions using inference rules of the form P1 · · · Pn C, where the zero or more Pi are called the premisses and the C is called the conclusion. The premisses and conclusion are schemata, i.e., they may contain metavariables, each of which ranges over some set of phrases, such as expressions, variables, or assertions. To avoid confusion, we will use italic (or occasionally Greek) characters for metavariables, but sans serif characters for the object variables of the logic and programming lanugage. An instance of an inference rule is obtained by replacing each metavariable by a phrase in its range. These replacements must satisfy the side conditions (if any) of the rule. (Since this is replacement of metavariables rather than substitution for variables, there is never any renaming.) For instance, Inference Rules Instances p0 p0 ⇒ p1 p1 x + 0 = x x + 0 = x ⇒ x = x + 0 x = x + 0 e1 = e0 ⇒ e0 = e1 x + 0 = x ⇒ x = x + 0 x + 0 = x x + 0 = x An inference rule is sound iff, for all instances, if the premisses of the instance are all valid, then the conclusion is valid. A formal proof (for assertions) is a sequence of assertions, each of which is the conclusion of some instance of a sound inference rule whose premisses occur earlier in the sequence. For example, x + 0 = x x + 0 = x ⇒ x = x + 0 x = x + 0
2.2.INFERENCE 场 Since we require the inference rules used in the proof to be sound,it follows that the assertions in a formal proof must all be valid. Notice the distinction between formal proofs,whose constituents are as containing assertio mmands】 and meta-proofs, are ordinary mathematical proofs using the semantics of assertions(and,in the next chap- ter,of commands). An inference rule with zero premisses is called an ariom schema.The overbar is often omitted.(Notice that the first assertion in a proof must be an axiom sche na.)An axiom sche etavariables s own unique instance)is called an ariom.The overbar is usually omitted. The following are inference rules that are sound for predicate calculus, and remain sound for the extension to assertions in separation logic: pp今9(modus ponens） p÷g when v￥FV(p) (2.1) p÷(u.q) p→9 when v￥FV(g). (日u.p)→q In addition,the following axiom schemas are sound for predicate calculus
2.2. INFERENCE 39 Since we require the inference rules used in the proof to be sound, it follows that the assertions in a formal proof must all be valid. Notice the distinction between formal proofs, whose constituents are assertions written in separation logic (or, in the next chapter, specifications containing assertions and commands), and meta-proofs, which are ordinary mathematical proofs using the semantics of assertions (and, in the next chapter, of commands). An inference rule with zero premisses is called an axiom schema. The overbar is often omitted. (Notice that the first assertion in a proof must be an instance of an axiom schema.) An axiom schema containing no metavariables (so that it is its own unique instance) is called an axiom. The overbar is usually omitted. The following are inference rules that are sound for predicate calculus, and remain sound for the extension to assertions in separation logic: p p ⇒ q q (modus ponens) p ⇒ q p ⇒ (∀v. q) when v ∈/ FV(p) p ⇒ q (∃v. p) ⇒ q when v ∈/ FV(q). (2.1) In addition, the following axiom schemas are sound for predicate calculus
CHAPTER 2.ASSERTIONS and assertions in separation logic: p→(g→p) (p→(g→r)→(p→q)→(p→r) (pAq)→p (pΛg→q p→(q→(pAg) p→(pVq) q→(pVq (2.2) p÷r)→(g→r)→(pVq→r) p→q)→(p→q)→p) (p)→p (p台q→(p→q)A(q→p) (P→q)A(g→p)→(p÷q) （u.p)→(p/u一e) (p/u→e)→（目u.p). The rules in (2.1)and(2.2)(with the exception of the rules involving)are e 82].Th (one of m plete rence rules (i. e.rule that are sound for any int rpretation of the domain of discourse or the function and predicate symbols) It is important to notice the difference between andp→g 0 A rule of the first form will be sound providing,for all instances,the validity of p implies the validity of g,i.e.,whenever p holds for all states,g holds for all states.But a rule of the second form will be sound providing,for all instances,pg is valid,i.e.,for every state,if p holds in that state then g holds in the same state.Consider the rule of generalization (which can be derived from the rules above), Yv.p
40 CHAPTER 2. ASSERTIONS and assertions in separation logic: p ⇒ (q ⇒ p) (p ⇒ (q ⇒ r)) ⇒ ((p ⇒ q) ⇒ (p ⇒ r)) (p ∧ q) ⇒ p (p ∧ q) ⇒ q p ⇒ (q ⇒ (p ∧ q)) p ⇒ (p ∨ q) q ⇒ (p ∨ q) (p ⇒ r) ⇒ ((q ⇒ r) ⇒ ((p ∨ q) ⇒ r)) (p ⇒ q) ⇒ ((p ⇒ ¬q) ⇒ ¬p) ¬(¬p) ⇒ p (p ⇔ q) ⇒ ((p ⇒ q) ∧ (q ⇒ p)) ((p ⇒ q) ∧ (q ⇒ p)) ⇒ (p ⇔ q) (∀v. p) ⇒ (p/v → e) (p/v → e) ⇒ (∃v. p). (2.2) The rules in (2.1) and (2.2) (with the exception of the rules involving ⇔) are taken from Kleene [44, page 82]. They are (one of many possible) complete sets of logical inference rules (i.e., rules that are sound for any interpretation of the domain of discourse or the function and predicate symbols). It is important to notice the difference between p q and p ⇒ q. A rule of the first form will be sound providing, for all instances, the validity of p implies the validity of q, i.e., whenever p holds for all states, q holds for all states. But a rule of the second form will be sound providing, for all instances, p ⇒ q is valid, i.e., for every state, if p holds in that state then q holds in the same state. Consider the rule of generalization (which can be derived from the rules above), p ∀v. p
2.2.INFERENCE This rule is sound;for example,the instance x+y=y+x Vx.x+y=y+x is sound because its conclusion is valid,while the instance ×=0 x.x=0 is sound because its premiss is not valid. On the eother hand,the corresponding implication p→u.p(unsound) is not sound,since,for instance,there is a state in which x =0 holds but Vx.x =0 does not. We have already seen the following general inference rules for assertions: P*P1台pP1*P (P*P)*P2台*(p1*P2) p*emp台p (Po Vp)*(po q)v(p q) (2.3) (PoApi)(po q)A(p q) (们r.po)*h÷3r.(po*ph)when x not free in p (Vr.po)*pVr.(po p1)when x not free in p P0*90→P1*91 p0*p1→p2 p÷(p*p2) (currying） (decurrying) P0÷(p1*P2) P0*p1→p2. as well as specific rules forand eo6Ae1一台eo6Aeo=e1A6= o一%*1一→e0≠e1 (2.4) emp÷a.(x-）) (e一e)Ap→(e-e)*(e一e)*p)
2.2. INFERENCE 41 This rule is sound; for example, the instance x + y = y + x ∀x. x + y = y + x is sound because its conclusion is valid, while the instance x = 0 ∀x. x = 0 is sound because its premiss is not valid. On the other hand, the corresponding implication p ⇒ ∀v. p (unsound) is not sound, since, for instance, there is a state in which x = 0 holds but ∀x. x = 0 does not. We have already seen the following general inference rules for assertions: p0 ∗ p1 ⇔ p1 ∗ p0 (p0 ∗ p1) ∗ p2 ⇔ p0 ∗ (p1 ∗ p2) p ∗ emp ⇔ p (p0 ∨ p1) ∗ q ⇔ (p0 ∗ q) ∨ (p1 ∗ q) (p0 ∧ p1) ∗ q ⇒ (p0 ∗ q) ∧ (p1 ∗ q) (∃x. p0) ∗ p1 ⇔ ∃x. (p0 ∗ p1) when x not free in p1 (∀x. p0) ∗ p1 ⇒ ∀x. (p0 ∗ p1) when x not free in p1 (2.3) p0 ⇒ p1 q0 ⇒ q1 p0 ∗ q0 ⇒ p1 ∗ q1 (monotonicity) p0 ∗ p1 ⇒ p2 p0 ⇒ (p1 −∗ p2) (currying) p0 ⇒ (p1 −∗ p2) p0 ∗ p1 ⇒ p2. (decurrying) as well as specific rules for 7→ and ,→: e0 7→ e 0 0 ∧ e1 7→ e 0 1 ⇔ e0 7→ e 0 0 ∧ e0 = e1 ∧ e 0 0 = e 0 1 e0 ,→ e 0 0 ∗ e1 ,→ e 0 1 ⇒ e0 6= e1 emp ⇔ ∀x. ¬(x ,→ −) (e ,→ e 0 ) ∧ p ⇒ (e 7→ e 0 ) ∗ ((e 7→ e 0 ) −∗ p). (2.4)