Jan Schwinghammer ; Lars Birkedal ; Bernhard Reus ; Hongseok Yang - Nested Hoare Triples and Frame Rules for Higher-order Store

lmcs:996 - Logical Methods in Computer Science, September 28, 2011, Volume 7, Issue 3 - https://doi.org/10.2168/LMCS-7(3:21)2011
Nested Hoare Triples and Frame Rules for Higher-order StoreArticle

Authors: Jan Schwinghammer ; Lars Birkedal ORCID; Bernhard Reus ORCID; Hongseok Yang

    Separation logic is a Hoare-style logic for reasoning about programs with heap-allocated mutable data structures. As a step toward extending separation logic to high-level languages with ML-style general (higher-order) storage, we investigate the compatibility of nested Hoare triples with several variations of higher-order frame rules. The interaction of nested triples and frame rules can be subtle, and the inclusion of certain frame rules is in fact unsound. A particular combination of rules can be shown consistent by means of a Kripke model where worlds live in a recursively defined ultrametric space. The resulting logic allows us to elegantly prove programs involving stored code. In particular, using recursively defined assertions, it leads to natural specifications and proofs of invariants required for dealing with recursion through the store.


    Volume: Volume 7, Issue 3
    Published on: September 28, 2011
    Imported on: March 8, 2011
    Keywords: Computer Science - Logic in Computer Science,F.3.1, F.3.2
    Funding:
      Source : OpenAIRE Graph
    • Resource Reasoning; Funder: UK Research and Innovation; Code: EP/H008373/1
    • Scalable Program Analysis for Software Verification; Funder: UK Research and Innovation; Code: EP/E053041/1
    • From Reasoning Principles for Function Pointers To Logics for Self-Configuring Programs; Funder: UK Research and Innovation; Code: EP/G003173/1

    11 Documents citing this article

    Consultation statistics

    This page has been seen 1418 times.
    This article's PDF has been downloaded 249 times.