Overview
Separation logic facilitates reasoning about: * programs that manipulate pointer data structures—includingAssertions: 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 andReasoning about programs: triples and proof rules
In separation logic, Hoare triples have a slightly different meaning than inSharing
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 only one that is laid out neatly using the separating conjunction. This idea was taken much further by Yang, who used to provide localized reasoning about mutations in the classic Schorr-Waite graph marking algorithm. Finally, one of the most recent works in this direction is that of Hobor and Villard, who employ not only but also a connective which has variously been called overlapping conjunction or sepish, and which can be used to describe overlapping data structures: holds of a heap when and hold for subheaps and whose union is , but which possibly have a nonempty portion in common. Abstractly, can be seen to be a version of the fusion connective ofConcurrent separation logic
A Concurrent Separation Logic (CSL), a version of separation logic for concurrent programs, was originally proposed by Peter O'Hearn, using a proof rule : which allows independent reasoning about threads that access separate storage. O'Hearn's proof rules adapted an early approach ofVerification and program analysis tools
Tools for reasoning about programs fall on a spectrum from fully automatic program analysis tools, which do not require any user input, to interactive tools where the human is intimately involved in the proof process. Many such tools have been developed; the following list includes a few representatives in each category. *Automatic Program Analyses. These tools typically look for restricted classes of bugs (e.g., memory safety errors) or attempt to prove their absence, but fall short of proving full correctness. ** A current example is Facebook Infer, a static analysis tool for Java, C, andReferences
{{Program analysis 2002 introductions Program logic Substructural logic Logic in computer science