Abstract
Separation logic formalizes the idea of local reasoning for heap-manipulating programs via the frame rule and the separating conjunction P * Q, which describes states that can be split into \emph{separate} parts, with one satisfying P and the other satisfying Q. In standard separation logic, separation means physical separation. In this paper, we introduce \emph{fictional separation logic}, which includes more general forms of fictional separating conjunctions P * Q, where "*" does not require physical separation, but may also be used in situations where the memory resources described by P and Q overlap. We demonstrate, via a range of examples, how fictional separation logic can be used to reason locally and modularly about mutable abstract data types, possibly implemented using sophisticated sharing. Fictional separation logic is defined on top of standard separation logic, and both the meta-theory and the application of the logic is much simpler than earlier related approaches.
Originalsprog | Engelsk |
---|---|
Titel | Lecture Notes in Computer Science : 21st European Symposium on Programming, ESOP 2012, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. Proceedings |
Redaktører | Helmut Seidl |
Antal sider | 20 |
Vol/bind | 7211 |
Forlag | Springer |
Publikationsdato | 2012 |
Sider | 377-396 |
ISBN (Trykt) | 978-3-642-28868-5 |
ISBN (Elektronisk) | 978-3-642-28869-2 |
Status | Udgivet - 2012 |
Emneord
- Separation logic
- Heap-manipulating programs
- Fictional separation logic
- Mutable abstract data types
- Local reasoning