Specification patterns for reasoning about recursion through the store

Charlton, Nathaniel and Reus, Bernhard (2013) Specification patterns for reasoning about recursion through the store. Information and Computation, 231. pp. 167-203. ISSN 0890-5401

Full text not available from this repository.

Abstract

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.

Item Type: Article
Schools and Departments: School of Engineering and Informatics > Informatics
Subjects: Q Science > QA Mathematics > QA0075 Electronic computers. Computer science
Depositing User: Bernhard Reus
Date Deposited: 07 Nov 2013 09:15
Last Modified: 07 Nov 2013 09:15
URI: http://sro.sussex.ac.uk/id/eprint/46963
📧 Request an update