Footprints in Local Reasoning

Local reasoning about programs exploits the natural local behaviour common inprograms by focussing on the footprint - that part of the resource accessed bythe program. We address the problem of formally characterising and analysingthe footprint notion for abstract local functions introduced by Calcagno, OHearn and Yang. With our definition, we prove that the footprints are the onlyessential elements required for a complete specification of a local function.We formalise the notion of small specifications in local reasoning and showthat for well-founded resource models, a smallest specification always existsthat only includes the footprints, and also present results for thenon-well-founded case. Finally, we use this theory of footprints to investigatethe conditions under which the footprints correspond to the smallest safestates. We present a new model of RAM in which, unlike the standard model, thefootprints of every program correspond to the smallest safe states, and we alsoidentify a general condition on the primitive commands of a programminglanguage which guarantees this property for arbitrary models.Comment: LMCS 2009 (FOSSACS 2008 special issue