More Web Proxy on the site http://driver.im/

research-article

Local Hoare reasoning about DOM

Authors:

Philippa A. Gardner,

Gareth D. Smith,

Mark J. Wheelhouse,

Uri D. ZarfatyAuthors Info & Claims

PODS '08: Proceedings of the twenty-seventh ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems

Pages 261 - 270

https://doi.org/10.1145/1376916.1376953

Published: 09 June 2008 Publication History

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.

References

[1]

J. Berdine, C. Calcagno, B. Cook, D. Distefano, P. O'Hearn, T. Wies, and H. Yang. Shape analysis for composite data structures. In CAV, 2007.]]

Digital Library

[2]

J. Berdine, C. Calcagno, and P. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO, 2006.]]

Digital Library

[3]

J. Berdine, C. Calcagno, and P. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In FMCO, 2006.]]

Digital Library

[4]

C. Calcagno, P. Gardner, and U. Zarfaty. Context logic as modal logic: Completeness and parametric inexpressivity. In POPL, 2007.]]

Digital Library

[5]

P. Gardner, G. Smith, M. Wheelhouse, and U. Zarfaty. Local Hoare reasoning about DOM. Extended version, available online at http://www.doc.ic.ac.uk/~pg/publications.html.]]

Digital Library

[6]

S. Isthiaq and P. O'Hearn. BI as an assertion language for mutable data structures. In POPL, 2001.]]

Digital Library

[7]

P. O'Hearn, J. Reynolds, and H. Yang. Local reasoning about programs that alter data structures. In CSL, 2001.]]

Digital Library

[8]

P. W. O'Hearn. Resources, concurrency and local reasoning. TCS, 375(1-3):271--307, May 2007.]]

Digital Library

[9]

J. Orendorff. Compliance Patches for minidom. Included with Python, 2007. See http://bugs.python.org/issue1704134.]]

[10]

G. Smith. A context logic approach to the analysis and specification of xml update. PhD 1st year report, 2006.]]

[11]

Various. xml.dom.minidom, 2006. http://docs.python.org/lib/module-xml.dom.minidom.html.]]

[12]

W3C. Document Object Model (DOM) Level 1 Specification (2nd Ed.). Working draft, 2000. http://www.w3.org/TR/2000/WD-DOM-Level-1-20000929/.]]

[13]

W3C. DOM: Document Object Model. W3C recommendation, 2005. See http://www.w3.org/DOM/.]]

[14]

M. Wheelhouse. DOM: Towards a formal specification. Master's thesis, Imperial College, 2007.]]

[15]

U. Zarfaty and P. Gardner. Local reasoning about tree update. In MFPS, 2006.]]

Digital Library

Cited By

Fragoso Santos JMaksimović PSampaio GGardner P(2019)JaVerT 2.0: compositional symbolic execution for JavaScriptProceedings of the ACM on Programming Languages10.1145/32903793:POPL(1-31)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290379
Gardner PSabel DThiemann P(2018)JaVerTProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236974(1-4)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3236950.3236974
Elyasov APrasetya IHage J(2018)Search-Based Test Data Generation for JavaScript Functions that Interact with the DOM2018 IEEE 29th International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE.2018.00020(88-99)Online publication date: Oct-2018
https://doi.org/10.1109/ISSRE.2018.00020
Show More Cited By

Index Terms

Local Hoare reasoning about DOM
1. Theory of computation
  1. Logic
  2. Semantics and reasoning
    1. Program reasoning

Recommendations

A space efficient XML DOM parser

In many XML applications, parsing is a key operation. When the processing involves modifying data, random access, and/or in an order different from the one in which elements are stored, a DOM parser has to be used. A major problem with using a DOM ...
A Study on Efficiency of Markup Language Using DOM Tree

DOM and SAX are used usually in form parser for XML document processing. This study designed method of markup language using DOM tree extension and advantage about fast accessibility for XML document. Did so that can design simple type and complex type ...
The Research and Implementation of JDF Job Ticket Management Based on DOM
ICSEM '10: Proceedings of the 2010 International Conference on System Science, Engineering Design and Manufacturing Informatization - Volume 01

JDF (Job Definition Format) is an industry standard designed to describe job information and exchange data between different applications or systems in printing industry. According to the characteristic of JDF job ticket in XML (extensible Markup ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PODS '08: Proceedings of the twenty-seventh ACM SIGMOD-SIGACT-SIGART symposium on Principles of database systems

June 2008

330 pages

ISBN:9781605581521

DOI:10.1145/1376916

General Chair:
Phokion Kolaitis
IBM Almaden Research Center, USA
,
Program Chair:
Maurizio Lenzerini
SAPIENZA University of Rome, Italy

Copyright © 2008 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 June 2008

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

SIGMOD/PODS '08

Sponsor:

SIGMOD/PODS '08: SIGMOD/PODS '08 - International Conference on Management of Data

June 9 - 12, 2008

Vancouver, Canada

Acceptance Rates

PODS '08 Paper Acceptance Rate 28 of 159 submissions, 18%;

Overall Acceptance Rate 642 of 2,707 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

32
Total Citations
View Citations
374
Total Downloads

Downloads (Last 12 months)5
Downloads (Last 6 weeks)2

Reflects downloads up to 09 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Fragoso Santos JMaksimović PSampaio GGardner P(2019)JaVerT 2.0: compositional symbolic execution for JavaScriptProceedings of the ACM on Programming Languages10.1145/32903793:POPL(1-31)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290379
Gardner PSabel DThiemann P(2018)JaVerTProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236974(1-4)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3236950.3236974
Elyasov APrasetya IHage J(2018)Search-Based Test Data Generation for JavaScript Functions that Interact with the DOM2018 IEEE 29th International Symposium on Software Reliability Engineering (ISSRE)10.1109/ISSRE.2018.00020(88-99)Online publication date: Oct-2018
https://doi.org/10.1109/ISSRE.2018.00020
Sun KRyu S(2017)Analysis of JavaScript ProgramsACM Computing Surveys10.1145/310674150:4(1-34)Online publication date: 25-Aug-2017
https://dl.acm.org/doi/10.1145/3106741
Raad ASantos JGardner P(2016)DOM: Specification and Client ReasoningProgramming Languages and Systems10.1007/978-3-319-47958-3_21(401-422)Online publication date: 9-Oct-2016
https://doi.org/10.1007/978-3-319-47958-3_21
Genevès PGesbert N(2015)XQuery and static typing: tackling the problem of backward axesACM SIGPLAN Notices10.1145/2858949.278474650:9(88-100)Online publication date: 29-Aug-2015
https://dl.acm.org/doi/10.1145/2858949.2784746
Genevès PGesbert NFisher KReppy J(2015)XQuery and static typing: tackling the problem of backward axesProceedings of the 20th ACM SIGPLAN International Conference on Functional Programming10.1145/2784731.2784746(88-100)Online publication date: 29-Aug-2015
https://dl.acm.org/doi/10.1145/2784731.2784746
Park CWon SJin JRyu SCohen MGrunske LWhalen M(2015)Static analysis of JavaScript web applications in the wild via practical DOM modelingProceedings of the 30th IEEE/ACM International Conference on Automated Software Engineering10.1109/ASE.2015.27(552-562)Online publication date: 9-Nov-2015
https://dl.acm.org/doi/10.1109/ASE.2015.27
Gardner PRaad AWheelhouse MWright A(2014)Abstract Local Reasoning for Concurrent LibrariesElectronic Notes in Theoretical Computer Science (ENTCS)10.1016/j.entcs.2014.10.009308:C(147-166)Online publication date: 29-Oct-2014
https://dl.acm.org/doi/10.1016/j.entcs.2014.10.009
Gardner PNtzik GWright A(2014)Local Reasoning for the POSIX File SystemProceedings of the 23rd European Symposium on Programming Languages and Systems - Volume 841010.1007/978-3-642-54833-8_10(169-188)Online publication date: 5-Apr-2014
https://dl.acm.org/doi/10.1007/978-3-642-54833-8_10
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents