### 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.

### License

BSD License

### Topics

- Computer science/Data structures

### Session Core_DOM

- Hiding_Type_Variables
- Ref
- Core_DOM_Basic_Datatypes
- BaseClass
- Heap_Error_Monad
- BaseMonad
- ObjectPointer
- ObjectClass
- ObjectMonad
- NodePointer
- NodeClass
- NodeMonad
- ElementPointer
- CharacterDataPointer
- DocumentPointer
- ShadowRootPointer
- ElementClass
- ElementMonad
- CharacterDataClass
- CharacterDataMonad
- DocumentClass
- DocumentMonad
- Core_DOM_Functions
- Core_DOM_Heap_WF
- Core_DOM
- Testing_Utils
- Core_DOM_BaseTest
- Document_adoptNode
- Document_getElementById
- Node_insertBefore
- Node_removeChild
- Core_DOM_Tests

### Used by

- A Formal Model of the Document Object Model with Shadow Roots

## Cite

×

Core_DOM-AFP

    @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   = {December},
      year    = {2018},
      note    = {\url{https://isa-afp.org/entries/Core_DOM.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Jan 7, 2019 : Isabelle2018