|
A
Formal
Model
of
the
Document
Object
Model
Title: |
A Formal Model of the Document Object Model |
Authors:
|
Achim D. Brucker and
Michael Herzberg
|
Submission date: |
2018-12-26 |
Abstract: |
In this AFP entry, we formalize the core of the Document Object Model
(DOM). At its core, the DOM defines a tree-like data structure for
representing documents in general and HTML documents in particular. It
is the heart of any modern web browser. Formalizing the key concepts
of the DOM is a prerequisite for the formal reasoning over client-side
JavaScript programs and for the analysis of security concepts in
modern web browsers. We present a formalization of the core DOM, with
focus on the node-tree and the operations defined on node-trees, in
Isabelle/HOL. We use the formalization to verify the functional
correctness of the most important functions defined in the DOM
standard. Moreover, our formalization is 1) extensible, i.e., can be
extended without the need of re-proving already proven properties and
2) executable, i.e., we can generate executable code from our
specification. |
BibTeX: |
@article{Core_DOM-AFP,
author = {Achim D. Brucker and Michael Herzberg},
title = {A Formal Model of the Document Object Model},
journal = {Archive of Formal Proofs},
month = dec,
year = 2018,
note = {\url{https://isa-afp.org/entries/Core_DOM.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Used by: |
Shadow_DOM |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|