Philippa Gardner
Imperial College
Local Hoare Reasoning about DOM
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 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.
This talk describes joint
work with Gareth Smith, Mark Wheelhouse and Uri Zarfaty.
.
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, Calcagno, Gardner, and Zarfaty, POPL 2007.
Local Hoare Reasoning about DOM, Gardner, Smith, Wheelhouse, and
Zarfaty, PODS 2008.
Host:
John Reynolds
Appointments:
Margaret Weigand <weigand@cs.cmu.edu>
Wednesday, April 23, 2008
3:30 - 5:00 p.m.
Wean Hall 8220
Principles
of Programming Seminars