|
Size: 1863
Comment:
|
Size: 2536
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 5: | Line 5: |
| It introduces a new logical connective, *, called separating conjunction and proof rules for handling heap-manipulating commands. | '''Assertions.''' Separation logic assertions describe heaps. Besides the normal logical connectives (conjunction, disjunction, implication, etc), SL introduces the separating conjunction (<<latex($*$)>>) of two assertions. A heap satisfies the separating conjunction of two assertions if it can be divided into two disjoint parts satisfying the two assertions. Formally, <<latex($h \models P_1 * P_2$)>> if and only if there exist (disjoint) <<latex($h_1$)>> and <<latex($h_2$)>> such that <<latex($h = h_1 \uplus h_2$)>> and <<latex($h_1 \models P_1$)>> and <<latex($h_2 \models P_2$)>>. |
| Line 7: | Line 7: |
| <<latex(\mbox{$h \models P_1 * P_2$ if and only if there exist $h_1, h2$ such that $h = h_1 \uplus h_2$ and $h_1 \models P_1$ and $h_2 \models P_2$})>> The most prominent proof rule is the frame rule: |
'''Proof rules.''' SL inherits the standard rules and axioms of Hoare logic, has its own proof rules for heap-manipulating commands, and the all-important frame rule. |
| Line 16: | Line 13: |
| The best way to start is to read the following survey paper by John Reynolds: | The frame rule enables ''local reasoning'': the specification of a program need only mention the portion of the heap used by the program. |
| Line 18: | Line 15: |
| [[http://www.cs.cmu.edu/~jcr/seplogic.pdf|Separation Logic: A Logic for Shared Mutable Data Structures.]] JC Reynolds. In LICS 2002. | === Introductory material === |
| Line 20: | Line 17: |
| * [[http://www.cs.cmu.edu/~jcr/seplogic.pdf|Separation Logic: A Logic for Shared Mutable Data Structures.]] JC Reynolds. In LICS 2002. This is the best introduction to separation logic. | |
| Line 21: | Line 19: |
| Extensions of separation logic have been devised to better handle: | === Extensions of Separation Logic === There are extensions of separation logic: |
| Line 28: | Line 28: |
| === Tool support === |
|
| Line 30: | Line 32: |
| ToolSupport | For more information, see [[ToolSupport]]. === Further reading === TODO |
Separation logic
Separation logic is an extension of Hoare's logic oriented to reasoning about mutable data structures (or, programs with dynamically allocated pointers). It enables more compact proofs and specs of imperative programs than before because of its support for local reasoning, where specifications and proofs concentrate on the portion of memory used by a program component, and not the entire global state of the system.
Assertions. Separation logic assertions describe heaps. Besides the normal logical connectives (conjunction, disjunction, implication, etc), SL introduces the separating conjunction (
) of two assertions. A heap satisfies the separating conjunction of two assertions if it can be divided into two disjoint parts satisfying the two assertions. Formally, 
if and only if there exist (disjoint) 
and 
such that 
and 
and 
.
Proof rules. SL inherits the standard rules and axioms of Hoare logic, has its own proof rules for heap-manipulating commands, and the all-important frame rule.
This says that a program that runs correctly with a heap satifying its precondition also runs correctly with a bigger initial heap. Further, it is guaranteed not to touch the additional portion heap.
The frame rule enables local reasoning: the specification of a program need only mention the portion of the heap used by the program.
Introductory material
Separation Logic: A Logic for Shared Mutable Data Structures. JC Reynolds. In LICS 2002. This is the best introduction to separation logic.
Extensions of Separation Logic
There are extensions of separation logic:
- Abstraction (hypothetical frame rule, abstract predicates, context logic)
Concurrency (CSL, locks-in-the-heap, RGSep/SAGL/LRG, deny-guarantee)
- Assembly code
- Higher-order functions
Tool support
Separation logic has also been extensively used in semi-automatic and automatic program analyses (often known as shape analyses) for proving functional correctness of programs or simply the absence of certain kinds of runtime errors and/or memory leaks.
For more information, see ToolSupport.
Further reading
TODO