Details

Autor(en) / Beteiligte

• Gardner, Philippa A.
• Smith, Gareth D.
• Wheelhouse, Mark J.
• Zarfaty, Uri D.

Titel

Local Hoare reasoning about DOM

Ist Teil von

• Proceedings of the twenty-seventh ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems, 2008, p.261-270

Ort / Verlag

New York, NY, USA: ACM

Erscheinungsjahr

2008

Link zum Volltext

Quelle

ACM Digital Library

Beschreibungen/Notizen

• 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 simple tree update to this real-world DOM application. Our reasoning not only formally specifies a significant subset of DOM Core Level 1, but can also be used to verify, for example, invariant properties of simple Javascript programs.