The W3C Document Object Model (DOM) specifies an XML update library. DOM is written in English, and is therefore not compositional and not complete. We provide a first step towards a compositional specification of DOM. Unlike DOM, we are able to work
with a minimal set of commands and obtain a complete reasoning for straight-line code. Our work transfers O’Hearn, Reynolds
and Yang’s local Hoare reasoning for analysing heaps to XML,
viewing XML as an in-place memory store as does DOM. In particular, we apply recent work by Calcagno, Gardner and Zarfaty
on local Hoare reasoning about a simple tree-update language to
DOM, showing that our reasoning scales to DOM. Our reasoning
not only formally specifies a significant subset of DOM Core Level
1, but can also be used to verify e.g. invariant properties of simple
Javascript programs.