Small Specifications for Tree Update (Full Version)

Abstract. O’Hearn, Reynolds and Yang introduced local Hoare reason-ing about mutable data structures using Separation Logic. They reason about the local parts of the memory accessed by programs, and thus con-struct their smallest complete specifications. Gardner et al. generalised their work, using Context Logic to reason about structured data update. In particular, they developed a formal specification of the Document Ob-ject Model, a W3C XML update library. Whilst they kept to the spirit of local reasoning, they were not able to retain small specifications: for ex-ample, the specification of appendChild was not small. In this paper we introduce Segment Logic which provides a more fine-grained analysis of the tree structure and yields small specifications. As well as being aes-thetically pleasing, such small axioms are essential for reasoning about concurrent tree update