Mohammad Raza ; Philippa Gardner - Footprints in Local Reasoning

lmcs:1118 - Logical Methods in Computer Science, April 24, 2009, Volume 5, Issue 2 - https://doi.org/10.2168/LMCS-5(2:4)2009
Footprints in Local ReasoningArticle

Authors: Mohammad Raza ; Philippa Gardner

    Local reasoning about programs exploits the natural local behaviour common in programs by focussing on the footprint - that part of the resource accessed by the program. We address the problem of formally characterising and analysing the footprint notion for abstract local functions introduced by Calcagno, O Hearn and Yang. With our definition, we prove that the footprints are the only essential elements required for a complete specification of a local function. We formalise the notion of small specifications in local reasoning and show that for well-founded resource models, a smallest specification always exists that only includes the footprints, and also present results for the non-well-founded case. Finally, we use this theory of footprints to investigate the conditions under which the footprints correspond to the smallest safe states. We present a new model of RAM in which, unlike the standard model, the footprints of every program correspond to the smallest safe states, and we also identify a general condition on the primitive commands of a programming language which guarantees this property for arbitrary models.


    Volume: Volume 5, Issue 2
    Published on: April 24, 2009
    Imported on: September 1, 2008
    Keywords: Computer Science - Software Engineering,Computer Science - Logic in Computer Science,D.2.4,F.3.1

    6 Documents citing this article

    Consultation statistics

    This page has been seen 1695 times.
    This article's PDF has been downloaded 307 times.