File(s) not publicly available
Specification patterns for reasoning about recursion through the store
journal contribution
posted on 2023-06-08, 16:17 authored by Nathaniel Charlton, Bernhard ReusBernhard ReusHigher-order store means that code can be stored on the mutable heap that programs manipulate, and is the basis of flexible software that can be changed or reconfigured at runtime. Specifying such programs is challenging because higher-order store allows recursion through the store, where new (mutual) recursions between code are set up on the fly. This paper presents a series of formal specification patterns that capture increasingly complex uses of recursion through the store. To express the necessary specifications we extend the separation logic for higher-order store given by Schwinghammer et al. (CSL, 2009), adding parameter passing, and certain recursively defined families of assertions. We give proof rules for our extended logic and show their soundness. Finally, we apply our specification patterns and rules to an example program that exploits many of the possibilities offered by higher-order store; this is the first larger case study conducted with logical techniques based on work by Schwinghammer et al. (CSL, 2009), and shows that they are practical.
History
Publication status
- Published
Journal
Information and ComputationISSN
0890-5401Publisher
ElsevierExternal DOI
Volume
231Page range
167-203Department affiliated with
- Informatics Publications
Full text available
- No
Peer reviewed?
- Yes
Legacy Posted Date
2013-11-07Usage metrics
Categories
No categories selectedKeywords
Licence
Exports
RefWorks
BibTeX
Ref. manager
Endnote
DataCite
NLM
DC