LFCS Seminar

A Compositional Specification of DOM using Context Logic

Philippa Gardner

Imperial College, London

2pm Friday 23rd November 2007
Room 2511, JCMB, King's Buildings

Note nonstandard day and time

---

Abstract

The Document Object Model (DOM) specifies an XML update library, and is maintained by the World Wide Web Consortium. DOM is used in many applications for accessing and updating XML. For example, consider a webpage with a button labelled `today's weather'; click on the button and embedded Javascript (using an implementation of DOM) puts `today's weather' in the tree.

DOM is written in English. It is therefore not compositional and not complete. We provide a concise, 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 and Reynold's pioneering techniques in 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 Zaraty on local Hoare reasoning about a simple tree-update language using Context Logic to this DOM application, showing that the Context-logic reasoning scales to DOM's more complicated tree structure and update language. Our reasoning not only formally specifies DOM, but can also be used to verify, for example, simple Javascript programs.

This is joint work with Gareth Smith, Mark Wheelhouse and Uri Zarfaty.