|
A
Formal
Model
of
the
Document
Object
Model
with
Shadow
Roots
Title: |
A Formal Model of the Document Object Model with Shadow Roots |
Authors:
|
Achim D. Brucker and
Michael Herzberg
|
Submission date: |
2020-09-28 |
Abstract: |
In this AFP entry, we extend our formalization of the core DOM with
Shadow Roots. 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. |
BibTeX: |
@article{Shadow_DOM-AFP,
author = {Achim D. Brucker and Michael Herzberg},
title = {A Formal Model of the Document Object Model with Shadow Roots},
journal = {Archive of Formal Proofs},
month = sep,
year = 2020,
note = {\url{https://isa-afp.org/entries/Shadow_DOM.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Core_DOM |
Used by: |
DOM_Components |
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.
|
|