Local Hoare Reasoning about DOM
File(s)
Accepted version
Author(s)
Gardner, PA
Smith, G
Wheelhouse, M
Zarfaty, U
Type
Conference Paper
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 OHearn, Reynolds and Yangs 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. Copyright 2008 ACM.
Date Issued
2008
Citation
2008, pp.261-270
ISBN
978-1-60558-152-1
Publisher
ACM
Start Page
261
End Page
270
Copyright Statement
© 2008 ACM. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in PODS 2008, http://doi.acm.org/10.1145/1376916.1376953
Source
27th ACM SIGMOD-SIGACT-SIGART Symposium on Principles of Database Systems (PODS 2008)
Start Date
2008-06-09
Finish Date
2008-06-11
Coverage Spatial
Vancouver, Canada