In computer science, separation logic is an extension of Hoare logic, a way of reasoning about programs. It was developed by John C. Reynolds, Peter O'Hearn, Samin Ishtiaq and Hongseok Yang, drawing upon early work by Rod Burstall. The assertion language of separation logic is a special case of the logic of bunched implications (BI).
Separation logic facilitates reasoning about:
- programs that manipulate pointer data structures — including information hiding in the presence of pointers;
- "transfer of ownership" (avoidance of semantic frame axioms); and
- virtual separation (modular reasoning) between concurrent modules.
Separation logic supports the developing field of research described by Peter O'Hearn and others as local reasoning, whereby specifications and proofs of a program component mention only the portion of memory used by the component, and not the entire global state of the system. Applications include automated program verification (where an algorithm checks the validity of another algorithm) and automated parallelization of software.
Assertions: operators and semantics
Separation logic assertions describe "states" consisting of a store and a heap, roughly corresponding to the state of local (or stack-allocated) variables and dynamically-allocated objects in common programming languages such as C and Java. A store is a function mapping variables to values. A heap is a partial function mapping memory addresses to values. Two heaps and are disjoint (denoted ) if their domains do not overlap (i.e., if for every memory address , at least one of and is undefined).
The logic allows to prove judgements of the form , where is a store, is a heap, and is an assertion over the given store and heap. Separation logic assertions (denoted as , , ) contain the standard boolean connectives and, in addition, , , , and , where and are expressions.
- The constant asserts that the heap is empty, i.e., when is undefined for all addresses.
- The binary operator takes an address and a value and asserts that the heap is defined at exactly one location, mapping the given address to the given value. I.e., when (where denotes the value of expression evaluated in store ) and is otherwise undefined.
- The binary operator (pronounced star or separating conjunction) asserts that the heap can be split into two disjoint parts where its two arguments hold, respectively. I.e., when there exist such that and and and .
- The binary operator (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.
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 .
- Reynolds, John C. (2002). "Separation Logic: A Logic for Shared Mutable Data Structures" (PDF). LICS.
- Reynolds, John C. (1999). "Intuitionistic Reasoning about Shared Mutable Data Structure". In Davies, Jim; Roscoe, Bill; Woodcock, Jim. Millennial Perspectives in Computer Science, Proceedings of the 1999 Oxford–Microsoft Symposium in Honour of Sir Tony Hoare. Palgrave.
- Ishtiaq, Samin; O'Hearn, Peter (2001). "BI as an Assertion Language for Mutable Data Structures". POPL (ACM).
- O'Hearn, Peter; Reynolds, John C.; Yang, Hongseok (2001). "Local Reasoning about Programs that Alter Data Structures". CSL.
- Burstall, R. M. (1972). "Some techniques for proving programs which alter data structures". Machine Intelligence 7.
- O'Hearn, P. W.; Pym, D. J. (June 1999). "The Logic of Bunched Implications". Bulletin of Symbolic Logic 5 (2): 215–244.
- The Ynot Project homepage, Harvard University, USA.
- Infer project page, GitHub.
- Separation logic and bi-abduction, page, Infer project site.