### Abstract

In this AFP entry, we extend our formalization of the safely composable DOM with Shadow Roots. This is a proposal for Shadow Roots with stricter safety guarantess than the standard compliant formalization (see "Shadow DOM"). Shadow Roots are a recent proposal of the web community to support a component-based development approach for client-side web applications. Shadow roots are a significant extension to the DOM standard and, as web standards are condemned to be backward compatible, such extensions often result in complex specification that may contain unwanted subtleties that can be detected by a formalization. Our Isabelle/HOL formalization is, in the sense of object-orientation, an extension of our formalization of the core DOM and enjoys the same basic properties, i.e., it is extensible, i.e., can be extended without the need of re-proving already proven properties and executable, i.e., we can generate executable code from our specification. We exploit the executability to show that our formalization complies to the official standard of the W3C, respectively, the WHATWG.

### License

BSD License

### Topics

- Computer science/Data structures

### Session Shadow_SC_DOM

- ShadowRootClass
- ShadowRootMonad
- Shadow_DOM
- Shadow_DOM_BaseTest
- slots
- slots_fallback
- Shadow_DOM_Document_adoptNode
- Shadow_DOM_Document_getElementById
- Shadow_DOM_Node_insertBefore
- Shadow_DOM_Node_removeChild
- Shadow_DOM_Tests

### Depends on

- The Safely Composable DOM

### Used by

- A Formalization of Safely Composable Web Components

### Auto-related entries

- A Formal Model of the Document Object Model with Shadow Roots
- Executable Randomized Algorithms
- A Formal Model of the Document Object Model

## Cite

×

Shadow_SC_DOM-AFP

    @article{Shadow_SC_DOM-AFP,
      author  = {Achim D. Brucker and Michael Herzberg},
      title   = {A Formal Model of the Safely Composable Document Object Model with Shadow Roots},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2020},
      note    = {\url{https://isa-afp.org/entries/Shadow_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