Personal tools
You are here: Home Events Abstract Archives 2007-2008 Local Hoare Reasoning about DOM

Local Hoare Reasoning about DOM

Philippa Gardner Imperial College, London 4pm Tuesday 11th March 2008 Room 2511, JCMB, King's Buildings

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

Document Actions