Local Reasoning about Shared Mutable Data Structure

We describe an extension of Hoare's logic for reasoning about programs that alter data structures. We consider a low-level storage model based on a heap addressed by natural numbers, with associated lookup, update, allocation and deallocation operations, and arbitrary address arithmetic. The logic includes a spatial conjunction and spatial implication, which are used to decompose and compose specifications according to the areas of memory they refer to. We show how the formalism supports local reasoning: a specification and proof can concentrate on only those cells in memory that a program accesses. This is made possible using a rule for introducing frame axioms, which enables invariant properties for memory that a program does not access to be inferred automatically.