Abstract

Local reasoning based on separation logic captures the natural local behaviour of programs by allowing reasoning to focus on the footprints of commands. In the semantic formalization of abstract separation logic, programs are modelled as “local functions” that act locally on abstract resource models. However, certain issues related to dynamic allocation force some non-intuitive choices in the general definition of locality, and lead to some unnatural outcomes. For example, the safety footprints of a program do not always yield a complete specification of the program, and one is forced to work with non-deterministic allocation in unbounded memory. We investigate these issues, and first present a formalization of “completeness footprints” which yield complete specifications. We then present an alternative memory model in which completeness footprints do correspond to safety footprints, and deterministic or bounded memory allocation can be modelled as local functions. More generally, a stronger notion of locality is identified which provides the correspondence between safety and completeness footprints for arbitrary resource models.