Web编程中的核心DOM形式语义

跟踪：Web编程WWW 2018，2018年4月23日至27日，法国里昂741Isabelle/HOL中核心DOM的形式语义摘要阿希姆·D英国谢菲尔德大学计算机科学系a. sheffield.ac.uk英国谢菲尔德大学计算机科学系msherzberg1@sheffield.ac.uk模型（DOM）定义了一个树状数据结构，用于表示文档对象模型（DOM）的核心是定义一个树状数据结构，用于表示一般的文档，特别是HTML文档。它是任何现代Web浏览器的核心。形式化DOM的关键概念是 客户端JavaScript程序的形式化推理分析现代Web浏览器中的安全概念我们提出了一个正式的核心DOM，重点是节点树和节点树上定义的操作，在伊莎贝尔/HOL。我们使用的形式化来验证DOM标准中定义的最重要的功能的功能正确性。此外，我们的形式化是（1）可扩展的，即，可以被扩展而不需要重新证明已经证明的性质和（2）可执行的，即，我们可以从我们的规范生成可执行代码。CCS概念• 信息系统→标记语言;文档结构;·软件及其工程→软件验证;语义学;形式化软件验证;关键词文档对象模型; DOM;形式语义; Isabelle/HOLACM参考格式：阿希姆·D Brucker和Michael Herzberg。2018. Isabelle/HOL中核心DOM的形式语义在WWW'18同伴：The 2018 Web Conference Companion，2018年4月23日至27日，法国里昂。ACM，New York，NY，USA，9页。https://doi.org/10.1145/3184558.31859801引言在一个越来越多的应用程序作为互联网上的服务提供的世界中，Web浏览器开始在我们的日常IT基础设施中扮演类似于操作系统的核心角色。因此，Web浏览器应该像操作系统一样严格和正式地开发。虽然形式化方法是操作系统开发中的一种成熟技术（参见E。例如，在一个实施例中，克莱恩[15]作为概述），很少有使用正式方法改进Web浏览器开发的建议[2，9，12，17]。作为验证的客户端Web应用程序堆栈的第一步，我们的模型和正式验证的文档对象模型（DOM）在伊莎贝尔/HOL。DOM [21，23]是所有现代Web浏览器的中心数据结构在其核心，文档对象本文在知识共享署名4.0国际（CC BY 4.0）许可下发布作者保留在其个人和公司网站上以适当的归属方式传播作品的权利。WWW©2018 IW3C2（国际万维网会议委员会），在知识共享CC BY 4.0许可下发布。ACM ISBN 978-1-4503-5640-4/18/04。https://doi.org/10.1145/3184558.3185980文档，特别是HTML文档因此，DOM实现的正确性对于确保web浏览器正确地显示网页是至关重要的此外，DOM是客户端JavaScript程序底层的核心数据结构，即。例如，客户端JavaScript程序主要是读取、写入和更新DOM的程序。更详细地说，我们将核心DOM形式化为Isabelle/HOL中的浅嵌入[14]我们的形式化是基于一个类型化的数据模型的节点树，即。例如，用于以树结构表示类似XML的文档的数据结构。此外，我们形式化的类型堆存储（部分）节点树连同必要的一致性约束。最后，我们对允许操作节点树的堆进行形式化操作（如DOM标准[ 23 ]中所述）。我们的DOM节点树的机器检查形式化[23]具有以下理想属性：(1) 它提供了一致性保证。 由于我们的形式语义中的所有定义是保守的，所有的规则都是派生的，DOM节点树的逻辑一致性降低到HOL的一致性。(2) 它是证明系统的技术基础。基于导出的规则和节点树上的证明策略的具体设置，我们的形式化提供了一个通用的证明环境，用于验证程序操纵节点树。(3) 它是可执行的，这允许通过评估正式模型上的符合性测试套件来验证其对标准的符合性。(4) 它在[5]的意义上是可扩展的，即。例如，在核心DOM上证明的属性不需要为面向对象的扩展（如HTML文档模型）重新证明最后，我们展示了正确的功能，用于操纵的DOM w.r. t。标准中的假设在第2节中介绍了Isabelle和高阶逻辑之后，我们在第2节中介绍了DOM的形式化数据模型和DOM上的操作。3.第三章。节中4，我们形式化的要求，一个有效的堆，其次是讨论的验证DOM操作的重要属性在节。五、最后，我们讨论了相关的工作（第6节），并得出结论（第6节）。（七）.2在本节中，我们将概述我们的DOM节点树的形式化的底层逻辑和方法框架。2.1高阶逻辑与IsabelleIsabelle [16]是一个用函数式编程语言SML实现的通用定理证明器。Isabelle/HOL是实例跟踪：Web编程WWW 2018，2018年4月23日至27日，法国里昂742⇒⇒⇒转→→一⇒⇒×个联系我们⇒⇒{1}|}⇒⇒I¢xory）=e·I¢x）e∨I¢y）eλ）Isabelle支持高阶逻辑（HOL）[1，8]。它支持对定义、数据类型、原始和良基递归的保守性检查，以及基于重写和tableau证明器的强大通用证明引擎。HOL是一个经典的逻辑与平等丰富的全多态高阶函数。HOL是强类型的，即，每个表达式e具有类型‘a’，写为e：：‘a’。在Isabelle中，我们用质数（e）表示类型变量。例如，在一个实施例中，“a）而不是希腊字母（e.例如，在一个实施例中，a）通常在教科书中使用函数空间的类型构造函数使用中缀表示法编写：'a 'b. HOL以扩展逻辑等式_=_为中心，类型为'a 'a bool，其中bool是基本逻辑类型。HOL中的函数是纯函数，即它们只接受一个参数，只返回一个结果，并且不会产生副作用。为了模拟具有多个参数的函数，我们让这些函数再次返回一个函数，直到它最终返回一个非函数。因此，在阅读curry函数定义时，以以下方式解释函数定义链可能会有所帮助：最后一个类型定义表示函数的当对有状态函数建模时，例如在我们的例子中，我们通常定义接受表示状态的参数并返回更新版本的函数（即，包含附加条目的映射）表示状态改变。类型学科排除了诸如罗素的悖论只通过一个特定的公理模式;这个模式公理保持一致性的（元级）证明可以在[10]中找到。2.2浅嵌入与我们现在关心的问题是一种语言如何在逻辑中表示。区分两种手法：一是深嵌入将抽象语法表示为数据类型，并定义从语法到语义的语义函数I第二，浅嵌入直接定义语义;每个构造由语义域上的一些函数表示。假设我们想要嵌入一个简单的逻辑语言BOOL，由两个逻辑运算符_and_and_or_组成，到HOL中。语义I：exprenvbool是一个将BOOL表达式和环境映射到bool的函数，其中environments env=var bool将变量映射到bool值。使用浅嵌入，我们直接定义：x和y≡λe·x e∧y e x或y≡λe·x e∨y e浅嵌入允许在语义域和对它们的操作方面的直接定义在深度嵌入中，我们必须将BOOL的语法定义为递归数据类型：expr = varvar|expr和expr|expr或expr以及显式语义函数I：无类型集合论中的dox。类型的集合可以定义为iso-形化为a⇒bool型函数;关系元素varx=λ e·e（x）__具有类型‘a’，设置为bool并且基本上对应于函数应用;集合理解{_。（通常写 _ _ 在教科书中）具有类型'a set（' a bool）'a set并且对应于λ-抽象。Isabelle/HOL允许定义抽象数据类型。例如，以下语句引入了选项类型：datatype 'a option = None|“某个”除了构造函数None和Some之外，还有NoneF的匹配操作情况x |差不多吧。选项类型允许我们将部分函数（通常称为映射）表示为类型为'a'b选项的全函数。对于这种类型，我们引入简写'a'b。我们定义dom f，称为部分函数f的域，由f的所有参数的集合不产生None。我们还使用求和类型'a + 'b和乘积类型'a'b。使用sum类型，可以表示元组，例如，可用于实现与返回类似的结果一个函数的元组。product类型表示'a或'b，并且对于建模错误很有用，因为它允许函数返回成功计算的结果或返回错误。当扩展逻辑时，可以区分两种方法：一方面是公理化方法，另一方面是保守扩展。通过公理扩展HOL核心，即，引入新的，未经证明的定律似乎是更容易的方法，但它通常容易导致不一致; 2考虑到在任何主要的理论证明系统中，核心理论和库包含数千个定理和引理，公理化方法在实践中是相反，保守扩展引入了新的常量（通过常量定义）和类型（类型定义）I¢x and y）=λ e·I（x）e ∧ I（y）e这个例子揭示了深度嵌入的主要缺点：该语言与底层Meta语言HOL更远，即语义功能表示演绎的障碍。然而，对于分析某些元理论分析，深度嵌入具有优势。由于我们对DOM的简洁语义描述和有效的证明支持感兴趣（我们对元理论证明不感兴趣），因此我们选择了浅嵌入。3形成DOM在本节中，我们将展示我们遵循WHATWG规范[23]的核心DOM的形式化，这是W3C DOM 4标准的更新版本[21]。这包括用于表示文档的树状数据结构的定义以及用于创建和修改文档的一组函数。3.1DOM的核心数据模型：节点树DOM的主要目的是提供用于管理树结构文档的数据结构，例如：例如，在一个实施例中，遵循HTML或XML标准。图1示出了一个小示例：图1a示出了简单文档的文本表示（使用HTML作为语法），图1b示出了DOM节点树的可视化，图1c示出了渲染输出（e.例如，在一个实施例中，在web浏览器中）。由于DOM建模的是一种树状数据结构，因此DOM规范的核心数据类型是Document和Node，并具有两个专门化元素和字符数据，这并不奇怪。在我们的数据模型中，我们省略了可以从其他属性计算的属性，例如，表示跟踪：Web编程WWW 2018，2018年4月23日至27日，法国里昂743(a) HTML文档类型：htmlHTMLclass=eHEAD标题文字：外星人？身体正文：为什么是。(b) Dom为什么是的。(c) 渲染其次，我们使用Isabelle中提供的记录包定义表示对象的HOL类型。总的来说，我们使用相同的构造类型多项式来表示继承HOL。由于空间的原因，我们省略了类型构造的技术细节。我们建议感兴趣的读者参考Isabelle形式化[4]。对于每个类，我们定义一个记录：记录对象= nothing：：unit记录节点= Object +nothing：：unitrecord_ Element =节点+tag_name：：tag_type图1：DOM的简单示例：（a）示出了使用HTML语法的文本表示，（b）DOM的节点树的可视化，以及（c）示出了渲染该DOM的结果，例如，通过web浏览器的呈现引擎已经由childNodes表示的逆关系，以及documentElement属性虽然以可扩展的方式形式化面向对象数据模型的核心思想1遵循[3，5]中提出的构造，但我们在诸如类型化指针（引用）和方法调用的后期绑定。由于篇幅所限，本文不作讨论。首 先 ， 我 们 为 公 共 超 类 Object 和 类 Node 、 Element 、CharacterData和Document的类型化指针定义抽象数据类型：数据类型'object_ptr object_ptr = Ext'object_ptr'node_ptr node_ptr = Ext'node_ptr'element_ptr element_ptr = Ref ref| Ext'element_ptr'character_data_ptr character_data_ptr = Ref ref| Ext 'document_ptr| Ext'document_ptr指向抽象类object_ptr和node_ptr的指针只支持用于扩展的构造函数;常规类也有一个用于引用对象本身的构造函数 我们使用这些数据类型来引入表示DOM模型的实际指针类型的类型同义词（参见图10）。2）的情况。child_nodes：：“_ node_ptr Core_DOMlist”attributes：：attributes_typerecordCharacterData = Node +data：：DOMStringrecord_ Document = Object +doctype：：doctypedocument_element：：“_ element_ptr Core_DOMoption”disconnected_nodes：：“_ node_ptr Core_DOM列表”由于记录包的技术限制，我们需要为那些本身没有定义至少一个属性的类引入一个nothing属性根据这些定义，我们可以定义CharacterData对象如下：定义“CharacterDataExample =（|Object.nothing =（），Node.nothing =（），data = ''Why yes.“的一声|）”本质上，这是一个树形数据结构的面向对象数据模型，在DOM标准中称为节点树，其中(1)树的根是Document的实例，（2）Document的类Element可以是内部节点或叶，以及（3）类CharacterData的实例只能显示为叶。最后，我们定义一个堆来存储节点树，即，DOM数据模型的实例DOM堆是从对象指针到对象的映射：类型_同义词_堆Core_DOM=“_ object_ptrCore_DOM_ ObjectCore_DOM“在面向对象模型Where_Object 核心_DOM 是实例化的是其超类的HOL类型的实例。这是允许可扩展形式化的关键构造。有关详细信息，请参阅[5]。在本文的其余部分，我们将使用下划线来表示指针的类型构造函数的类型变量的元组和对象类型。例如，我们将写入_node_ptrCore_DOM而不是（'node_ptr，'element_ptr，'character_data_ptr）node_ptrCore_DOM并假设相同名称的类型变量用相同的类型实例化。1这种面向对象形式的可扩展性允许我们，例如，以后将DOM模型扩展为基于DOM标准的标准的正式模型，例如HTML，而不需要在DOM上重新证明属性对象的超类型（类似于指针的构造图3说明了如何在我们的正式DOM堆中表示图13.2节点树上的操作和查询在下文中，我们将定义用于创建、查询和修改存储在DOM堆中的节点树的核心DOM方法我们在Isabelle/HOL中正式定义了以下函数。图4提供了它们的正式类型签名的概述。所有操作都是在DOM堆上定义的，即，它们以堆作为输入，并返回一个异常或一个包含返回值和新堆的元组type_synonym（_，'result）dom_prog =“_dom_heapCore_DOM⇒exception +（'result ×_dom_heapCore_DOM）”<！文档类型html><标题>外星人？/title><联系我们<身体>为什么是的。产品介绍<联系我们跟踪：Web编程WWW 2018，2018年4月23日至27日，法国里昂744test_heap = map_of [(cast（document_ptr.Ref 1），cast（|Object.nothing =（），doctype = ''html''，document_element = Some（element_ptr.Ref 1），disconnected_nodes=[]|））的情况下，(cast10），int（|Object.nothing =（），Node.nothing =（），tag_name = ''html ''，child_nodes = [cast（element_ptr.Ref 2），cast（element_ptr.Ref4）]，(cast10），int（|Object.nothing =（），Node.nothing =（），attributes = map_of [（''class''，''e ''）]，shadow_root_opt=None|））的情况下，]”tag_name = ''head ''，child_nodes = [cast（element_ptr.Ref 3）]，attributes =空，shadow_root_opt =无|））的情况下，(cast 10））}）}））|Object.nothing =（），Node.nothing =（），tag_name = ''title ''，child_nodes=[cast（character_data_ptr.Ref 1）]，attributes = empty，shadow_root_opt = None|））的情况下，(cast（character_data_ptr.Ref 1），cast（|Object.nothing =（），Node.nothing =（），data =''Aliens？“的一声|），（cast（element_ptr.Ref 4），cast（|Object.nothing =（），Node.nothing =（），tag_name=''body ''，child_nodes = [cast（character_data_ptr.Ref 2）]，attributes = empty，shadow_root_opt =None|）），（cast（character_data_ptr.Ref 2），cast（|Object.nothing =（），Node.nothing =（），data类型同义词Copyright © 2018 - 2019 www.jsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsjsj© 2018 - 2019 www.jszy.com版权所有并保留所有权利+ 'document_ptr document_ptr + 'shadow_root_ptr shadow_root_ptr + 'object_ptr）object_ptr”（'node_ptr，'element_ptr，'character_data_ptr）node_ptrCore_DOM=“（'element_ptr element_ptr + 'character_data_ptr character_data_ptr + 'node_ptr）node_ptr”'element_ptr element_ptrCore_DOM =“' element_ptr element_ptr”图2：核心DOM的可扩展类型化指针的HOL类型。类型多项式确保面向对象数据模型中的子类的指针是它们的超类的指针的HOL类型的实例图3：包含我们的简单示例DOM的堆的形式表示（回想图12）。①的人。如果参数无效，则所有操作都会导致异常e. 例如，在一个实施例中，不表示当前堆中有效对象的指针我们使用堆和错误单子来建模异常。这允许我们定义类似于Haskell中有状态编程的复合方法，但也接近官方规范。函数create_element接受一个（所有者）文档和新元素的标记名它返回更新后的堆，其中包括没有子元素和属性的新元素以及对新元素的引用，该引用存储在堆中的第一个空闲位置这确保了它不会改变堆中的任何现有位置，我们将在后面证明这另外，新元素被添加到给定的文档，因为它还不是节点树的一部分函数get_child_nodes接受一个堆和一个指向节点的指针，并返回指向其子节点的指针列表对于元素，它返回存储在数据类型中的子列表。对于文本节点，它返回空列表。对于文档，我们将其文档元素转换为适当的节点列表。函数get_attribute在元素的属性映射中查找给定的属性。如果存在具有给定键的属性，则返回Some attr，否则返回None。官方规范也有一个称为“reflected content attribute”的概念函数set_attribute更新堆中指针的给定属性。在官方规范中，不允许将属性分别设置为None或null以删除属性。我们通过允许这个来推广这个定义。函数get_parent_node接受一个指向节点的指针，并返回一个指向其父节点的指针，如果节点没有父节点，则返回None节点没有父节点的情况只会发生在断开连接的节点树中，我们将在后面讨论我们的API不接受文档，因为它们永远不会有父级。使类型尽可能窄将使证明更容易 函数get_parent_node是一个方法的例子，其中官方规范在实现方面留下了很大的解释空间。它既没有提供一个算法来解释如何在给定一个节点的情况下获得一个父节点，也没有指定父节点引用应该存储在对象中为了避免指定额外的一致性约束，如果子引用和父引用都要存储，我们通过搜索整个堆来实现get_parent_node，以查找其get_child_nodes包含给定引用的任何节点函数remove_child非常接近官方规范;如果child的parent与 传 递 的 parent 不 同 ， 那 么 我 们 “ 抛 出 ” 一 个NotFoundError。否则，我们将移除的子节点添加到其所有者文档的断开连接节点列表中，并将其从document_element或child_nodes属性。跟踪：Web编程WWW 2018，2018年4月23日至27日，法国里昂745create_element：：“tag_type⇒_ document_ptrCore_DOM⇒_dom_prog”get_attribute：：“_ element_ptrCore_DOM⇒ attributes_key⇒_dom_prog”set_attribute：：“_ element_ptr核心DOM⇒属性键⇒属性值选项⇒_dom_prog”get_child_nodes：：“_object_ptrCore_DOM⇒_dom_prog”get_parentremove_child：：“_ object_ptrCore_DOM⇒_ node_ptrCore_DOM⇒_dom_prog”：：“_node_ptrCore_DOM⇒_dom_prog”get_element_by_id：：“_object_ptrCore_DOM⇒ attributes_value⇒_dom_prog”采用节点insert_before：：“_ object_ptrCore_DOM⇒_ node_ptrCore_DOM⇒_ node_ptrCore_DOMoption ⇒_dom_prog”：：“_ document_ptrCore_DOM⇒_ node_ptrCore_DOM⇒_dom_prog”图4：用于创建、查询和修改核心DOM的方法的正式类型签名函数get_element_by_id以树的顺序（深度优先，从左到右）搜索具有给定id的第一个元素。我们的定义比官方规范更通用，因为我们放弃了get_element_by_id只在文档上可用的要求，这是一个遗留要求。3.2.1采用节点。 方法adopt_node从它以前的父节点中删除一个节点（如果有），并将其分配给新的ownerDocument。首先，它尝试检索要采用的节点的父如果节点有父节点，则从子节点列表中删除该节点最后，该节点现在被添加到新文档的断开连接的节点中。定义adopt_node：：“_ document_ptrCore_DOM⇒_node_ptrCore_DOM⇒_dom_prog”哪里“adopt_node文档节点=do{ parent_opt ←get_parent节点;（case parent_optof一些父节点⇒remove_child父节点| None ⇒ do {old_document ←get_owner_document（cast节点）;remove_from_disconnected_nodes old_document}）;add_to_disconnected_nodes文档节点}”3.2.2插入节点。使用insert_before，可以插入任意节点（即，不一定在相同的节点树中）从堆到节点树：定义insert_before：：“_ object_ptr核心DOM⇒_node_ptr核心DOM⇒_ node_ptrCore_DOM选项 ⇒_dom_prog”哪里“insert_before ptr node child = do{ ensure_pre_insertion_validity nodeptrchild; reference_child ←（if Some node =child然后next_sibling节点return child）;owner_document ←get_owner_document ptr;adopt_node owner_document节点;insert_node ptr node reference_child}”文件元件元件元件元件元件CharacterDataCharacterData元件CharacterData图5：带有可见文档（灰色）和运行时树（白色）的一个节点应该是插入需要到履行cer-确定格式良好性标准。这是使用ensure_preinsertion_validity函数来检查的，该函数从DOM标准中形式化了预插入有效性然后，需要确定参考子节点，该参考子节点是要被插入的节点应该被放置在其之前的节点。然后，我们将该节点引入（可能是新的）节点树中，并实际将该节点插入到child_nodes或document_element属性中。4DOM堆的良好格式我们的DOM堆是一个从对象指针到对象的映射。虽然单独的映射将允许许多此外，我们的数据模型省略了标准的一些字段，例如parentNode，我们使用堆和get_child_nodes来计算。尽管如此，仍然存在一些可能的非法堆配置，例如具有循环get_child_nodes关系的堆配置因此，我们需要进一步的良构性约束，我们需要证明DOM方法保持良构性。现在我们将介绍验证给定堆是否符合标准的谓词4.1所有者文件DOM规范要求每个节点只由一个文档（即其所有者文档）拥有。此外，每个节点参与树w.r.t. get_child_nodes-关系。DOM可能并且通常将由几个树组成，即，DOM是一个树的森林。我们将以主文档为根的树称为可见文档，因为这是要呈现的DOM的一部分。例如，在一个实施例中，通过网络浏览器。跟踪：Web编程WWW 2018，2018年4月23日至27日，法国里昂746∀图 5 示 出 了 示 例 的 这 种 关 系 ： 灰 色 节 点 （ 由 使get_child_nodes-关系可视化的实线箭头连接）表示可见文档 。 白 色 节 点 （ 由 虚 线 箭 头 连 接 ， 可 视 化get_owner_document关系）形成临时运行时树。运行时树不是序列化的（e.例如，在一个实施例中，在HTML或XML文档中）且仅存在于运行时。我们定义一个节点的get_owner_document作为根，如果根是一个文档;否则，我们返回其disconnected_nodes包含该节点的文档。为了使这个定义格式良好，我们需要以下谓词：定义owner_document_valid：：“_ heap Core_DOM ⇒ bool”其中“owner_document_valid h =（{node_ptr. doc_ptrdisc_node_ptrs.（h get_disconnected_nodes doc_ptr→r disc_node_ptrs）−→node_ptr∈setdisc_node_ptrs}= {node_ptr. ∀ptr.（h get_root_node（cast node_ptr）→rptr）−→¬is_document_ptr_kindptr}）”这个谓词向我们保证所有disconnected_nodes字段中的节点集就是没有文档作为根的节点集。4.2将DOM限制为树到目前为止，我们没有限制get_child_nodes给出的关系是非循环的，这是可能的，因为我们使用指针。为了防止这种情况，我们可以使用以下谓词：定义acyclic_heap：：“_ heap Core_DOM ⇒ bool”其中“acyclic_heap”h = acyclic {（parent，child）.孩子。（hget_child_nodes parent →r children）−→child ∈cast我们利用关系上的非周期性定义，即，一组元组。我们的关系包含所有指针parent和child，其中child在parent的子集合中。4.3节点共享DOM标准假定一个节点不能是多个节点的子节点堆的这个属性被官方标准非正式地暗示了，所有修改树的方法都确保不能构建这样的DOM但是，我们必须处理所有符合堆类型的堆因此，除了保证堆中的所有树都是非循环的堆谓词之外，我们还需要一个谓词来防止节点有多个父节点。因此，我们正式定义了另一个堆谓词：4.4指针有效性此外，我们需要确保对象不包含无效的指针（例如：例如，在一个实施例中，不指向存储在相同类型的堆中的对象的指针）。否则，每当我们使用指针时，我们将不得不处理“空指针异常”的可能性因此，我们要求：定义all_ptrs_in_heap：：“_ heap Core_DOM ⇒ bool”其中“all_ptrs_in_heap h =（（））（hget_child_nodes ptr → r children）−→set children node_ptr_kindsh）∧（doc_ptrdisc_node_ptrs.（h get_disconnected_nodes doc_ptr→r disc_node_ptrs）−→set disc_node_ptrsnode_ptr_kindsh））”我们唯一可以找到指针的地方（没有仲裁器-（这是应该避免的）是在其中一个数据类型字段中。因此，对于堆中的所有指针，我们重新检索相应的对象，并检查存储在适用字段（childNodes、document_element和disconnected_nodes）中的所有指针是否存在于堆中。4.5堆是强类型的当我们为类型化指针和对象建模时，我们希望确保某个类型的指针实际上映射到给定堆中相关类型的对象，例如：例如，在一个实施例中，document_ptr实际上映射到文档。下面的谓词向我们保证这对整个堆都成立：definitionmatches_heapCore_DOM：：“_ heapCore_DOM⇒ bool”其中“matches_heapCore_DOM =（doc_ptr∈document_ptr_kinds堆。the（get（cast doc_ptr）is_document_kind heap）∧.. .与document类似，该定义还包含对其他类的检查定义检查是 否 对 于 所 有 ， 例 如 ， 文 档 指 针 ， 堆 实 际 上 返 回is_document_kind持有的对象。4.6无多边childNodes和disconnected_nodes属性的类型为list。因此，它们可以包含重复，即，相同的指针多次。这可能会导致奇怪的效果，例如在调用remove_child之后，指针仍然在列表中。官方规范没有解决此行为我们明确了这一要求：定义distinct_lists：：“_ heap Core_DOM ⇒ bool”其中，“distinct_lists h =（（））”表示子项。定义maximum_one_parent：：“_堆核心_DOM ⇒bool”（h get_child_nodes ptr→rchildren）−→不同的子项）其中“maximum_one_parent h =（node_ptr.（length（sorted_list_of_set {parent.孩子。（hget_child_nodes parent →r children）−→node_ptr∈setchildren}））≤1）”该定义检查对于任何节点，可能的父节点的集合（即，其子节点包含所述节点的指针）恰好包含零个或一个父节点。∧（doc_ptrdisc_node_ptrs.（h get_disconnected_nodes doc_ptr→r disc_node_ptrs）- →distinct disc_node_ptrs））”我们检索堆中每个指针的列表，并要求它们是不同的。在5.2节中，我们将给出一个正式的证明，证明insert_node实际上永远不会导致一个有重复项的childNodes跟踪：Web编程WWW 2018，2018年4月23日至27日，法国里昂747表1：核堆方法的良构性性质无副作用仅修改保持格式良好获取子节点✓获取父节点✓get_element_by_id✓get属性✓创建元素✓✓集合属性✓✓删除子项✓✓采用节点✓✓插入之前✓✓4.7格式良好的堆为了把所有这些放在一起，我们定义一个良构堆作为满足所有讨论的约束的堆：5.1.2堆修改是本地的。我们希望确保堆修改函数不会任意修改堆。因此，我们首先引入两个谓词，它们通过指定分别读取或写入哪些位置（指针）和字段来定义读取：：“（_object_ptrCore_DOM×（_ object_ptrCore_DOM ⇒_heapCore_DOM⇒_ heapCore_DOM ⇒bool））set⇒_ dom_prog ⇒bool”其中“读取S f←→（h h’x.（h f→rx）−→（（ptr，P）∈S. P ptr h h'）−→（h'f→rx））”定义写入：：“（_object_ptrCore_DOM×（_ object_ptrCore_DOM ⇒_heapCore_DOM⇒_ heapCore_DOM ⇒bool））set⇒_ dom_prog ⇒bool”其中“写为S f←→（h h’。（h f→hh'）定义heap_is_wellformed：：“_堆heap_is_wellformed h←→核心_DOM ⇒bool”−→（ptr.get∈Sg. （ptr，get）gS −→getptr h h'））”这两个谓词都采用一组断言的指针和谓词finite（object_ptr_kinds h）∧matches_heapCore_DOMh∧owner_document_valid h∧acyclic_heap h∧all_ptrs_in_heap h∧maximal_one_parent h∧ distinct_lists h”5在DOM上推理到目前为止，我们只定义了DOM数据结构、用于存储DOM实例的堆以及它们的方法我们现在讨论这些方法的验证，从形式上证明它们保持了堆的良构性。5.1DOM方法5.1.1堆方法的良构性 DOM方法（见3.2节和表1）可以分为两类：所有查询函数（以前缀get_开始）都使用堆来计算值，但不修改堆。因此，很容易证明它们保持了堆的良构性。对于所有其他函数，我们必须正式证明它们的正确性w.r.t.保持堆的良好形成如果所有方法都保持格式良好，那么我们已经证明了任何无异常的DOM方法序列都会创建一个格式良好的DOM堆。对于所有方法，我们需要证明以下形式的引理：引理insert_before_preserves_wellformedness：假设“heap_is_wellformed h”和“h