Assertions Standard predicate logic assertions,plus ·emp (empty heap) The heap is empty. ●e→e (singleton heap) The heap contains one cell,at address e with contents e'. ●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
Assertions Standard predicate logic assertions, plus
Some Abbreviations e、 def a.e where a'not free in e ee der ee*true def e→e1,..,ene→e1*.·*e+n-1→en def e→e1,.·,em dere一e1*…*e十n-1一en ife一e1,.,en*true
Examples of Separating Conjunction 1.x3,y asserts that x points to an adjacent 3 pair of cells containing 3 and y. y 2.y→3，x asserts that y points to an adjacent y pair of cells containing 3 and x. 3.x一3，y*y一3，x asserts that situations (1)and(2)hold for separate parts of the heap
4.x一3，y∧y→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. 5.x一3，y∧y→3，x asserts that either (3)or (4)may hold,and that the heap may contain additional cells