Local Reasoning about Shared Mutable Data Structure

Peter O'Hearn, John Reynolds, Hongseok Yang

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.