CHAPTER 1.AN OVERVIEW that e points to e'somewhere in the heap: eege一e*true and that e points to a record with several fields: ee,,enge一e1*…*e+n-1en ee1,,enge一e1*…*e+n-le 证e一e1,,en*true Notice that assertions of the form ee',e-,and ee1. determine the extent (i.e..domain)of the heap they describe.while those of the form eand do no (Technic ally,the f forme said to be precis given in Section 2.3.3.) By using→，→，and both separating and ordinary conjunction,it is eas to describe simple sharing patterns concisely.For instance: 1.x3,y asserts that x points to an adjacent pair of cells containing 3 and y(i the store maps× x-3 and y into some values a and B,a is an address y and the heap maps a into 3 and a+1 into B). 2.y3.x asserts that y points to an adjacent pair of cells containing 3 and x. 圆 3.￥ →3y y一3，asserts that situations() and(2)hold for separate parts of the heap. ® 4.×-3,yAy一3，×asserts that situations(1)and (2)hold for the same heap,which can only happen if the values of x and y are the same 5.x -3,yy 3,x asserts that either (3)or (4) may hold,and that the heap may contain additional cells
12 CHAPTER 1. AN OVERVIEW that e points to e 0 somewhere in the heap: e ,→ e 0 def = e 7→ e 0 ∗ true, and that e points to a record with several fields: e 7→ e1, . . . , en def = e 7→ e1 ∗ · · · ∗ e + n − 1 7→ en e ,→ e1, . . . , en def = e ,→ e1 ∗ · · · ∗ e + n − 1 ,→ en iff e 7→ e1, . . . , en ∗ true. Notice that assertions of the form e 7→ e 0 , e 7→ −, and e 7→ e1, . . . , en determine the extent (i.e., domain) of the heap they describe, while those of the form e ,→ e 0 and e ,→ e1, . . . , en do not. (Technically, the former are said to be precise assertions. A precise definition of precise assertions will be given in Section 2.3.3.) By using 7→, ,→, and both separating and ordinary conjunction, it is easy to describe simple sharing patterns concisely. For instance: 1. x 7→ 3, y asserts that x points to an adjacent pair of cells containing 3 and y (i.e., the store maps x and y into some values α and β, α is an address, and the heap maps α into 3 and α + 1 into β). y x ✲ 3 2. y 7→ 3, x asserts that y points to an adjacent pair of cells containing 3 and x. x y ✲ 3 3. x 7→ 3, y ∗ y 7→ 3, x asserts that situations (1) and (2) hold for separate parts of the heap. ◦ x ✲ 3 ◦ ❨✯ 3 ✛ y 4. x 7→ 3, y∧y 7→ 3, x asserts that situations (1) and (2) hold for the same heap, which can only happen if the values of x and y are the same. ◦ 3 ❍❥ ✟✯ x y ② 5. x ,→ 3, y ∧ y ,→ 3, x asserts that either (3) or (4) may hold, and that the heap may contain additional cells
1.4.ASSERTIONS 妇 Separating implication is somewhat more subtle,but is illustrated by the following example(due to O'Hearn):Suppose the assertion p asserts various conditions about the store and heap,including that the store maps x into the address of a record containing 3 and 4: Store:x:a,… Heap:a:3,a+1:4,Rest of Heap Then (x3,4)-*p asserts that,if one were to add to the current heap a disjoint heap consisting of a record at address x containing 3 and 4,then the resulting heap would satisfy p.In other words,the current heap is like that described by p,except that the record is missing: Store x:o... Heap:Rest of Heap,as above Moreover,x1,2 ((x3,4)-+p)asserts that the heap consists of a record at x containing I and 2.plus a separate part as above: Store:x:a,... Heap:a:1,a+1:2. x-1 Rest of Heap,as above This example suggests that x1,2 ((3,4)-+p)describes a state that would be d by the mutation c rations：=3and+1:=4 into a state satisfying.n fact,we will find that {x一1,2*(x一3,4)*p)}=3；+1=4{p} is a valid specification (i.e.,Hoare triple)in separation logic-as is the more general specification {x一-，-*(x一3,4)*p)}冈=3；x+1]:=4{p} The inference rules for predicate calculus(not involving the new operators we have introduced)remain sound in this enriched setting.Additional axiom schemata for separating conjunction include commutative and associative
1.4. ASSERTIONS 13 Separating implication is somewhat more subtle, but is illustrated by the following example (due to O’Hearn): Suppose the assertion p asserts various conditions about the store and heap, including that the store maps x into the address of a record containing 3 and 4: Store : x: α, . . . Heap : α: 3, α + 1: 4, Rest of Heap 4 x ✲ 3 ✛ ◦ ✛ ◦ ✎ ✍ ☞ ✌ Rest of Heap Then (x 7→ 3, 4) −∗ p asserts that, if one were to add to the current heap a disjoint heap consisting of a record at address x containing 3 and 4, then the resulting heap would satisfy p. In other words, the current heap is like that described by p, except that the record is missing: Store : x: α, . . . Heap : Rest of Heap, as above x ✲ ✛ ◦ ✛ ◦ ✎ ✍ ☞ ✌ Rest of Heap Moreover, x 7→ 1, 2 ∗ ((x 7→ 3, 4) −∗ p) asserts that the heap consists of a record at x containing 1 and 2, plus a separate part as above: Store : x: α, . . . Heap : α: 1, α + 1: 2, Rest of Heap, as above 2 x ✲ 1 ✛ ◦ ✛ ◦ ✎ ✍ ☞ ✌ Rest of Heap This example suggests that x 7→ 1, 2 ∗ ((x 7→ 3, 4) −∗ p) describes a state that would be changed by the mutation operations [x] := 3 and [x + 1] := 4 into a state satisfying p. In fact, we will find that {x 7→ 1, 2 ∗ ((x 7→ 3, 4) −∗ p)} [x] := 3 ; [x + 1] := 4 {p} is a valid specification (i.e., Hoare triple) in separation logic — as is the more general specification {x 7→ −, − ∗ ((x 7→ 3, 4) −∗ p)} [x] := 3 ; [x + 1] := 4 {p}. The inference rules for predicate calculus (not involving the new operators we have introduced) remain sound in this enriched setting. Additional axiom schemata for separating conjunction include commutative and associative
4 CHAPTER 1.AN OVERVIEW laws,the fact that emp is a neutral element,and various distributive and semidistributive laws: p1*P2台P2*P (P1*p2)*内台P1*(P2*P3) p*emp台p (P1 V p2)*(p q)v (p2 q) (p1Ap2）*9÷(P1*q)A(P2*q (目z.p)*P2÷3r.(p1*p2)when x not free in p2 (.ph)*p2→z.(p1*h)when x not free in p2 There is also an inference rule showing that separating conjunction is mono- tone with respect to implication: pm→24→2 (monotonicity） P1*91→P2*92 and two further rules capturing the adjunctive relationship between separat- ing conjunction and separating implication: P1*P2→P内 p1→(p2*) (currying) (decurrying) p1→(P2*p) D1*2→p3· On the other hand,there are two rules that one might expect to hold for an operation called "conjunction"that in fact fail: (Contraction-unsound) p*q→p (Weakening-unsound) A counterexample to both of thes to be x1 and g to be y→2；then p holds for a certain single-field heap while p *p holds for no heap,and p *q holds for a certain two-field heap while p holds for no two-field heap.(Thus separation logic is a substructural logic.)
14 CHAPTER 1. AN OVERVIEW laws, the fact that emp is a neutral element, and various distributive and semidistributive laws: p1 ∗ p2 ⇔ p2 ∗ p1 (p1 ∗ p2) ∗ p3 ⇔ p1 ∗ (p2 ∗ p3) p ∗ emp ⇔ p (p1 ∨ p2) ∗ q ⇔ (p1 ∗ q) ∨ (p2 ∗ q) (p1 ∧ p2) ∗ q ⇒ (p1 ∗ q) ∧ (p2 ∗ q) (∃x. p1) ∗ p2 ⇔ ∃x. (p1 ∗ p2) when x not free in p2 (∀x. p1) ∗ p2 ⇒ ∀x. (p1 ∗ p2) when x not free in p2 There is also an inference rule showing that separating conjunction is monotone with respect to implication: p1 ⇒ p2 q1 ⇒ q2 p1 ∗ q1 ⇒ p2 ∗ q2 (monotonicity) and two further rules capturing the adjunctive relationship between separating conjunction and separating implication: p1 ∗ p2 ⇒ p3 p1 ⇒ (p2 −∗ p3) (currying) p1 ⇒ (p2 −∗ p3) p1 ∗ p2 ⇒ p3. (decurrying) On the other hand, there are two rules that one might expect to hold for an operation called “conjunction” that in fact fail: p ⇒ p ∗ p (Contraction — unsound) p ∗ q ⇒ p (Weakening — unsound) A counterexample to both of these axiom schemata is provided by taking p to be x 7→ 1 and q to be y 7→ 2; then p holds for a certain single-field heap while p ∗ p holds for no heap, and p ∗ q holds for a certain two-field heap while p holds for no two-field heap. (Thus separation logic is a substructural logic.)
1.5.SPECIFICATIONS AND THEIR INFERENCE RULES 6 Finally,we give axiom schemata for the predicate.(Regrettably,these are far from complete.) e1一eAe2-÷e1-eAe1=e2Ae=e4 e1一e*e2一→e1卡e2 emp÷红.(x-) (ee)np→(ee)*(ee)*p) 1.5 Specifications and their Inference Rules While assertions describe states,specifications describe commands.In spec- ification logic,specifications are Hoare triples,which come in two flavors: (specification)::= {(assertion)}(command){(assertion)} (partial correctness) I[(assertion)](command)[(assertion)] (total correctness) In both flavors,the initial assertion is called the precondition (or sometimes the precedent),and the final assertion is called the postcondition (or some- times the consequent). The partial correctness specification (p)cq}is true iff,starting in any state in which p holds No execution of c aborts,and When some execution of c terminates in a final state,then q holds in the final state. The total correctness specification [p]c[](which we will use much less often)is true iff,starting in any state in which p holds, No execution of c aborts,and Every execution of c terminates,and When some execution of c terminates in a final state,then g holds in the final state
1.5. SPECIFICATIONS AND THEIR INFERENCE RULES 15 Finally, we give axiom schemata for the predicate 7→. (Regrettably, these are far from complete.) e1 7→ e 0 1 ∧ e2 7→ e 0 2 ⇔ e1 7→ e 0 1 ∧ e1 = e2 ∧ e 0 1 = e 0 2 e1 ,→ e 0 1 ∗ e2 ,→ e 0 2 ⇒ e1 6= e2 emp ⇔ ∀x. ¬(x ,→ −) (e ,→ e 0 ) ∧ p ⇒ (e 7→ e 0 ) ∗ ((e 7→ e 0 ) −∗ p). 1.5 Specifications and their Inference Rules While assertions describe states, specifications describe commands. In specification logic, specifications are Hoare triples, which come in two flavors: hspecificationi ::= {hassertioni} hcommandi {hassertioni} (partial correctness) | [ hassertioni ] hcommandi [ hassertioni ] (total correctness) In both flavors, the initial assertion is called the precondition (or sometimes the precedent), and the final assertion is called the postcondition (or sometimes the consequent). The partial correctness specification {p} c {q} is true iff, starting in any state in which p holds, • No execution of c aborts, and • When some execution of c terminates in a final state, then q holds in the final state. The total correctness specification [ p ] c [ q ] (which we will use much less often) is true iff, starting in any state in which p holds, • No execution of c aborts, and • Every execution of c terminates, and • When some execution of c terminates in a final state, then q holds in the final state
CHAPTER 1.AN OVERVIEW These forms of specification are so similar to those of Hoare logic that it is important to note the differences.Our specifications are implicitly quantified over both stores and heaps,and also(since allocation is indeterminate)over all possible executions.Moreover,any execution(starting in a state satisfying p)that gives a memory fault falsifies both partial and total specifications. The last point goes to the heart of separation logic.As O'Hearn [5] paraphrased Miln "Well-specified program don 0 wrong..”As a cor sequence,during the execution of a program that has been proved to mee some specification (assuming that the program is only executed in initial states satisfying the precondition of the specification),it is unnecessary to check for memory faults,or even to equip heap cells with activity bits. In fact,it is not the implementor's responsibility to detect memory faults. It is the programmer's responsibility to avoid them-and separation logic is a tool this purpose Indeed ccord to the logi the is free to implement memory faults however he wishes,since nothing can be proved that might gainsay him. Roughly speaking,the fact that specifications preclude memory faults acts in concert with the indeterminacy of allocation to prohibit violations of record boundaries.For example.during an execution of co;×:=cons(1,2);q;x+2:=7, no allocation performed by the subcommand co or c can be guaranteed to allocate the location nodify ther OS: ty tha the hat there is no postcondition that makes the specification {true}co:x:=cons(1,2);c1;x+2=7{?} valid Sometimes,however,the notion of record boundaries dissolves,as in the following valid(and provable)specification of a program that tries to form a two-field record by gluing together two one-field records: {x一-*y一-} if y=x+1 then skip else if x=y+1 then x:=y else (1.5) (dispose x;dispose y:x:=cons(1,2)) {x一-，-
16 CHAPTER 1. AN OVERVIEW These forms of specification are so similar to those of Hoare logic that it is important to note the differences. Our specifications are implicitly quantified over both stores and heaps, and also (since allocation is indeterminate) over all possible executions. Moreover, any execution (starting in a state satisfying p) that gives a memory fault falsifies both partial and total specifications. The last point goes to the heart of separation logic. As O’Hearn [5] paraphrased Milner, “Well-specified programs don’t go wrong.” As a consequence, during the execution of a program that has been proved to meet some specification (assuming that the program is only executed in initial states satisfying the precondition of the specification), it is unnecessary to check for memory faults, or even to equip heap cells with activity bits. In fact, it is not the implementor’s responsibility to detect memory faults. It is the programmer’s responsibility to avoid them — and separation logic is a tool for this purpose. Indeed, according to the logic, the implementor is free to implement memory faults however he wishes, since nothing can be proved that might gainsay him. Roughly speaking, the fact that specifications preclude memory faults acts in concert with the indeterminacy of allocation to prohibit violations of record boundaries. For example, during an execution of c0 ; x := cons(1, 2) ; c1 ; [x + 2] := 7, no allocation performed by the subcommand c0 or c1 can be guaranteed to allocate the location x + 2; thus as long as c0 and c1 terminate and c1 does not modify x, there is a possibility that the execution will abort. It follows that there is no postcondition that makes the specification {true} c0 ; x := cons(1, 2) ; c1 ; [x + 2] := 7 {?} valid. Sometimes, however, the notion of record boundaries dissolves, as in the following valid (and provable) specification of a program that tries to form a two-field record by gluing together two one-field records: {x 7→ − ∗ y 7→ −} if y = x + 1 then skip else if x = y + 1 then x := y else (dispose x ; dispose y ; x := cons(1, 2)) {x 7→ −, −}. (1.5)