独立证书框架的开发及其在自动化推理中的应用

可在www.sciencedirect.com在线获取理论计算机科学电子笔记312（2015）51-67www.elsevier.com/locate/entcs开发独立证书的框架1ChristianSternagel和Ren'eThiemann计算机科学学院，因斯布鲁克大学6020因斯布鲁克，奥地利摘要当前用于自动化推理的工具通常功能强大且复杂。 由于它们的复杂性，它们存在包含错误并因此提供错误结果的风险。为了确保这些工具的可靠性，一种可能性是开发证书，在可信的证明助手的帮助下检查工具的结果。我们提出一个框架，说明了开发独立认证器的基本步骤，这些认证器可以有效地检查所使用的证明助手之外生成的证明。我们的框架已被用于开发各种物业的证书，包括终止、持续、完成和树自动机相关的物业。保留字：认证，Isabelle/HOL，证明助理1引言由于其增加的功率，自动证明器，如SAT求解器、SMT求解器、自动一阶定理证明器、模型检查器、终止证明器等，越来越多的软件验证。然而，这些证明器的复杂性非终止程序的终止声明）。因此，每当证明器的复杂性增加时，生成的答案的可靠性通常会降低因此，验证答案对于可靠性至关重要。为此，证明者不仅要提供像SAT或UNSAT这样的二元答案，而且还必须以证书的形式提供证明，这通常取决于证明者的领域它可能是一个满意的分配或SAT求解器的自然演绎证明，一个有根据的测量或终止证明器的循环序列等。验证证书-可用于恢复功能强大但复杂的自动检定仪所需的可靠性程度1由FWF（奥地利科学基金）项目J3202和P22767资助。http://dx.doi.org/10.1016/j.entcs.2015.04.0041571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。52C. 斯特纳格尔河Thiemann/Electronic Notes in Theoretical Computer Science 312（2015）51在本文中，我们提出了一个具体的框架，方便地开发高度可靠，高效，易于使用的证书。为此，在§2中，我们首先讨论了如何执行认证的各种替代方案然后，我们的框架介绍了一我们将在第3节讨论错误处理，在第4节讨论错误生成，在第五节，证明第六节中最终证明人的可靠性。我们在§7中得出结论。我们通过一个运行的例子来说明我们的框架由于这个例子只提出了一个非常简单的认证任务，我们很快就想提一下，这个框架已经成功地应用于更复杂的认证任务，其中认证器本身由超过35，000行Haskell代码组成在下文中，所有内容都是针对证明助手Isabelle/HOL [17]进行说明的，但大多数部分应该可以很容易地适应类似的证明助手，如Coq [2]或PVS [18]，只要它们支持代码生成机制。通过代码生成，我们意味着从所使用的证明助手的逻辑中定义的函数到实际程序代码的自动和可信的翻译。例如，Isabelle的代码生成器支持标准ML和Haskell（以及其他）作为目标语言。我们参考Haftmann和Nipkow [12]的工作以了解更多细节。框架的所有组件都可以在形式证明档案中找到[21，23，24]，运行示例的源代码可以在http://cl-informatik.uibk.ac.at/software/ceta/framework。一些这项工作的一部分已经在前面介绍过了[26]，但其完整性和详细性要差得多。我们的方法旨在简化用于验证算法的已验证检查器的构造[4]。在运行的示例中，这是针对Post的对应问题进行演示的2认证证书自动生成的证明（断言某些输入具有某些属性）的认证可以通过几种方式执行，下面将简要讨论作为一个运行的例子，我们考虑Post给定一个字母表，PCP实例p是一个在上的词对的集合 是可解i =存在非空列表[（x1，y1），.，（xn，yn）]的词对，使得每个（xi，yi）∈p和x1. x n= y1. y n.众所周知，PCP实例的可解性一般是不可判定的。我们希望验证可解决的PCP实例的证书。这是一个简单的认证任务，但可以用来说明开发认证程序过程中的各种设计选择和挑战。我们假设证明对p中的每对词进行编号，并将解决方案作为一个数字列表提供C. 斯特纳格尔河Thiemann/Electronic Notes in Theoretical Computer Science 312（2015）51532.1人工检查显然，人类可以检查证书，只要证书以 人类可读的形式。例如，PCP实例p={ 0：（A，ABA），1：（AB，BB），2：（BAA，AA）}和解决方案0，2，1，2形式的证书在下表中呈现。0212的1B2A 3A 4A5B 6B7A 8A 9A1B 2A 3A4 A5B6B 7A8A 9从这个表中很容易看出p是可解的：只要检查列是否对应于p中的单词对。此外，下标1，. . .，9表示单词help中的位置，检查两行是否包含相同的单词：只需检查两行是否包含按升序排列的下标1到9，并且两行中的每个数字都与同一个字母相连然而，人工检查显然容易出错，因此不是最好的认证方法。例如，考虑PCP实例pJ={ 0：（AAB，A），1：（AB，ABB），2：（AB，BAB），3：（BA，AAB）}其中最短的解是1，3，2，3，3，1，0，1，3，2，3，2，3，3，2，3，3，1，0，3，3、1、0、2、3、0、0、2、3、3、1、0、1、0、0、0、2、3、2、3、0、1、0、3、3、1、0、3、0、0、2、3、0，0，2，0，0，2，0，1，0，3，0，0，2.手工检查这个解决方案至少是乏味的。当我们从PCP转移到更复杂的证书时-其验证需要精心计算-人工检查不再可行。2.2通过程序代替人工检查，我们可以编写一个程序来检查证书中提到的所有证明步骤。这通常不是太复杂-与编写必须产生证明的程序相比-并且在简单的证书（如可解决的PCP实例的证书）的情况下，也可能是获得证书的好选择。然而，这种方法也有一些严重的缺点：例如，如果检查证书需要一些复杂的决策过程，那么实现该决策过程的程序本身就很复杂，并且可能存在错误。因此，证书的可靠性随着其复杂性而降低。另一个问题是依赖于潜在的令人敬畏的纸张证明和不一致的假设：例如，在论文中陈述（并在工具中实现）的定理可能是错误的;当将不同论文中的方法结合在一起时，可能会发生这种情况，即方法做出略微不同但不相容的假设，而这种不相容性可能仍然未被发现。比如说，[6]包含了一些不一致的假设，这些假设只在[25，§5]中被发现。在开发证书的过程中-在这种情况下，所有问题都可以修复，54C. 斯特纳格尔河Thiemann/Electronic Notes in Theoretical Computer Science 312（2015）51⇒∧⊆∧←→ ∃datatypeletter = A|Btype-synonymousword=letter listtype-synonympcp-problem=（word×word）set定义solvable：：pcp-problem bool哪里可解PCP（配对列表集合对列表PCPpair-list=[]concat（map fst pair-list）=concat（map snd pair-list））定义p′：：pcp-问题哪里p′=（[A， A， B]，[A]），（[A， B]，[A， B， B]），（[A， B]，[B， A， B]），（[B， A]，[A， A， B]）}Fig. 1. 输入和可解性但情况并非总是如此。这种方法的一个例子是算法库LEDA（由Alkassar等人扩展到使用验证的检查器）[1]）。2.3通过证明助理进行为了提高可靠性，我们可以使用LCF风格[10，11，19]证明助手，即，证明助手，其可靠性依赖于一个小的可信内核，定义包允许我们编写更高级别的证明，然后将其分解为内核原语，而无需添加新的公理。当使用证明助手时，首先必须对兴趣属性进行建模。该模型是否与人们感兴趣的房地产相对应，必须由人类仔细检查然而，之后可以将证书转换为证明脚本，然后可以由证明助理进行检查，从而产生所需的高度可靠性。例如，考虑以下Isabelle/HOL [17] PCP的形式化它从指定PCP实例及其可解性开始，并定义一个实例pJ（对应于§2.1中提到的示例pJ），参见。图1.在可解的定义中，条件集对列表（condition setpair-list）断言所有对列表中的所有元素都包含在PCP实例中，并且在相等性测试concat... = concat.. .映射FST对列表和映射SND对列表分别将词对列表投影到词对左侧和右侧的词列表中在指定之后，（pJ的）可解性可以通过图2中的脚本来证明。首先，定义了函数pair-of-index，它将索引映射到pJ的相应字对。然后，执行可解性的证明：首先，来自证明的解被用作存在性量化器的见证，然后调用Isabelle这种方法有几个优点，但也有一些缺点：+ 验证具有高度可靠性。+ 可以执行浅嵌入，即，证明助手的特征可用于对给定输入问题建模并用于建立证明。作为{C. 斯特纳格尔河Thiemann/Electronic Notes in Theoretical Computer Science 312（2015）5155⇒×funpair-of-index：：nat word word哪里索引对i=nth[([A， A， B]，[A]），（[A， B]，[A， B， B]），（[A， B]，[B， A， B]），（[B， A]，[A， A， B]）]ipcp-可解引理：可解p′apply（unfold solvable-def p′-def）应用（规则exI[of-（map pair-of-index[1， 3， 2， 3， 3， 1， 0， 1， 3， 2， 3， 2， 3， 3， 1， 0， 3， 3， 1， 0， 2， 3， 0， 0， 2， 3， 3， 1，0，1、 0、 0、 0、 2、 3、 2、 3、 0、 1、 0、 3、 3、 1、 0、 3、 0、 0、 2、 3、 0、 0、 2、 0、 0、 2、0、 1、 0、 3、 0、 0、 2]）]）应用简单做图二. 证明可解性因此，通常可以简洁和可读地指定模型，并且它还简化了证明的生成在PCP的情况下，作为浅嵌入的例子，我们为字母创建了一个特定于PCP实例pJ的数据类型。此外，我们使用Isabelle类似地，可以使用内置运算符或量化器，如λ、λ等，对输入问题进行建模;或者可以从证明助手调用一些强大的例程来履行证明义务，比如算术求解器等等。+ 如果感兴趣的属性与证明助手本身的证明义务相关，则认证允许将不受信任的自动化工具安全集成到证明助手中，以提高自动化程度例如，Isabelle [5]的Sledgehammer工具可以通过调用外部自动定理证明器来解决开放的证明目标，然后在metis的帮助下，在证明助手中重放生成的证明，metis是Isabelle内部的证明器，充当证明者。— 对于认证，需要安装并启动证明助手。此外，在证明助手中检查证明通常比在§2.2中执行程序要慢。— 如果一个证书不被接受，那么证明助手就会被困在一些中间的证明义务上，可能会有一些错误消息。为了理解证书被拒绝的原因，可能需要证明助理的一些知识。例如，为了理解被拒绝的PCP证书，可能需要理解Coq-、Isabelle-或PVS-脚本。— 校对助手中的更改仅在运行时检测到。例如，在一个示例中，如果Isabelle改变了简化器的配置，那么图2中的简化器调用可能不再成功。这 种 方 法 的 成 功 例 子 是 两 个 终 止 证 明 认 证 Coccinelle/CiME[7] 和CoLoR/Rainbow[3]。这里，Coccinelle和CoLoR是重写系统终止时的Coq库，即，它们定义了终止的概念，并包含一些终止准则的可靠性定理。CiME和Rainbow是将来自自动终止工具的证书转换为证明脚本的工具，然后基于以下定理应用适当的策略：56C. 斯特纳格尔河Thiemann/Electronic Notes in Theoretical Computer Science 312（2015）51⇒∧−⊆∧⊆⇒⇒联系我们←→ ∃⇒ ⇒×type-synonym'a word='a listtype-synonym′a pcp-problem=（′a word×′a word）set定义可解：：'一个pcp问题布尔哪里可解PCP（配对列表集合对列表PCPpair-list=[]concat（map fst pair-list）=concat（map snd pair-list））type-synonym′a pcp-problemI=（′a word×′a word）listfunpair-of-index：：′a pcp-problemI nat′a word′a word哪里索引对pcp i=第n个pcp itype-synonympcp-certificate=nat listfuncheck-solvable：：′a pcp-problemI pcp-certificate bool哪里检查可解PCP溶液=（let pair-list=map（pair-of-index pcp）solution inlist-all（λi. i<长度pcp）溶液溶液=[]concat（map fst pair-list）=concat（map snd pair-list））引理check-solvable：假设检查：检查可解决的pcp解决方案显示可解（设置pcp）证明让？pair-list = map（pair-of-index pcp）解决方案有concat（地图fst？pair-list）= concat（map snd？pair-list）使用简单检查而且有？pair-list = [] usingcheckby simp而且已经设置？pair-listset pcpusingcheckby（auto simp add：list-all-i）最终显示？论文展开可解定义 通过（Intro ExI [的-？pair-list]）自动QED可解输出码检查 在Haskell图3.第三章。首个获得PCP认证的生产商在图书馆里可以找到。2.4通过程序和证明助理进行认证最后，我们还提出了一种方法，它结合了§§2.2和2.3的优点。其基本思想是编写一个程序check-prop：：input验证证书，它可以像§2.2那样有效地检查证书，但完全是在一个证明助手中编写的。因此，我们可以在证明助手中开发所需属性P的模型，并结合check-prop的静态可靠性证明：check-prop input certificate=P input（1）因此，我们得到了§2.3的高可靠性。一旦建立，只需执行check-prop。这可以在校样助手中通过反射来完成。或者，人们可以调用证明助手的代码生成器来获得check-prop作为独立程序，然后每个人都可以方便地执行，甚至不必安装证明助手。作为一个例子，考虑图3，其中包含可解决的PCP实例的检查器，其中在最后一行中，完整的检查器通过Isabelle的代码生成器[ 12 ]作为Haskell代码利用所描述的方法，可以克服所有缺点，∧C. 斯特纳格尔河Thiemann/Electronic Notes in Theoretical Computer Science 312（2015）5157§在§2.3的末尾提到，代价是不能执行浅嵌入。因此，我们不能像在2.3中那样在字母表上创建合适的数据类型，而是使用具有类型变量的多态类型来创建字母表Ja（我们也可以选择字符串或数字等）。作为进一步的结果，check-prop中的所有例程都必须如此编程，即， 如果我们需要一个算术解算器，我们需要对其进行编程并证明它是正确的，并且不可能只调用算术解算器，而算术解算器可以通过证明助手中的某些策略来获得。在运行的示例中，让我们简要描述图2和图3之间的差异。后一种解决方案不能将具体的PCP实例编码为pair-of- index，而是必须将其作为参数传递。它还使用了一种新的类型来以可执行的形式表示PCP实例，即单词对列表而不是集合词对：pcp-problemI。此外，以前被简化器释放的条件现在在检查可解函数中是显式的，例如，通过list-all检查解决方案内的所有索引指向有效的字对。在本文的其余部分，我们将说明如何改进检查属性程序的这个基本版本。3错误处理目前，check-prop的类型是input_certificate_bool。也就是说，返回值只提供一位信息。对于被接受的证书，这是足够的，对于被拒绝的证书，我们通常对拒绝的原因感兴趣使用当前的方法（图3中的检查可解），在拒绝的情况下，我们甚至比§2.3中更糟糕（在§ 2.3中，我们需要解释来自证明助手的错误消息），因为现在我们只获得结果值：False。因此，我们的下一个目标是扩展check-prop，使其在拒绝时此外，这应该在没有太多开销的情况下完成，特别是它不应该混淆check-prop的可靠性证明。我们建议使用Isabelle和型表示的误差单子数据类型Ja + Jb = InlJa|印度卢比Jb其中误差用Inl表示，正确结果用Inr表示。布尔值现在被类型Je检查所取代，它是Je+unit的缩写。然后Inr（）对应于True，Inl e对应于False，并通过错误消息e来丰富。更一般的检查函数也可能在成功的情况下返回新的结果Inr x而不是plain（）例如，如果推理规则的前提条件不满足，则用于检查某个推理规则的函数可能会失败，否则将返回应用该规则所产生的新证明义务。在下文中，我们关注Je check，它取代了check-prop的布尔返回类型。我们提供了以下功能来简化从布尔值到错误单子的转换。• inspection：一个函数isOK，它测试给定的一元值是否是58C. 斯特纳格尔河Thiemann/Electronic Notes in Theoretical Computer Science 312（2015）51{/⇒⇒funcheck-solvable：：′a pcp problemI pcp-certificate string check哪里检查可解PCP溶液=DOcheck-all（λi. 1<长度PCP）溶液<+吗？ （λi. "index i invalid"）;let pair-list=map（pair-of-index pcp）solution;check（solution= []）′′solution must not beempty′′;check（concat（map fst pair-list）=concat（map snd pair-list））""结果单词不相等“”}<+？（λs.确保PCP的满足性的问题：引理check-solvable：假设check：isOK（检查可解决的pcp解决方案）显示可解（设置pcp）见图4。 带有错误消息的错误与否。因此，像（1）这样的可靠性证明现在被重新表述为isOK（check-prop input certificate）=验证输入（2）• 断言：为了断言基本属性，我们提供了函数check：：bool_INR_e_inr_e+unit，其中check_b_e=（if_b_then_Inr（）else_Inl_e），即，断言的属性与错误消息相耦合• 组合子：我们提供了几个组合子，如一元绑定（>=）：：je+ja（jaje+jb）je+jb（充当短路合取）和check-all：：（jabool）JA列表JA校验（其在成功的情况下表现得像在列表上的校验并返回给定谓词失败的第一个元素，否则）。此外，特别是对于一元绑定，我们扩展了Isabelle• 错 误 消 息 ： 有 一 些 操 作 符 可 以 改 变 错 误 消 息 ， 比 如 （ <+ ？ ）： ： Je +Ja<$（Je<$Jf）<$Jf + Ja，它采用一个函数，用于修改给定一元值的错误消息。因为修改只发生在错误，此操作在低于正常时没有影响。• 证明：我们对Isabelle进行了确认，在大多数情况下，简化器可以轻松消除一元开销和错误消息处理。此时，将错误消息集成到PCP检查器中非常容易。结果如图4所示，其中@是Isabelle请注意，可靠性证明几乎保持不变w.r.t.图3.我们只是将假设可检验的pcp解变为isOK（可检验的pcp解）。这是可行的，因为在我们设置之后，Isabelle（n ∈x ∈set solution. x<长度pcp）解决方案/= []concat（map fst（map（pair-of-index pcp）solution））=concat（map snd（map（pair-of-index pcp）solution））它再次谈到了布尔连接词，并且根本不包含任何一元值或错误消息。C. 斯特纳格尔河Thiemann/Electronic Notes in Theoretical Computer Science 312（2015）5159⇒≡≡⇒⇒type-synonymshows=stringstringclassshow=fixesshows-prec：：nat′a shows和shows-list：：′一个列表示出假设shows-prec p x（y@z）=shows-prec p x y@z和shows-list xs（y@z）=shows-list xs y@z开始abbreviationshows-prec0abbreviationshow x shows x[]end图五. 一个显示-类在伊莎贝尔/HOL4可读错误消息在上一节中，我们使用了一些基本的错误消息。然而，这些只是静态字符串。例如，使用证书[1， 3， 2， 3， 4， 1， 2]调用pJ上的check-solvable会产生输出。确保PCP满足性的InlJJ问题：索引i无效JJ索引i invalid中的类似地，如果不匹配，则不显示结果单词，并且也不显示实际分析的PCP实例实例然而，要生成所有这些错误消息，我们需要一些功能来显示任意值。为此，我们引入了一个类型类show，类似于Haskell类接口如图5所示。在这里，show是从字符串到字符串的函数类型，它允许常数时间连接。对于show-类的每个实例Ja，有一个函数shows-prec，它具有优先级（可能在括号中）和类型Ja的值。给定的值被转换成一个字符串，包装在shows类型中。要以特殊形式显示列表，可以使用shows-list，例如，以允许字符串的特殊处理，在Haskell和Isabelle中只是字符列表根据Haskell文档应该满足的show-law（或多或少地声明show-function不允许修改传入的字符串）在Isabelle类定义中强制执行除了必须为每个实例定义的shows-prec和shows-list之外，还有函数show和show不需要任何优先级，并提供一个字符串，可能包装到类型show中。请注意，与Haskell在实例化期间定义shows-prec（在这种情况下，shows-list获得默认实现）相比，在Isabelle为此，我们设计了一个专用的命令standard-shows-list，它基于shows-prec自动生成shows-list的定义，并使用shows-prec的定义证明shows-list的show-law。例如，图6中提供了单元类型的实例化。以类似的方式，我们为列表、N、Z、Q和产品定义了show函数仅针对字符，我们定义了一个专用的shows-list函数。60C. 斯特纳格尔河Thiemann/Electronic Notes in Theoretical Computer Science 312（2015）51{⇒⇒instantiationunit：：show开始定义shows-prec p（x：：unit）=shows-string′′（）′′lemmashows-prec-append-unit：shows-prec p（x：：unit）y@z=shows-prec p x（y@z）通过（简单添加：shows-prec-unit-def）标准显示列表显示前附件单元端图第六章实例化单元类型的show类funcheck-solvable：：（′a：：show）pcp-problemI pcp-certi tificate显示检查哪里检查可解PCP溶液=DOcheck-all（λi. 1<长度PCP）溶液<+吗？ （λi. ′′index′′+#+显示i +@+显示′′invalid ′′）;let pair-list=map（pair-of-index pcp）solution;检查（解决方案[]）（显示"解决方案不能为空"）;let left=concat（map fst pair-list）;let right=concat（map snd pair-list）;check（left=right）（“"结果单词不相等：”“+#+显示左+@+"”！=′′+#+显示右侧）}<+？（λs. "确保PCP满足性的问题“”+#+显示PCP +@+显示-nl +@+ s）见图7。 具有正确错误消息的认证对于Isabelle的其他一些标准类型，即bool、sum和option，我们使用了一种更自动化的方法，类似于Haskell更准确地说，我们已经编写了一种策略，可以自动定义数据库的show函数-打印数据库的构造函数并添加括号-并证明所需的show-law。然后就可以用简单的命令来实例化show-class：deriveshowdatatype.虽然我们可以使用这个工具来定义N和products的实例，但我们并没有选择这个解决方案来获得更好的表现。目前，show（3，True）的结果是字符串（3，True），而如果我们使用derive，结果将是Pair（Suc（Suc（Suc（zero）（True）。现在可以使用show将正确的错误消息添加到PCP检查器中图7.在这里，+#+和+@+分别是字符串类型的常量时间连接运算符，分别是字符串showshow和字符串showshowshow当将新定义与图4中的前一个定义进行比较时，人们首先注意到检查可解类型的不同：字母Ja的类型现在配备了类型类约束show。此外，生成的错误消息的类型是show而不是string。在定义中，很明显错误消息从静态变为动态，例如，打印索引i，显示结果单词，甚至在错误消息中返回整个PCP实例请注意，所执行的修改（w.r.t.图4）不需要在可靠性证明中进行单个改变。C. 斯特纳格尔河Thiemann/Electronic Notes in Theoretical Computer Science 312（2015）51615解析让我们简单地概括一下我们到目前为止所取得的成就：我们可以方便地定义类型为输入验证的检查-prop程序，它保证语义属性，在拒绝的情况下提供可读的错误消息，并且可以通过代码生成导出到各种目标语言因此，为了验证一些具体的输入和证书，只需要将自动证明器提供的输入和证书转换为check-prop所期望的输入和证书类型。然而，这些转换通常取决于代码生成器和目标语言：Isabelle类型如何在生成的代码中输入和证书构造器的确切名称是什么等等。因此，我们建议仅构建一个不需要任何维护的解析器，而不是必须构建几个解析器--每个目标语言一个解析器--并且还通过例如反映代码生成器的命名方案中的改变来这个想法是直接在证明助手中定义解析器。然后这个解析器也可以导出到所有目标语言，唯一必须维护的目标语言接口是字符串。由于我们不知道任何自动解析器生成器的证明助理，即，生成器在证明助手的逻辑内自动生成解析器，我们开发了一些机器来简化解析器的手动定义。在这里，我们只使用结构化XML格式的输入和证书。我们的支持分为两个步骤：我们提供了将字符串解析为XML文档的功能（伴随着Isabelle数据类型来表示XML文档），以及一组组合子来简化XML文档的解析5.1一个从字符串到XML的对于第一阶段，字符串应该转换为XML，我们指定了一个手写的解析器作为一个monadic函数，其中monad是一个带有错误的状态monad，即，它捕获一个状态（剩余的字符列表）并返回正常结果或以错误消息结束。这个解析器对monad使用do标记，很容易以可读的方式定义。例如，最复杂的解析器是图8中描述的XML节点列表解析器，其中当前状态大部分隐藏在monad中，xml list parser只是字符串string+（xml list×string）的缩写。然而，由于我们使用Isabelle这需要对状态单子的内部状态进行冗长的推理，我们必须证明一些辅助解析器实际上在每次递归调用解析节点之前消耗令牌，并且在递归调用之前调用的解析器都不会增加令牌列表的长度，其中包括解析节点本身。因此，一个简单的结构性终止参数是不适用的，相反，我们写了一个160行的证明，同时显示了终止和结果令牌列表长度的减少62C. 斯特纳格尔河Thiemann/Electronic Notes in Theoretical Computer Science 312（2015）51←{←/∨}{{←←{←′←←←}'}'}解析节点ts=（如果ts=[] 取2 ts=′′′′，′′> ′′];λts. 如果e=′′/>′′然后（做cs parse-nodes;return（XML n atts[]#cs））tselse（docsparse-nodes;exactly"";ns个解析节点;return（XML n atts cs#ns））ts）ts）图八、一个XML节点列表的解析器作为第一阶段的最终结果，我们提供了一个类型为string+xmldoc的doc-of-string函数，它接受一个字符串并返回一个错误消息或一个XML文档。5.2XML解析库在第二阶段，必须定义输入和证书的XML解析器，我们通过一组组合子来支持证书的开发人员，这些组合子可以用来轻松定义解析器。与§5.1相反，这里我们没有使用函数包，而是使用Isabelle优点是这个命令允许我们定义函数而无需任何终止证明。正如前一段所指出的，即使对于简单的解析器，这些终止性证明也会变得相当乏味;事实上，在使用部分函数之前，我们经常只是假设各种解析器的终止性是公理。然而，使用部分函数有一个先决条件：函数必须是一元的，并且单调w.r.t.某个具有最小元素的点完全偏序，这是指定非终止性情况下的行为所必需的。原则上，错误monadJa+Jb将是XML解析器的适当返回类型。然而，这种类型不满足前提条件，因为它不具有唯一的最小元素，因为它允许不同的错误消息。为此，我们定义了一个专用的一元类型Ja+Jb，构造函数LeftJa（用于错误），RightJb（用于结果）和（用于非终止）。此外，更改结果或错误消息是这种类型上的单调操作为了方便地指定这种类型的一元XML解析器，我们提供了几个C. 斯特纳格尔河Thiemann/Electronic Notes in Theoretical Computer Science 312（2015）5163⇒⊥⇒⊥⇒×⊥←⇒⊥{<？=”1.0“？>><？- 样式表type=”text/xsl”href=”pcp. xsl”？> ><证书><公司简介<配对>sym>A/sym>/lh s>sym>A/sym>sym>B/sym>sym>A/sym>/rh s><配对>sym>A/sym>sym>B/sym>/lh s>sym>B/sym>sym>B/sym>/rh s><配对>sym>B/sym>sym>A/sym>sym>A/sym>/lh s>sym>A/sym>sym>A/sym>/rh s><产品展示<解决方案>0/id x>id x>2/id x>id x>1/id x>id x>2/id x><解决方案图第九章XML中的PCP实例p及其解决方案定义certificate-of-xml：：xmlstring +PCP认证哪里certificate-of-xml= XMlt. 许多“”解决方案"（XMlt. nat′′idx ′′）idpartial-function（sum-bot）pcp-of-xml：：xmlstring +字符串pcp-problemI哪里[代码]：pcp-of-xml xml=XMlt. 许多“PCP”（XMlt. 对“”对“”（XMlt. 许多"lhs"（XMlt. text′′sym ′′）id）（Xmlt. 许多"rhs"（XMlt.text′′sym ′′）id）对）id xml定义parse-input-and-certificate：：stringstring+（字符串pcp-问题Ipcp-证书）哪里parse-input-and-certificate s =（case Xml. doc-of-strings ofInle误差eInr文件编号XMlt. 对“证书”pcp-of-xml证书-of-xml对（根节点文档））定义证书：：stringstring +字符串哪里证书s=do（pcp， c）parse-input-and-certificate s;（case（check-solvable pcp c）ofInle误差（e"）| Inr-⇒ return ′′certified that pcp is solvable ′′)}图10. PCP可解性的解析器和证明器基本的解析器（字符串、数字等）以及pair或many这样的组合子，它们组合两个解析器，或者将单个XML节点的解析器提升为XML节点列表上的解析器。虽然这些组合子的定义很简单，但我们想提一下，设置组合子并不是一个完全微不足道的任务：我们必须以一种方式配置Isabelle，即由组合子定义的解析器所需的单调性证明是自动的。对于PCP，可以使用组合子轻松设置XML模式和解析器，参见。图9和图10。前者以XML格式提供PCP实例p的证书，后者显示解析器以及函数证书，函数证书是调用所有必需组件的最终证书|64C. 斯特纳格尔河Thiemann/Electronic Notes in Theoretical Computer Science 312（2015）51主要（主要）验证人--认证符. 环境--for getArgs.--因为文件读取. 出口--因为错误代码主要=args-.args1 ->输入<-（args！！0）开始输入--“美国一个ge：. pcp. 证书湾xml“开始输入=验证器输入松博特（印度卢比）留言）->“接受“消息松博特（包括留言）->“住所“消息（退出失败1）见图11。 一个Haskell包装器来验证证书首先，定义解决方案和PCP实例的解析器。前者，certificate-of-xml是一个标准的（非递归的）定义，后者pcp- of-xml是通过部分函数定义的，可以使用递归而不需要终止;然而，PCP的格式非常简单，不需要递归然后，parse-input-and-certificate将字符串到XML解析器与XML解析器