Nested Hoare Triples and Frame Rules for Higher-order Store

Jan Schwinghammer; Lars Birkedal; Bernhard Reus; Hongseok Yang

doi:10.2168/LMCS-7(3:21)2011

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 ; Bernhard Reus ; 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.

https://doi.org/10.2168/LMCS-7(3:21)2011

Source: arXiv.org:1109.3031

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

Licence: arXiv.org - Non-exclusive license to distribute

Funding:

Source : OpenAIRE Graph

Scalable Program Analysis for Software Verification; Funder: UK Research and Innovation; Code: EP/E053041/1
Resource Reasoning; Funder: UK Research and Innovation; Code: EP/H008373/1
From Reasoning Principles for Function Pointers To Logics for Self-Configuring Programs; Funder: UK Research and Innovation; Code: EP/G003173/1

Classifications

Mathematics Subject Classification 2020¹

Sources:

[1] zbMATH Open.

Bibliographic References

11 Documents citing this article

Ayesha Sadiq;Yuan-Fang Li;Sea Ling, 2019, A survey on the use of access permission-based specifications for program verification, Journal of Systems and Software, 159, pp. 110450, 10.1016/j.jss.2019.110450.

Willem Penninckx;Amin Timany;Bart Jacobs, Zenodo (CERN European Organization for Nuclear Research), Specifying I/O using abstract nested hoare triples in separation logic, 2142, pp. 1-7, 2019, London United Kingdom, 10.1145/3340672.3341118, https://zenodo.org/record/3354956.

José Fragoso Santos;Philippa Gardner;Petar Maksimović;Daiva Naudžiūnienė, Spiral (Imperial College London), Towards Logic-Based Verification of JavaScript Programs, pp. 8-25, 2017, 10.1007/978-3-319-63046-5_2, http://hdl.handle.net/10044/1/55840.

Arlen Cox;Bor-Yuh Evan Chang;Xavier Rival, Lecture notes in computer science, Desynchronized Multi-State Abstractions for Open Programs in Dynamic Languages, pp. 483-509, 2015, 10.1007/978-3-662-46669-8_20, https://doi.org/10.1007/978-3-662-46669-8_20.

Bernhard Reus;Nathaniel Charlton;Ben Horsfall, 2014, Symbolic Execution Proofs for Higher Order Store Programs, Sussex Research Online (University of Sussex), 54, 3, pp. 199-284, 10.1007/s10817-014-9319-8, http://sro.sussex.ac.uk/id/eprint/53364/2/paper.pdf.

Nick Benton;Martin Hofmann;Vivek Nigam, arXiv (Cornell University), Abstract effects and proof-relevant logical relations, 2014, San Diego California USA, 10.1145/2535838.2535869, https://arxiv.org/abs/1212.5692.

Nick Benton;Martin Hofmann;Vivek Nigam, 2014, Abstract effects and proof-relevant logical relations, ACM SIGPLAN Notices, 49, 1, pp. 619-631, 10.1145/2578855.2535869, https://doi.org/10.1145/2578855.2535869.

Kasper Svendsen;Lars Birkedal;Matthew Parkinson, Lecture notes in computer science, Joins: A Case Study in Modular Specification of a Concurrent Reentrant Higher-Order Library, pp. 327-351, 2013, 10.1007/978-3-642-39038-8_14.

Kasper Svendsen;Lars Birkedal;Matthew Parkinson, Lecture notes in computer science, Modular Reasoning about Separation of Concurrent Data Structures, pp. 169-188, 2013, 10.1007/978-3-642-37036-6_11, https://doi.org/10.1007/978-3-642-37036-6_11.

Luís Caires;João C. Seco, 2013, The type discipline of behavioral separation, CiteSeer X (The Pennsylvania State University), 48, 1, pp. 275-286, 10.1145/2480359.2429103, http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.304.4146.

Ben Horsfall;Nathaniel Charlton;Bernhard Reus, Proceedings of the 14th Workshop on Formal Techniques for Java-like Programs, Verifying the reflective visitor pattern, pp. 27-34, 2012, Beijing China, 10.1145/2318202.2318208.

Sources : OpenCitations, OpenAlex & Crossref

Share and export

Consultation statistics

This page has been seen 1855 times.

This article's PDF has been downloaded 284 times.