Fictional Separation Logic

Jonas Buhrkal Jensen, Lars Birkedal

    Research output: Conference Article in Proceeding or Book/Report chapterArticle in proceedingsResearchpeer-review

    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.
    Original languageEnglish
    Title of host publicationLecture 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
    EditorsHelmut Seidl
    Number of pages20
    Volume7211
    PublisherSpringer
    Publication date2012
    Pages377-396
    ISBN (Print)978-3-642-28868-5
    ISBN (Electronic)978-3-642-28869-2
    Publication statusPublished - 2012

    Cite this