(pronounced magic wand or separating implication) asserts that extending the heap with a disjoint part that satisfies its first argument results in a heap that satisfies its second argument. I.e,. when for every heap such that , also holds. The operators and share some properties with the classical conjunction and implication operators. They can be combined using an inference rule similar to modus ponens and they form an adjunction, i.e., if and only if for ; more precisely, the adjoint operators are and . Reasoning about programs: triples and proof rules In separation logic, Hoare triples have a slightly different meaning than in Hoare logic. The triple asserts that if the program executes from an initial state satisfying the precondition then the program will not go wrong (e.g., have undefined behaviour), and if it terminates, then the final state will satisfy the postcondition . In essence, during its execution, may access only memory locations whose existence is asserted in the precondition or that have been allocated by itself. In addition to the standard rules from Hoare logic, separation logic supports the following very important rule: This is known as the frame rule (named after the frame problem) and enables local reasoning. It says that a program that executes safely in a small state (satisfying ), can also execute in any bigger state (satisfying ) and that its execution will not affect the additional part of the state (and so will remain true in the postcondition). The side condition enforces this by specifying that none of the variables modified by occur free in , i.e. none of them are in the 'free variable' set of . Sharing Separation logic leads to simple proofs of pointer manipulation for data structures that exhibit regular sharing patterns which can be described simply using separating conjunctions; examples include singly and doubly linked lists and varieties of trees. Graphs and DAGs and other data structures with more general sharing are more difficult for both formal and informal proof. Separation logic has, nonetheless, been applied successfully to reasoning about programs with general sharing. In their POPL'01 paper, O'Hearn and Ishtiaq explained how the magic wand connective could be used to reason in the presence of sharing, at least in principle. For example, in the triple we obtain the weakest precondition for a statement that mutates the heap at location , and this works for any postcondition, not