局部树更新的上下文逻辑推理

理论计算机科学电子笔记158（2006）399-424www.elsevier.com/locate/entcs关于树更新乌里·扎尔法蒂英国伦敦帝国理工学院计算机系菲利帕·加德纳2英国伦敦帝国理工学院计算机系摘要分离逻辑和上下文逻辑已经被用来在本地推理堆更新和简单树更新。我们研究本地推理的上下文逻辑的基础上，更现实的，本地树更新语言，更新命令与查询相结合。这种组合导致多个位置的更新，这大大降低了推理的复杂性。保留字：局部推理，上下文逻辑，树更新1引言O’Hearn, Reynolds and Yang introduced the concept of 这个想法是，如果一个更新只访问堆的一部分，而其余部分不变，那么这个局部性属性也应该在推理中被考虑。在Calcagno中，我们最近引入了上下文逻辑[3]，以允许对诸如树之类的非线性结构进行类似的推理。虽然我们公正地1电子邮件地址：udz@doc.ic.ac.uk2电子邮件地址：pg@doc.ic.ac.uk1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.04.020400联合Zarfaty，P.Gardner/Electronic Notes in Theoretical Computer Science 158（2006）399我们的逻辑部分地通过对简单的命令式树更新命令的推理，我们没有将我们的想法应用于涉及更新命令与查询的集成的完整的、现实的树更新语言。这被证明是一个重要的步骤，因为在多个位置处的更新和树的非重复性的组合意味着我们不能直接使用O 'Hearn等人。的小公理方法，其中命令仅在堆或树的一部分上指定，它们是一个对象。在本文中，我们表明，我们仍然能够本地推理我们的树更新语言。首先，我们描述了我们的语言，其中令我们惊讶的是需要一些非标准的，但我们相信自然的，设计的选择。我们专注于当地的指挥。如果命令在树上的结果是相同的，则该命令是本地的，而不管该树放置在哪个上下文中。堆的更新命令自然是本地的。我们必须非常努力地寻找一个非局部命令：例如，命令“remove all the values 25 from the heap”是非局部的，但实际上不会使用。相比之下，目前用于更新网络数据的语言几乎都是非本地的。例如，tree-update命令这个命令的一个自然变体是 这也是非本地的，因为位置n可以不是在树中，但可能会出现在更广泛的背景下。然而，我们可以给出这个命令的本地解释：如果n在树中，那么处理所有标记为a的节点;如果n不在树中，那么返回一个错误。我们关注这些局部命令的最初动机是，它们对于我们探索局部推理是必不可少的。我们现在还相信，当将树视为可更新的数据存储而不是完整的文档（如XML文档）时，本地命令是很好的设计实践我们提出了一个霍尔逻辑推理本地我们的树更新语言。以前的工作局部推理使用分离逻辑突出使用小公理指定本地命令。这些公理只提到了由命令（足迹）所涉及的堆的一部分，并使用帧规则扩展到整个堆。例如，考虑本地命令这只是a取地址n，它的小公理是{n<$→−d}是posen{0}，其中前置条件声明堆只是一个地址为n的单元，后置条件声明该单元已被删除。precondi-tion对应于执行命令所需的最小安全条件。小公理只描述了命令在联合Zarfaty，P.Gardner/Electronic Notes in Theoretical Computer Science 158（2006）399401--特殊细胞为了将其扩展到更大堆的属性，我们使用框架规则来导出三元组{P<$（n<$→）−}dispose{P<$0}其中前提条件规定堆可以不相交地分成具有任意值的单元n和具有属性的堆的其余部分。P，这是由dispose命令执行的。后置条件具有相同的结构，移除的单元格指定为0。小公理和框架规则是优雅的，直观地表达了命令的行为。此外，命令的最弱前提条件在此框架中是可导出的，这是提供验证工具的自然要求。独立于分离逻辑的发展，Cardelli和Gor- don发明了环境逻辑[5]用于静态树的推理。由于这具有类似的推理风格，一个自然的问题是是否可以基于环境逻辑来开发用于树更新（XML更新）的局部Hoare推理通过卡尔卡尼奥，我们已经证明这是不可能的。相反，我们必须通过引入上下文逻辑从根本上改变我们对结构化数据的推理方式[3]。本地数据更新通常识别要替换的数据部分，删除它，并在同一位置插入新数据。有了上下文逻辑，我们可以推理数据和插入位置（上下文）。我们已经表明，上下文逻辑可以用来开发本地霍尔推理树更新，堆更新（类似于分离逻辑推理，一个重要的健全检查），和长期重写（逃避使用分离逻辑推理）。在我们最初的论文[3]中提出的树更新的局部Hoare推理使用了与堆情况类似的小公理和框架规则。在本文中，我们表明，这样的推理是不可行的本地树更新语言在这里，因为命令的行为在树中的一些不同的位置，而不是只有一个位置。例如，考虑局部树命令 这个命令的足迹很复杂：m和n可能位于树的不相交部分，或者一个节点可能位于另一个节点之下。因此，不可能简单地使用小公理进行推理。尽管如此，本地霍尔推理仍然是可能的，我们的语言，使用不同的公理风格的前提条件描述满足适当的安全属性的任意树。例如，我们的“dispose l”公理{Ql <$x} dispose l {fold（λn，Q. （图a，k，y。 （a n：k [y]<$Q）（0）xl}前提条件指定了安全属性，即所有由l表示的位置都在给定的树中，并将给定的树与值x相等，我们402联合Zarfaty，P.Gardner/Electronic Notes in Theoretical Computer Science 158（2006）399在后置条件中使用如果l有值{n}，则后置条件等于a，k，y. （an：k[y]nx）（0），它指定可以用树an：k[y]替换空的子树0以获得原始树x。 对于任意位置集合L中，归纳折叠断言从L中一个接一个地挑选位置N，用形式为An：k[y]的树替换空子树，以最终获得原始树X。这个公理并不小，因为前提条件并没有指定命令所涉及的树的确切部分（由l表示的节点）。我们的推理仍然是局部的，因为我们可以应用框架规则将推理扩展到更大的树。它也比较容易使用，因为公理组合为复杂程序提供安全条件，并且最弱前提条件的推导显示出高度的规律性。我们的公理风格无疑不如小公理方法优雅。关键是我们已经确定了一个局部更新的例子，其中简单的小公理推理是不可行的。在本文中，我们证明，这是可能的，做本地推理，虽然与非小公理。未来的工作仍然是调查，通过转向一个明显更复杂的上下文结构，我们是否可以重新获得小公理方法。相关工作我们最近在Biri和Galmiche关于Hoare推理的工作[ 2 ]中看到了我们的公理风格，该工作是部分受到我们在上下文逻辑方面的工作的启发，他们提出了资源树作为XML文档的替代模型。它们使用兄弟唯一性实现唯一节点地址，这允许在树上使用全组合操作符，在树内的资源上使用部分组合操作符。他们为他们的更新语言提供了Hoare推理，基于Bunched Logic和路径推理（具有唯一的解决方案），而不是上下文逻辑。他们的工作是基于一个简单的更新语言，如[3]中的语言，而不是这里研究的多位置语言。从他们的讨论中，我们还不清楚是否可以使用小公理方法（除了一个命令之外，他们对所有命令都有框架属性），或者是否像我们怀疑的那样，他们的路径推理需要非小方法。2树模型我们的树模型由一个标记的树结构组成，具有唯一标识的节点和每个节点上的一组指针：节点标识符允许我们在本地更新树，标签允许我们使用路径表达式遍历树，指针提供到数据结构其他部分的链接。该模型是联合Zarfaty，P.Gardner/Electronic Notes in Theoretical Computer Science 158（2006）399403≡≡|Ghelli [4]使用指针集而不是[3]中使用的单个指针。它类似于《Web上的数据》[ 1 ]一书中研究的树我们的树模型可以使用ID和IDREF类型属性以XML表示法来描述。给定节点名n∈ N和标签a∈ A的有限集合，我们将特定节点处的链接定义为有限节点集L∈ Pfin（N）。树T∈ T和上下文C∈C定义如下：T：：=0|an：L[T]|不|TC：：=− |an：L[C]|不|C|C|不在上下文中插入一棵树被写为C（T），并以标准的方式定义我们假设树和上下文上的一个简单的结构同余，记为T1T2和C1C2，它表明并行组合（）与恒等式0是可交换的和可结合的。另一种选择是使用非交换组合，以更接近XML表示法。这个选择需要我们的推理做一个微小的改变。一个格式良好的树或上下文是一个节点标识符是唯一的。我们假设所有的树和上下文都是良构的。我们把树T的节点标识符集写成节点（T）。我们不直接关心节点标识符的实际名称：我们的更新语言不直接引用它们，就像标准堆更新一样，append命令重命名要插入的树以避免名称冲突，这也是标准做法。我们说两棵树是等价的模重命名，写为T1T2，如果每一棵树都可以通过重命名它的节点标识符和任何内部指针映射到另一棵树上。我们给出了一个标准的例子[1]的树与指针，以说明我们的符号。 我们还将在后面的文章中使用这个例子来展示一个示例更新程序的效果。c〇unt ryn1：{n2，n3}[T1]|cityn2：{n1}[T2]|cityn3：{n1}[T3]3本地更新语言我们为树模型提供了一个核心更新语言，将原语更新命令与查询命令集成在一起。与关系数据库的更新不同，树的更新语言很少被深入研究（但参见[13]）。我们强调本地查询和更新命令对我们的树的重要性这种强调是非标准的。世界上大多数语言404联合Zarfaty，P.Gardner/Electronic Notes in Theoretical Computer Science 158（2006）399A × P N ×T文献是非本地的：例如，查询命令相比之下，我们对查询“return allthe nodes labeled a under l”的解释考虑到我们将树视为潜在的大型数据存储，而不是一个封闭的文档（如XML文档），我们认为使用本地命令是一个很好的设计实践。此外，局部性对于本文所研究的局部推理是必不可少的。3.1存储模型和表达式我们的数据存储模型由两个部分组成：存储s∈ S，它将变量映射到值，以及工作树T。 我们的命令语言使用三种类型的变量：VarT={x，y，. 对于树; Var L={k，l，. };并且Var A={a，b，. }的标签。一个store是一个局部的，有限的函数s：（VarA~finn）(VarL~finn（））(VarT~finn）. 我们不要求存储节点标识符的变量，因为我们的语言只处理位置集的更新 我们写[s|x ← v]表示s被s（x）= v覆盖。我们定义树表达式ET，链接表达式EL和标签表达式EA：E T：：= x |0E L：：= l |A：：= a|a ∈A我们写[[[E]]s表示E相对于存储s的估值。请注意，表达式不引用显式的节点标识符，就像堆更新语言中的表达式不显式引用堆地址一样。相反，我们的语言只是间接地引用标识符，通过查询树来获得节点标识符集，或者使用“new”命令来创建具有新标识符的新节点。3.2本地查询我们给一个抽象的本地查询。我们所有的结果都将在这个抽象的层次上给出。节中3.3，我们描述了一种特定的查询语言来帮助示例，并说明本地查询仍然可以表达。定义。一个查询q：S × T → Pfin（N）<${error}是一个函数，使得q（s，T）∈ Pfin（N）蕴涵q（s，T）个节点（T）。一个查询q是局部的当且仅当q=s，T，L，C. q（s，T）= L和C（T）良构意味着q（s，C（T））= L。我们的定义是非标准的。我们在没有节点满足查询时返回空集和在没有节点满足查询时返回“错误”之间做了本质上的区别联合Zarfaty，P.Gardner/Electronic Notes in Theoretical Computer Science 158（2006）399405查询在树上定义不好：例如，如果它试图跟随一个悬挂指针。这是因为我们决定使用本地查询：如果一棵树足以使本地查询无错误地执行，那么查询将保证永远不会我们将在Sect中进一步解释这一点3.3我们给出了本地查询的具体示例。3.3一种局部查询语言对于我们的结果，我们将使用抽象查询。在这里，我们简要描述了一种由XPATH [14]激发的本地查询语言，以帮助示例，并表明我们并没有因为转向本地查询而失去太多的表达能力：q= l/π|克|克|q-q查询π：：= π a：：π f|π/π |π ∪ π |π ∩ π |π − π路径π a：：= self|孩子|后裔|母|链路 路径轴线π f：：= E A|标签过滤器一个基本查询l/π是L. 然后它 每个路径步骤由一个路径轴组成，该轴描述了下一个路径轴是不言自明的，除了“链接”轴，它“跟随”来自当前节点的所有指针。注意，任意的祖先轴是不可能的，因为它会破坏我们的局部性要求。 我们还要求l给出的所有初始节点都在树中，否则查询将返回错误。 类似地，当一个查询试图通过跟随一个悬空指针或树根处的父轴来“移动”到树外时，我们会得到一个错误这些条件使我们的查询本地.例如，查询l/descendant：：a返回由l给出的节点标识符下标记为a的所有节点，如果所有标识符都在树中。如果一个标识符不在树中，则查询将导致错误。这个选择类似于本地堆更新，如果堆中不存在地址，则返回错误。有人可能会说，如果至少有一些节点在树中，查询应该能够返回部分答案，但如果我们要求推理是局部的，这就不可行。附录中给出了这种语言的查询语义。下面是我们的语言中的一些其他简单的查询示例，使用一些标准符号：πfforchild：：πf，'. 'for r p a r e n t：：band'。’• l/city-l的所有• l/city_link：：city-l的所有' city '标记的子节点或链接目标。406联合Zarfaty，P.Gardner/Electronic Notes in Theoretical Computer Science 158（2006）399特里斯分配查找更新动议新x：=E不L油墨lJ：=ELlJ：=qlJ：= get-links atldispose-links atlappend-linksEL atl拉阿贝尔a：=E一x：=在l在l处处理，在l处附加ET，将l移动到lJlJ：=l处的新EAa：=在l在l处设置标签E一Fig. 1. 基本更新命令• l/（（../ -.）- 我所有的兄弟姐妹请注意，由于局部性条件，这将返回根级别节点的错误3.4更新命令我们提出了我们的高层次的命令式更新语言，本地manipulat- ING树指针。图中给出了基本命令。1.一、它们包括用于分配、查找和更新的命令，每个命令都有用于树、链接和标签的相关表单。它们还包括“移动”和“新建”命令。我们假设命令序列C;C，但不提出循环控制命令，因为他们不有助于本文提出的想法。扩展到包含这样的循环命令，以及相应的扩展到推理，是标准的。这些命令应该相当熟悉。然而，有一些微妙之处.所有的命令，除了赋值之外，都作用在一组由链接变量l给出的位置上。为了确保命令的位置，我们坚持l给出的所有位置都出现在命令树中执行;否则返回错误。许多命令有几种可能的行为解释：例如，当在一个节点上引用一棵树时，我们可以引用包括该节点在内的整个树，或者只是子森林;当在一个节点上附加一棵树时，我们可以将它附加在节点下面或作为兄弟节点。在本文中，我们选择一个行为的简洁性（前者在上述两种情况下）;我们的选择可以平凡地适应其他行为。更新命令的正式操作语义在附录中给出。我们在这里给出一个非正式的（但精确的）描述。赋值将表达式的值赋给适当类型的变量对于链接还有一个额外的情况，lJ：=q，它计算查询q并将结果节点集分配给链接变量lJ。联合Zarfaty，P.Gardner/Electronic Notes in Theoretical Computer Science 158（2006）399407从链接变量l指定的节点中获取链接，树或标签值（其中我们选择了节点处的树值，以包括该节点处的子树和节点本身）。由于结果是一组值，而我们的语言只使用值，因此存在如何将许多值组合成一个的问题我们为每种数据类型给出一种解决方案：对于树，我们连接结果，必要时重命名节点;对于链接，我们返回结果的并集;对于标签，我们从结果中随机选择。为了简单起见，我们选择使用这些特定的解决方案，但可以很容易地将我们的推理扩展到更抽象的方法。Update更新由链接变量l指定的节点处的树、链接或标签。在树的情况下，这涉及到两个命令：dispose，它处理位于l的树，或者append atl，它将树表达式ET的值附加在l中的节点下面。直接追加是部分操作。 我们选择重命名节点标识符和任何内部链接，以获得总追加函数。这种重命名是标准做法。类似地，有两个链接更新命令，而标签更新由一个命令组成，该命令简单地用新标签替换旧标签Move从源位置删除一棵树，并在一个目标位置添加完全相同的树，而不重命名任何节点。只有当目标位置不包含在源中时，才可能进行移动，而非重命名仅在源和目标目标都只包含一个节点时才有效。move命令很重要，因为非重命名允许我们维护入站链接。相比之下，append命令不能让我们控制入站链接：悬空指针可能通过重命名被捕获，也可能保持悬空状态。New在链接变量l指定的位置创建新节点。新节点具有由EA指定的标签和新鲜标识符，它们存储在链接变量lJ中。节点没有链接，也没有子树。这些可以使用其他命令添加。3.5示例我们提出了两个简单的程序，显示容易折叠的链接结构。第一个折叠位置l处的所有链接;第二个仅折叠由变量lJ给出的链接。在右边，我们展示了“崩溃”的动作408联合Zarfaty，P.Gardner/Electronic Notes in Theoretical Computer Science 158（2006）399N∈K所有链接二、在l处关闭所有链接k：=l/link：：n;x：= get-trees atk;appendx atl;dispose-links atl在l处的链接lJk：=l/link：：链接lJ;x：= get-trees atk;在l处附加x;kJ：=l/link：：−lJ; dispose-linksatl;append-linkskJatl在l处附加所有链接，其中l={n1}请注意，当l引用多个位置时，这两个程序仍然可以工作。4树更新的上下文逻辑我们将上下文逻辑推理应用到我们的树模型中。这里提出的大多数思想都是与上下文逻辑相关的先前思想的变体。我们还介绍了一些简单的归纳谓词的位置集的工作。4.1环境虽然我们的更新语言使用变量来广泛地表示节点集，但它并不直接引用单个节点标识符。然而，对于我们的霍尔推理，必须提及并量化这些标识符。我们定义节点变量Var N={m，n，... }和环境e：Var N~finn。为了允许在节点集和标识符之间进行比较，我们还可以将链接表达式扩展为EL：EL：：= EL|{n} |ELEL|ELEL[2019 - 05 - 19 00：00：00][2019 - 01：00][2019 - 01：00][2019 - 01：00]4.2逻辑上下文逻辑由两种断言语言组成：树P ∈ P上的断言和上下文K上的断言. 两种语言都包含标准断言从布尔一阶逻辑，结构断言分析树和上下文结构，这是新的上下文逻辑，和专门的断言联合Zarfaty，P.Gardner/Electronic Notes in Theoretical Computer Science 158（2006）399409P：：= K（P）|KP的结构性断言树断言上下文断言e，s，T K（P）i C，T J. （T_j）C（T_J）_ e，s，C_P_1、P_2和T_（？）（e，s，T）e，s，T K P C. （e，s，CKC（T）e，s，CK e，s， TP）e，s，C−i <$C−合式的C（T）（n =2）e，s，TETiT=[[ET]]se，s，T[[P]]iTJ. （TTJe，s，TjP）e，s，CEA（n：EL）[K]iCJ. （e，s，CjK合式的C（T）（s，s，C（T）（P））e，s，TEA=EAJi[[[EA]]s=[[EAJ]]se，s，TEL=ELJi[[[EL]]es=[[ELJ]]ese，s，TELq（. ）i<$q（s，T）=[[E<$L]]ese，s，C |K i ZaoT，CJ. （C）|CjC[[EA]]s（[[n]]e，[[EL]]es）[CJ]）e，s，T Pe，s，C jK）图二. 结构断言和特殊断言与我们的树模型相关联断言由语法定义[[P]] |E TEA= EA|EL= E|ELq（. ）特定断言PP|错误的古典断言P.P.|P.P.|P. |Pquanti filersK：：= PD P|-结构断言EA（n：EL）[K]|P|KspecificassertionsKK|错误的古典断言x.K| K.L.K|K.K. |Kquanti filers结构化和特定断言的语义在图中给出。2，使用在环境、商店以及树（对于P）或上下文（对于K）上定义的过载满意度关系。结构断言构成了语境逻辑的本质。应用公式K（P）指定给定的树可以被分成满足K的上下文应用于满足P的子树。例如，如果True False等于 False，则公式True（P）表示某个子树满足属性P。我们也有应用的两个右伴随。第一个，KaP，被给定的树满足，如果，每当我们成功地将树插入到满足K的上下文中，那么结果tree satisfiesP.例如，公式Truea P表明，无论我们将给定的树放在什么上下文中，结果都将满足P。同时，另一个伴随，P1DP2，满足给定的上下文，如果，每当我们成功地插入一个满足P1的子树，那么得到的树满足P2。例如，如果true false≠ false，则上下文公式trued P2表示，无论将哪个子树放入给定的上下文中，结果都将满足P2。这种伴随对于表示更新的最弱前提条件是必不可少的。断言-指定空上下文。布尔一阶逻辑的断言是标准的，因此是410联合Zarfaty，P.Gardner/Electronic Notes in Theoretical Computer Science 158（2006）399∀¬ ∧∨∧ ⇔∧图中未给出。二、我们使用派生的连接词，和。我们扩展量化了值变量（树，链接，标签）和节点变量，并导出。上下文逻辑的大部分例如，我们经常会使用下面的推导公式：• QPTrue（P）指定在某处性质P成立;•P1<$P2<$（P1D<$P2）说明存在满足P1的树，使得当将其放入给定上下文的洞中时，结果满足P2;• K（P2<$（KP2）说明存在满足K的上下文这样，当给定的树放在洞里时，结果满足P2;• P1和P2（− P（P1DP2））（true）说明，只要一棵树满足P1则它也满足P2。特定的树和上下文断言专门用于我们的树更新应用。上下文断言直接对应于树的上下文结构：断言EA（n：E_L）[K]是将上 下文断 言扩 展到树的上下文结构的断言。由EA（n：EL）和K的子文本描述;P|K指定上下文可以水平拆分为满足以下条件的树：P和满足K的上下文。由此我们定义子类似的树断言，记为P|Q为（P|−）（Q）andndEA（n：E<$L）[Q]forr（EA（n：E<$L）[−]）（Q）. 另一个断言K|P，对应于右边的平行构图，不需要，因为我们的树是可交换的;然而，添加它可以让我们很容易扩展逻辑来处理非交换树。此外，我们有以下特定的树断言：重命名模态[[[P]]，由任何树满足，该树等价于将节点标识符模重命名为满足P的树（我们将使用这一点来推理树查找和更新命令）;树表达式ET，如果当前树在结构上等于ET的值，则满足;以及等式断言EA=EA，EL=EL和ELq（. ）. 质量标准EA=EA和EL=EL是（E=EJ）K（P）。 这个性质在推导证明中很有用。对于树表达式的等式和等式模重命名，我们没有显式断言，因为它们是可导出的：ET=FTET FTETFTE T[[F T]]。Ourfinalequali tyELq（. ）判断查询q在 当 前 树 上 求 值 时 是 否 返回与E_L相同的值。 注意，althroughE<$Lq（. ）不纯，则我们的查询的逻辑计算意味着如果E=q（. ）h对于一棵树成立，则对于一棵更大的树也成立：即i s，K（（E<$Lq（. ））P）（ELq（. ））.最后，我们给出了一些其他有用的推导公式：联合Zarfaty，P.Gardner/Electronic Notes in Theoretical Computer Science 158（2006）399411• n∈E<$L（E<$L<${n}）={n}• n ∈ E TE T a，k. Qan：k[true]• EL=FLGL（EL=FLGL）（FLGL=）• |EL|为|FL|1996年， xyn. （n∈E<$L惠n∈x<$n ∈F<$L惠n∈y）• QELn. （n∈E<$L<$a，k. Qan：k[true]）前四个断言都是“纯粹的”，并且相当不言自明。最后一个断言的特性是，在E树中的所有位置都在树中。4.3归纳性等同器械我们的更新命令通常作用于一组位置，这些位置可能彼此不相交或嵌套。 为了推理这种更新，我们使用一种简单形式的归纳谓词，它对我们的目的来说足够有表现力，并且对应于节点集上的折叠式运算符。另一种选择是将全递归添加到我们的逻辑中，但我们相信我们的方法对于这个特定的任务更简单。我 们 定 义 了 一 个 有 三 个 参 数 的 归 纳 谓 词 fold ： 一 个 函 数 Pf ：N×P→P，一个basecasertionP0，以及一个链接表达式E L，表示归纳发生的位置集：折叠PfP0EL（（EL=）P0）（伊根湖）（EL=l{n}）Pf（n，foldPfP0l））下面使用来自EL的位置，通过一个不确定的命令，递归地扩展P，其中P0作为EL空着时的数据空间。这个定义是众所周知的，E表示一组有限的位置。注意，扩展顺序的任意性意味着存在替代，折叠的等价定义，它将折叠向另一个方向展开：折叠PfP0EL（（EL=）P0）（伊根湖）（EL=l{n}）n倍PfPf（n，P0）l）作为一个例子，考虑下面的fold断言，我们稍后将使用它来推理dispose：fold（λn，Q. a，k，y. （an：k[y]Q）（0））P0l这个断言被一棵树满足，如果有可能添加根节点为n的子树，对于l中的每个n，以获得满足基本断言P0的树：换句话说，从满足P0的树开始，断言简单地描述了在l中的节点处放置子树的结果。412联合Zarfaty，P.Gardner/Electronic Notes in Theoretical Computer Science 158（2006）399.fold-val（λy，n，Q.对于lookup和new，我们需要一个更有表现力的fold谓词，它在递归展开时计算τ类型的值（其中τ是T，L或A）。我们定义了一个归纳谓词折叠值，这次需要四个参数-函数Pf：τ×N ×（τ→ P）→ P，基本情况断言P0：τ→P，起始值E0：τ，以及一个链接表达式EL：Fold-valPfP0E0EL（（EL=）P0（E0））（伊根湖）（E<$L=l{n}）<$Pf（E0，n，λx. 倍-v（PfP0xl））例如，这使用来自E_NL的l_o阳离子来递归地扩展P，但另外在具有起始值E0的调用之间传递值。例如，考虑以下用于推理树查找的断言：Ja，k，y0，y1. Qa n：k[y1]（yJ[[a n：k [y1] |y0）Q（y0）（λyJ. yJ= 0）y l这说明变量y表示树an：k[y]在l中的节点n处的级联（重命名），当l为空时，基值为0。5程序逻辑我们提出了一个霍尔逻辑推理本地我们的树更新语言。正如在引言中所描述的，我们的树更新的脱节性质，涉及多个，可能嵌套的位置，阻止我们使用小公理规范。然而，我们表明，当地霍尔推理仍然是可能的，使用不同的公理风格。我们提出的公理，给出相应的最弱的先决条件，并表明，推导的最弱的先决条件有一个高度一致的结构。我们还表明，我们的公理风格是比较容易使用的，说明我们的想法使用的三点五5.1Hoare逻辑我们的霍尔逻辑使用霍尔三元组的避免错误的解释：{P} C {Q}保持i，当C在满足P的状态下运行时，则C不出错，并且结果状态满足Q。我们使用四个推理规则：后果，辅助变量消除、排序和框架规则。前三个是标准的[11]。局部推理的关键规则是框架规则：框架规则：{P}C{Q}{K（P）}C{K（Q）}Mod（C）FV（K）={}联合Zarfaty，P.Gardner/Electronic Notes in Theoretical Computer Science 158（2006）399413分配：{（m=EL）0}l：=EL{（l=m）0}更新：{（mq（. ））x}l：=q{（l=m）x}{Qlx}{Qlx}d isposeatl{foldd（λ n，Q. （图a，k，y。（an：k[y]<$Q）（0）xl}{Qlλx}apend-linksELatl{foldd（λ n，Q. （图a，k，y。（an：k[y]<$Q）（an：k<$EL[y]）xl}{Qlx}d是pose-linksatl{foldd（λ n，Q. （图a，k，y。（an：k[y]<$Q）（an：k[y]）xl}在l处附加ET{foldd（λ n，Q. （图a，k，y。（an：k[y]<$Q）（an：k[y]|[[ET]]]]）xl}C：C=y：= get-trees atl{Qlx}在l处设置标签EA{Qlx}C8{foldd（λ n，Q. （图a，k，y。（an：k[y]<$Q）（（EA）n：k[y]）xl}„«9新的：C=k：=新的EA在l<{Qlx}C@ fold-val（λy，n，Q.Ja，k，y，y. Qa [y]01n：k1（yJ[[an：k[y1]|y0）Q（y0））一<：（λyJ. yJ= 0）yl阿克斯fold-val（λk，n，Q.J„，k，a，k，y。 （k = k± {0J0m}）移动：n）=9;J（l={n：（λ kJ. （kJ=）x）kl（an：k[y]<$Q（k0））（an：k[y|EA（m：）[0]]）JJ（0分Qa}）（l=J{n}）ff把l移到lJ J（a[y]（an：Kn：k[z]x）（0））n：K''[y]）（a [z]）xn：K（aJn'：k'[y|an：k[z]]）“的一声;ff图三. （精选）命令公理其中Mod（C）包含由命令C修改的变量，FV（K）是K中自由变量的集合。框架规则将局部行为的概念形式化，声明如果树P对于命令的无故障执行是足够的，那么使用上下文断言K引入的任何附加树结构都不会被该命令改变。框架规则的合理性取决于命令的位置。我们的更新语言中的所有命令都是本地的。5.2命令公理一个有代表性的命令公理的选择是在图。3 .第三章。比较这两个公理给出的分配。第一个公理是的查询求值的公理是类似的，但有细微的不同：前提条件现在指定树具有由变量x给定的值，并且变量m包含执行查询q的结果;后置条件指定树没有改变，并且l具有m的值。关键的变化是，不知道查询的足迹，公理不能小。 相反，公理现在被定义在任意树上，等式mq（. ）充当确保查询可以在该树上执行的安全条件。其他公理都遵循同样的统一结构。所有的先决条件都指定了一个安全条件，使命令能够成功，并将x分配给给定的树。后置条件是所有可能的最强条件，414联合Zarfaty，P.Gardner/Electronic Notes in Theoretical Computer Science 158（2006）399∈所得到的树已经如命令所规定的那样被改变：换句话说，可以撤消所有更新并返回到原始树x。考虑一下update命令，我们已经完整地介绍了这些命令，以强调它们的一致性。前提条件Q1指定所有更新位置必须在树中的安全属性。后置条件规定了生成的树只是通过更新得到的树：换句话说，我们可以用原始子树an：k[y]替换所有更新的子树，对于每个n∈l，得到原始树x。查找公理和new类似，但使用fold-val而不是fold。对于查找，postcon-版本声明给定的树是不变的（x），并且y是由位置n∈l给出的所有（重命名的）子树an：k[y1]的组合;对于new，后置条件声明结果树具有新节点m在每个n∈l，标签为EA，没有子树或链接，这些节点被收集到变量k中。最后，考虑移动公理。安全属性比其他情况更复杂（见Sect。3.4）。它指定源变量l和目标变量lJ的值为树中的单个位置n和nJ，并且nJ不能在n之下。后置条件指出，生成的树在节点nJ下有一个节点n，并且可以将n移动到其他地方（实际上是移动到它的原始位置）以获得原始树x。5.3最弱前提条件我们给出最弱的前提条件，并从命令轴中导出它们。这为直线代码提供了一个完整性结果，并且在构建验证工具时很有用。图中命令的最弱前提条件。3在图中给出。四、注意命令公理和这些最弱的前提条件之间的强对偶性，后者经常与前者“相反”。然而，尽管公理后置条件只需要指定由前置条件产生的存在性，但最弱的前置条件必须描述导致后置条件P的所有可能的树。考虑更新命令的最弱前提条件。使用fold，这些规定，只要有可能从工作树中删除子树an：k[y]，并将其替换为适当的更新子树，则结果树必须满足后置条件P。 请注意，与规范中使用的存在伴随RdQ相比，使用了泛伴随 对于dispose情况，这并不重要，因为 R只满足于结构相等的树（它是“精确的”）。然而，d对于树附加是必不可少的，因为前提条件必须考虑附加树的所有可能的节点重命名。最后，请注意，对于更新联合Zarfaty，P.Gardner/Electronic Notes in Theoretical Computer Science 158（2006）399415分配：{P[EL/l]}l：=EL{P}更新：嗯。（（mq（. ））P[m/l]）}l：=q{P}{foldd（λ n，Q. （图a，k，y。（an：k[y|[[ET]]<$Q）（an：k[y]）））Pl}{foldd（λ n，Q. （图a，k，y。（an：[y]<$Q）（an：k[y]）Pl}{foldd（λ n，Q. （图a，k，y。（0<$Q）（an：k[y]）Pl}在l在L在l处附加ET{P}{P}{foldd（λ n，Q. （图a，k，y。（an：kEL[y]<$Q）（an：k[y]））Pl}apend-linksELatl{P}{P}{foldd（λ n，Q. （图a，k，y。（（EA）n：k[y]<$Q）（ann：k[y]）Pl}在l处设置标签EAC：C=y：= get-trees atl8<{P}：Qly.J0@ fold-val（λy，n，Q.J（λyJ. yJ= 0）yJl„a，k，y，y. Qa [y]01n：k1（yJ[[an：k[y1]|y0）Q（y0）n）1新的：C=k：=新的EA在l9=8>：JBfold-val（λk，n，Q.a，k，y. （an：k[y|EA（m：）[0]] ）CA@.格但斯克（k=k±{0J0Jm}）<$Q（k0））（an：k[y]）（λ kJ. （kJ=）P[lJ/k]）lJl！19>=C{P}n，n. （l={Jn}）（l={J Jn} ）a，k，y，a，k，z.JJ（0分（aJn'：k'[y|an：k[z]]<