|
⇤ ← Revision 1 as of 2011-02-03 16:33:28
Size: 658
Comment:
|
Size: 658
Comment:
|
| Deletions are marked like this. | Additions are marked like this. |
| Line 8: | Line 8: |
| {{http://www.cs.cmu.edu/~jcr/seplogic.pdf|John Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS 2002.}} | [[http://www.cs.cmu.edu/~jcr/seplogic.pdf|John Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS 2002.]] |
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.
The best way to start is to read the following paper by John Reynolds:
John Reynolds. Separation Logic: A Logic for Shared Mutable Data Structures. In LICS 2002.