Editing Bunched logic (section)

=== Separation logic ===

Separation logic is an extension of [[Hoare logic]] that facilitates reasoning about mutable data structures that use [[pointer (computer programming)|pointer]]s.  Following Hoare logic the formulae of separation logic are of the form
<math>\{Pre\} program \{Post\}</math>, but the preconditions and postconditions are formulae interpreted in a model of bunched logic.
The original version of the logic was based on models as follows:
* <math> Heaps = L \rightharpoonup_f V \qquad </math> (finite [[partial function]]s from locations to values)
* <math> h_0 \bullet h_1 = </math> union of heaps with disjoint domains, undefined when domains overlap.
It is the undefinedness of the composition on overlapping heaps that models the separation idea. This is a model of the boolean variant of bunched logic.

Separation logic was used originally to prove properties of sequential programs, but then was extended to concurrency using a proof rule
:<math> \frac{\{P_1\} C_1 \{Q_1\} \quad \{P_2\} C_2 \{Q_2\}}{\{P_1 * P_2\} C_1 \parallel C_2 \{Q_1 * Q_2\}}</math>
that divides the storage accessed by parallel threads.<ref>{{cite journal|last1=O'Hearn|first1=Peter|title=Resources, Concurrency and Local Reasoning|journal=Theoretical Computer Science|date=2007|volume=375|issue=1–3|pages=271–307|doi=10.1016/j.tcs.2006.12.035|url=http://www0.cs.ucl.ac.uk/staff/p.ohearn/papers/concur04.pdf|doi-access=free}}</ref>

Later, the greater generality of the resource semantics was utilized: an abstract version of separation logic works for Hoare triples
where the preconditions and postconditions are formulae interpreted over an arbitrary partial commutative monoid instead of a particular heap model.<ref>{{cite book |doi=10.1109/LICS.2007.30|chapter-url=http://www.cs.ox.ac.uk/people/hongseok.yang/paper/asl-short.pdf|isbn=978-0-7695-2908-0|citeseerx=10.1.1.66.6337|chapter=Local Action and Abstract Separation Logic|title=22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007)|pages=366–378|year=2007|last1=Calcagno|first1=Cristiano|last2=O'Hearn|first2=Peter W.|last3=Yang|first3=Hongseok|s2cid=1044254}}</ref> 
By suitable choice of commutative monoid, it was surprisingly found that the proofs rules of abstract versions of concurrent separation logic could be used to reason about interfering concurrent processes, for example by encoding rely-guarantee and trace-based reasoning.<ref>{{cite journal|last1=Dinsdale-Young|first1=Thomas|last2=Birkedal|first2=Lars|last3=Gardner|first3=Philippa|last4=Parkinson|first4=Matthew|last5=Yang|first5=Hongseok|title=Views: Compositional Reasoning for Concurrent Programs|journal=Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages|volume=48|pages=287–300|date=2013|doi=10.1145/2480359.2429104|url=http://research.microsoft.com/pubs/180039/views.pdf}}</ref><ref>{{cite journal|last1=Sergey|first1=Ilya|last2=Nanevski|first2=Aleksandar|last3=Banerjee|first3=Anindya|title=Specifying and Verifying Concurrent Algorithms with Histories and Subjectivity|journal=24th European Symposium on Programming|date=2015|url=http://ilyasergey.net/papers/histories-esop15.pdf|bibcode=2014arXiv1410.0306S|arxiv=1410.0306}}</ref>

Separation logic is the basis of a number of tools for automatic and semi-automatic reasoning about programs, and is used in the Infer program analyzer currently deployed at Facebook.<ref>{{cite web|last1=Calcagno|first1=Cristiano|last2=Distefano|first2=Dino|last3=O'Hearn|first3=Peter|title=Open-sourcing Facebook Infer: Identify bugs before you ship|url=https://code.facebook.com/posts/1648953042007882/open-sourcing-facebook-infer-identify-bugs-before-you-ship/|date=2015-06-11}}</ref>