Computer Science – Software Engineering
Scientific paper
2009-03-05
LMCS 5 (2:4) 2009
Computer Science
Software Engineering
LMCS 2009 (FOSSACS 2008 special issue)
Scientific paper
10.2168/LMCS-5(2:4)2009
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.
Gardner Philippa
Raza Mohammad
No associations
LandOfFree
Footprints in Local Reasoning does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Footprints in Local Reasoning, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Footprints in Local Reasoning will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-115626