Specification patterns for reasoning about recursion through the store

Higher-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.

Authors

• Nathaniel Charlton
• Bernhard Reus

Keywords

• Hoare logic
• Higher-order store
• Separation logic