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 associative1.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