University of Sussex
Browse

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

History

Publication status

  • Published

Journal

Information and Computation

ISSN

0890-5401

Publisher

Elsevier

Volume

231

Page range

167-203

Department affiliated with

  • Informatics Publications

Full text available

  • No

Peer reviewed?

  • Yes

Legacy Posted Date

2013-11-07

Usage metrics

    University of Sussex (Publications)

    Categories

    No categories selected

    Exports

    RefWorks
    BibTeX
    Ref. manager
    Endnote
    DataCite
    NLM
    DC