### Abstract

In this AFP entry, we formalize the core of the Safely Composable Document Object Model (SC DOM). The SC DOM improve the standard DOM (as formalized in the AFP entry “Core DOM”) by strengthening the tree boundaries set by shadow roots: in the SC DOM, the shadow root is a sub-class of the document class (instead of a base class). This modifications also results in changes to some API methods (e.g., getOwnerDocument) to return the nearest shadow root rather than the document root. As a result, many API methods that, when called on a node inside a shadow tree, would previously “break out” and return or modify nodes that are possibly outside the shadow tree, now stay within its boundaries. This change in behavior makes programs that operate on shadow trees more predictable for the developer and allows them to make more assumptions about other code accessing the DOM.

### License

BSD License

### Topics

- Computer science/Data structures

### Session Core_SC_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 Safely Composable Document Object Model with Shadow Roots

## Cite

×

Core_SC_DOM-AFP

    @article{Core_SC_DOM-AFP,
      author  = {Achim D. Brucker and Michael Herzberg},
      title   = {The Safely Composable DOM},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Core_SC_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
- Nov 26, 2020 : Isabelle2020