Small Specifications for Tree Update

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 at the same level of abstraction as the data itself. In particular, they developed a formal specification of the Document Object Model, a W3C XML update library. Whilst they kept to the spirit of local reasoning, they were not able to retain small specifications: for example, the specification of ap-pendChild was not small. We show how to obtain small specifications by working with a more fine-grained context structure, allowing us to work with arbitrary tree fragments