O'Hearn, Reynolds and Yang introduced local Hoare reasoning about mutable data
structures using separation logic. They reason about the local parts of the memory
accessed by programs, and thus construct their smallest complete specifications.
Gardner et al. generalised their work, using context logic to reason about structured
data at the same level of abstraction as the data itself. In particular, we developed
a formal specification of the Document Object Model (DOM), a W3C XML update
library. Whilst we kept to the spirit of local reasoning, we were not able to retain
small specifications for all of the commands of DOM: for example, our specification
of the appendChild command was not small.
We show how to obtain such small specifications by developing a more fine-grained
context structure, allowing us to work with arbitrary segments of a data structure.
We introduce segment logic, a logic for reasoning about such segmented data structures, staring at first with a simple tree structure, but then showing how to generalise
our approach to arbitrary structured data.
Using our generalised segment logic we construct a reasoning framework for abstract program modules, showing how to reason about such modules at the client
level. In particular we look at modules for trees, lists, heaps and the more complex
data model of DOM.
An important part of any abstraction technique is an understanding of how to
link the abstraction back to concrete implementations. Building on our previous
abstraction and refinement work for local reasoning, we show how to soundly implement the segment models used in our abstract reasoning. In particular we show how
to implement our fine-grained list and tree modules so that their abstract specifications are satisfied by the concrete implementations. We also show how our reasoning
from the abstract level can be translated to reasoning at the concrete level.
Finally, we turn our attention to concurrency and show how having genuine small
axioms for our commands allows for a simple treatment of abstract level concurrency
constructs.