1.4.ASSERTIONS 之 The remaining operations,for mutation,lookup,and deallocation,all cause memory faults (denoted by the terminal configuration abort)if an inactive address is dereferenced or deallocated.For example: Store x:3,y:4 Heap:empty Allocation x:=cons(1,2); Store:: Lookup y=X☒： Store x:37,y:1 Heap:37:1,38:2 Mutation+]:=3; abort 1.4 Assertions As in Hoare logic,assertions describe states,but now states contain heaps as Thus,in addition to the sual operati 兰e four ner ·emp (empty heap The heap is empty. ·e-e (singleton heap) The heap contains one cell,at address e with contents e'. D1*D2 (separating conjunction) The heap can be split into two disjoint parts such that p holds for one part and pa holds for the other. (se parating implication) If the heapis extended witha disjont part in then holds for the extended heap. It is also useful to introduce abbreviations for asserting that an address e is active: edf 3r'er'where r'not free in e.1.4. ASSERTIONS 11 The remaining operations, for mutation, lookup, and deallocation, all cause memory faults (denoted by the terminal configuration abort) if an inactive address is dereferenced or deallocated. For example: Store : x: 3, y: 4 Heap : empty Allocation x := cons(1, 2) ; ⇓ Store : x: 37, y: 4 Heap : 37: 1, 38: 2 Lookup y := [x] ; ⇓ Store : x: 37, y: 1 Heap : 37: 1, 38: 2 Mutation [x + 2] := 3 ; ⇓ abort 1.4 Assertions As in Hoare logic, assertions describe states, but now states contain heaps as well as stores. Thus, in addition to the usual operations and quantifiers of predicate logic, we have four new forms of assertion that describe the heap: • emp (empty heap) The heap is empty. • e 7→ e 0 (singleton heap) The heap contains one cell, at address e with contents e 0 . • p1 ∗ p2 (separating conjunction) The heap can be split into two disjoint parts such that p1 holds for one part and p2 holds for the other. • p1 −∗ p2 (separating implication) If the heap is extended with a disjoint part in which p1 holds, then p2 holds for the extended heap. It is also useful to introduce abbreviations for asserting that an address e is active: e 7→ − def = ∃x 0 . e 7→ x 0 where x 0 not free in e