Nested Hoare Triples and Frame Rules for Higher-order Store
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 va...
| Main Authors: | , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2011-09-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/996/pdf |
| _version_ | 1797268716975554560 |
|---|---|
| author | Jan Schwinghammer Lars Birkedal Bernhard Reus Hongseok Yang |
| author_facet | Jan Schwinghammer Lars Birkedal Bernhard Reus Hongseok Yang |
| author_sort | Jan Schwinghammer |
| collection | DOAJ |
| description | 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. |
| first_indexed | 2024-04-25T01:36:55Z |
| format | Article |
| id | doaj.art-b3e5a2d549b1449ebfffeb5a37bcdac4 |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:36:55Z |
| publishDate | 2011-09-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-b3e5a2d549b1449ebfffeb5a37bcdac42024-03-08T09:17:23ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742011-09-01Volume 7, Issue 310.2168/LMCS-7(3:21)2011996Nested Hoare Triples and Frame Rules for Higher-order StoreJan SchwinghammerLars Birkedalhttps://orcid.org/0000-0003-1320-0098Bernhard Reushttps://orcid.org/0000-0002-5807-856XHongseok YangSeparation 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://lmcs.episciences.org/996/pdfcomputer science - logic in computer sciencef.3.1, f.3.2 |
| spellingShingle | Jan Schwinghammer Lars Birkedal Bernhard Reus Hongseok Yang Nested Hoare Triples and Frame Rules for Higher-order Store Logical Methods in Computer Science computer science - logic in computer science f.3.1, f.3.2 |
| title | Nested Hoare Triples and Frame Rules for Higher-order Store |
| title_full | Nested Hoare Triples and Frame Rules for Higher-order Store |
| title_fullStr | Nested Hoare Triples and Frame Rules for Higher-order Store |
| title_full_unstemmed | Nested Hoare Triples and Frame Rules for Higher-order Store |
| title_short | Nested Hoare Triples and Frame Rules for Higher-order Store |
| title_sort | nested hoare triples and frame rules for higher order store |
| topic | computer science - logic in computer science f.3.1, f.3.2 |
| url | https://lmcs.episciences.org/996/pdf |
| work_keys_str_mv | AT janschwinghammer nestedhoaretriplesandframerulesforhigherorderstore AT larsbirkedal nestedhoaretriplesandframerulesforhigherorderstore AT bernhardreus nestedhoaretriplesandframerulesforhigherorderstore AT hongseokyang nestedhoaretriplesandframerulesforhigherorderstore |