The traditional core of DOM (Document Object Model) and its formal representation in fDOM

DOI: 10.31673/2412-9070.2023.062327

Abstract

This article discusses the differences between two models of web documents: the traditional DOM (Document Object Model) and fDOM (formal DOM). The discussion begins with a description of Core DOM, which represents the structure of web documents as a hierarchical tree of nodes. Each node represents elements, attributes, and textual content, allowing for navigation, modification, and deletion of document components. The visual structure of DOM is illustrated using HTML code. The use of Isabelle/HOL, a higher-order logic system, for working with fDOM is then considered. This allows for the formalization of the mathematical properties of fDOM, ensuring their correctness and resistance to vulnerabilities. An example of code in Isabelle/HOL demonstrates how operations on web document elements can be defined and verified. The article also compares DOM and fDOM, highlighting differences in their approaches to representation and interaction with web documents. It is emphasized that while the traditional DOM provides a flexible interface for web documents, fDOM offers a more rigorous, mathematical representation, focused on precision and strictness. The discussion concludes with the advantages and disadvantages of fDOM. Among the advantages are formal verification, strong typing, consistent behavior, clear definitions, and enhanced security. However, increased complexity and development time, less flexibility, higher resource costs, and a steep learning curve are noted as disadvantages of fDOM. The conclusion emphasizes that fDOM offers a reliable, verified foundation for web applications but also introduces additional development requirements, making it particularly useful for applications where correctness and security are important.

Keywords: fDOM; Isabelle/HOL; web components; information systems; web technologies; scaling of web applications; optimization.