Footprints in local reasoning
File(s)0903.1032v2.pdf (243.83 KB)
Published version
Author(s)
Raza, M
Gardner, P
Type
Conference Paper
Abstract
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.
Date Issued
2009-01-01
Date Acceptance
2008-03-29
Citation
Logical Methods in Computer Science, 2009, 5 (2)
ISSN
1860-5974
Publisher
Logical Methods in Computer Science e.V.
Journal / Book Title
Logical Methods in Computer Science
Volume
5
Issue
2
Copyright Statement
© The Author(s) 2009. This article is available under a CC BY ND 2.0 license.
Source
11th International Conference on Foundations of Software Science and Computational Structures
Subjects
Science & Technology
Technology
Computer Science, Theory & Methods
Logic
Computer Science
Science & Technology - Other Topics
COMPUTER SCIENCE, THEORY & METHODS
LOGIC
footprints
separation logic
local reasoning
SEPARATION LOGIC
SEMANTICS
RESOURCES
cs.SE
cs.LO
D.2.4; F.3.1
0101 Pure Mathematics
0803 Computer Software
0802 Computation Theory And Mathematics
Publication Status
Published
Start Date
2008-03-29
Finish Date
2008-04-06
Coverage Spatial
Budapest, Hungary