Abstract
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 using Context Logic to this DOM application, showing that our
reasoning scales to DOM's more complicated tree structure and update language.. 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.
References:
Local Hoare Reasoning about Data Update, Calcagno, Gardner, and Zarfaty, POPL 2005 and
Plotkin's festschrift
Context Logic as Modal Logic: Completeness and Parametric Inexpressivity, PCalcagno,
Gardner, and Zarfaty, POPL 2007
Local Hoare Reasoning about DOM, Gardner, Smith, Wheelhouse, and Zarfaty, PODS 2008, to
appear.
Joint work with: Gareth Smith, Mark Wheelhouse and Uri Zarfaty