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