KeY Prover: 基于Taclets的交互式定理证明的用户界面

理论计算机科学电子笔记103（2004）67-79www.elsevier.com/locate/entcsTaclets和KeY Prover马丁·吉斯查尔姆斯理工大学计算机科学系S-41296 Gothenburg，Sweden电子邮件地址：giese@ira.uka.de摘要我们简要介绍了KeY证明器[1]-从用户界面的角度。特别是，我们解释的概念taclets，这是基本的基石，证明在基证明。关键词：交互式定理证明，用户界面，taclets1介绍正在进行的KeY项目[1]的目标是使形式化方法的应用在现实世界的软件开发环境中成为可能和有效的。KeY项目的主要产品之一是KeY工具，它允许规范和验证JAVA CARD [16]程序。KeY Prover是一个集成的交互式自动定理证明器，用于KeY工具中，以推理程序和规范。KeY证明器采用的逻辑是用于JAVA CARD的动态逻辑，称为JAVA CARD DL[2]。这可以被看作是一种一阶多模态逻辑，其中模态运算符由程序索引。菱形公式<$π <$φ意味着程序有一个终止执行在π之后φ成立，盒子公式[π]φ意味着φ在每次终止执行之后都成立。证明是用序列式演算构造的。大多数在KeY系统中可用的证明规则象征性地执行DL公式中的程序。例如，处理if语句的规则1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.09.01468M. Giese / Electronic Notes in Theoretical Computer Science 103（2004）67-基本上是：1e，ra;cφ，<$e，rb;cφ，rifethenaelseb;cφ，也有一些归纳规则来推理循环和递归。然而，演算的Meta变量是基础项的占位符，可以引入这些基础项来代替量化器实例化，然后使用统一化来实例化。与合适的呈现机制一起，这允许使用一个公共演算进行有效的自动证明搜索和交互式证明构造，参见[7]。由于程序验证无法完全自动地完成，因此使KeY证明器的交互式用户界面直观且功能强大非常重要。在本文中，我们从用户界面的角度来描述KeY证明器，而不深入技术细节。然而，我们将介绍taclets的想法，这是在KeY证明器中的交互式和自动化证明构造可以从KeY项目主页http://www.key-project.org/免费下载KeY工具2Prover窗口在图1中，示出了KeY校准器的主窗口。 在窗口的左侧部分，整个证明树显示为树结构，显示了应用的规则和案例区别，它们对应于证明树中的拆分。请注意，显示的标签有时是规则的名称（或者更确切地说是taclets，稍后将解释），如int归纳或hide right。但在许多情况下，会打印更多有用的信息，例如int i;表示变量声明语句的符号执行，而{}表示删除空块。此外，分支规则可以为不同的分支分配有用的名称，如这里的归纳规则所示2单击证明树视图中显示的证明步骤，1真正的规则更复杂，由于JAVA语言的复杂性，如e中的副作用，突然终止等，参见[2]2归纳规则允许在“基本案例”和“步骤案例”分支上归纳地证明任意语句。然后可以在“用例”分支上使用已证明的语句M. Giese / Electronic Notes in Theoretical Computer Science 103（2004）67-69Fig. 1. KeY证明器弹出菜单，其允许用户例如在某个点处剪切校样的任意部分。 也可以折叠和展开证明树的部分，这是一个非常有价值的功能，用于更大的证明。 使用左窗格顶部的用户约束主要包含用户在证明过程中选择的量化器实例，但它允许纠正现有证明中的错误实例，而无需回滚整个证明，参见[7]。右窗格包含打开的校样列表。在这种情况下，只有一个问题文件demo.key被打开，但通常情况下，这里的程序验证任务可能会有许多证明义务。似乎更可取的是允许切换证明这种方式打开一个窗口，每一个可能大量的证明。窗口的中央部分显示当前正在处理的序列号。Oppen的pretty-printer风格的格式化引擎如图所示，当前位于鼠标指针下的公式、子公式、项等被突出显示。突出显示与布局一起帮助用户理解复杂公式的结构。请注意，我们选择在公式语法中将自己限制在ASCII字符集上，尽管quantifiers，junctor等。用数学符号表示是很容易的。根据我们的经验，尽管这样的特性受到理论家的欢迎，但它却让最终70M. Giese / Electronic Notes in Theoretical Computer Science 103（2004）67-图二. 选择要应用关键系统的目标客户。显示的公式中的{i：=0}是一个更新，这是我们微积分的一个特殊功能，它表示下面的公式应该在修改后的状态下解释。更新后的公式是包含JAVA程序的菱形公式。该程序由一对额外的花括号包围，主要是为了简化JAVA CARD DL公式的解析。单击公式中的运算符，将显示一个弹出菜单，为该子公式提供可能的规则应用选择，参见图2。在KeY证明器中，构建证明的规则与用户应该如何与这些规则交互的信息相结合，形成称为taclets的实体，这将在下一节中描述在这种情况下，在该特定位置处，仅存在两个适用的taclet我们将展开循环的一次执行。另一种是应用对偶性将这个公式转化为一个在图右边的盒子公式。可用规则的集合被设计成最小化键盘交互的量。例如，命题推理是简单地通过选择一个合适的规则来进行的。实例化量化器的通常方法是不点击量化的公式，而是点击需要实例的项。如果选择tacletsinst all或inst ex，则会出现一个对话框，其中要实例化的量化公式可以从左侧的通用公式中选择。存在公式的右边。同样的ef-M. Giese / Electronic Notes in Theoretical Computer Science 103（2004）67-71还可以使用拖放手势来实现效果。 用户点击该术语并将其拖放到出现在列表中的一个顶级量化器上。仅当需要序列中尚未出现的实例时，用户才选择允许直接使用键盘输入术语的实例化规则。进一步降低用户交互的复杂性源于这样一个事实，即在通常的定理证明器中，大多数量化实例都需要获得公理和引理的实例。在KeY证明器中，这些通常被编码为taclets，参见Sec。3，它可以从应用它们的上下文中获得大部分所需的信息。通过窗口顶部的一组工具栏按钮可以实现许多有用的功能。“应用启发式”和“自动恢复启发式”按钮指的是所解释的taclets的自动应用 在下一节。“RunSIMPLIFY”按钮从目标中提取算术公式，并尝试使用外部定理证明器“GoalBack”删除当前分支上的最后一个校对步骤。最后，快进符号用于控制目前正在实施的证明重用机制，这将允许重用早期的证明尝试，以在程序更改后显示属性，例如由于修复错误。3塔克莱由于本文的重点是用户界面方面，我们只能简要介绍taclets的概念。对于taclets的深入技术讨论，也考虑了与JAVA CARD DL微积分相关的特殊困难，请参见[3]。大多数现有的交互式定理证明器是“战术定理证明器”。这些系统被命名的策略是作用于证明树的程序，主要是通过原始规则的许多应用，其中有一个小的，固定的集合。用户通过选择要运行的策略来构造证明。为了某种目的编写一个新的策略，例如支持一个新的数据类型理论，需要证明者的专业知识在KeY证明器中，策略和原始规则都被taclet概念所取代。3taclet将一条规则的逻辑内容与指示如何以及何时使用它的实用信息结合起来。与通常固定的基本规则集不同，taclets可以很容易地添加到系统中。它们被公式化为简单的模式匹配和替换3Taclets已经以图式理论特定规则（STSR）的名义引入[10]见《易经》。 572M. Giese / Electronic Notes in Theoretical Computer Science 103（2004）67-图式 例如，一个非常简单的taclet可能如下所示：find（b−>c==>）if（b==>）replacewith（c==>）简化这意味着如果公式b也出现在一个式子的左边，那么式子左边的蕴涵b−>c可以被c除了这个它将出现在弹出菜单中时，点击的含义子句explanistics（simplify）表明该规则应该是名为simplify的启发式的一部分。启发式算法就是一组命名的taclets。 用户可以交互式地更改在某个时间应该激活哪些代理。 按下“应用启发式”按钮将应用所有属于 进行某种激活的试探如果勾选了“自动恢复策略”按钮，则在每次交互式taclet应用后自动应用策略。有时候临时切换这种行为是很方便的，可以依次应用几个交互步骤。作为taclets的进一步示例，下面是前面提到的量化器实例化taclets：inst all{if（all u.b==>）find（t）add（{u t}（b）==>）}inst ex{if（==>ex u.b）find（t）add（==>{u t}（b））}当用户点击某个术语t时，如果存在通用响应，则会显示这些规则。左边的存在主义量化器，右下角。 如果有几个，用户可以选择实例化哪一个。语法{u t}（b）表示用t替换b中所有出现的u的结果。4虽然taclets可能比战术定理证明器的典型的最小化的规则更复杂，但它们并不构成战术编程语言。没有条件语句，没有过程调用，也没有循环结构。这使得taclets比tactics更容易理解和制定。结合启发式应用的适当机制，它们仍然足够强大，可以允许舒适的交互式定理证明[10]。对于自动化的执行策略，其思想是任何可能的taclet应用程序最终都将被执行（公平），但某些taclet可能会通过为其附加优先级而被优先选择[4]由于一阶模态逻辑中的非刚性项的困难，实际规则稍微复杂一些。M. Giese / Electronic Notes in Theoretical Computer Science 103（2004）67-73还要注意，taclet是相当轻量级的实体。例如，绝对可以引入几十个ad-hoctaclets来以直观的方式推理某些特定的数据类型。taclets的集合应该并且可以以这样的方式设计，即可用的taclets反映关于某些应用领域的通常的人类推理。将taclet附加到操作符的一个重要结果是，特定数据类型的taclet几乎都将附加到相应类型的操作符。例如，用于对数字进行推理的taclets被附加到+或>=等运算符上，这意味着当用户单击特定运算符时，只有那些与该上下文中的该运算符相关的taclets才会可见。这大大减轻了用户的负担，通常与大型集合相关的规则。 例如，加法的取消法规定， x+z=y+z意味着x=y可以在tacletfind（x + z = y + z）replacewith（x = y）这个taclet将只附加到两边实际上有相同的被加数的等式。原则上，没有什么可以阻止代表不健全的检验步骤的taclet的制定。然而，可以从taclet自动生成一阶证明义务，代表其逻辑内容。如果这个公式可以用一组有限的“原始”taclet来证明，那么新的taclet就保证是一个正确的派生规则。例如，上述取消法taclet的举证义务就是：a+c=b+c→a=b对于一些新的常数a，b，c对于inst所有taclet，一个得到：（n =x.p（x））→p（c）其中p是新的函数符号，c是新的常数。在这方面，taclets与许多基于高阶逻辑的系统不同，在高阶逻辑中，派生规则的正义化是在某些元逻辑中完成的。taclets的证明义务与taclets所依据的证明义务具有相同的逻辑。见[3]详细说明如何计算证明义务。目前在用户界面中没有提供用于taclet的交互式构造。它们以上面所示的文本形式给出，并由解析器读入系统。在未来的版本中，可能会在系统中添加在用户界面中定义taclet的可能性。74M. Giese / Electronic Notes in Theoretical Computer Science 103（2004）67-4执行KeY证明器是用JAVA编程语言（见[8]）实现的，使用Swing GUI库（见[17]）。所显示的证明树、当前数据库等与底层逻辑数据结构之间的协调遵循模型、视图、控制器架构，并大量使用观察者设计模式（参见[5]）。表示证明树的数据结构中的每一个变化都触发相关用户界面组件等待的事件虽然这不是最快的技术，但它有助于提供系统的良好模块化。4.1突出为了帮助用户选择taclet应操作的公式或项，当鼠标指针在指针上移动时，KeY证明器会突出显示鼠标指针所例如，在公式中p&（q|r &s），假设合取（&）优先于析取（|），右合取（q|当&指针位于|或其中一个圆括号，&当指针位于右侧时，r s将突出显示&，如果指针位于左侧，则整个公式将突出显示&。如果指针位于符号p、q、r或s之一上，则仅突出显示该符号。此功能的实现依赖于快速机制来查找与所显示的字符串中的特定字符相这是使用位置表来实现的，位置表记录了嵌套公式和项的开始和结束，嵌套公式和项在每个子公式/项中。位置表是在布局过程中由漂亮的打印机建立的，附加成本很低，而且非常有效。 当鼠标移到屏幕上时，不会因高亮显示而出现可察觉的延迟。位置表具有与所表示的项相同的树结构，因此找到与字符对应的位置的时间在项的深度上是线性的。到目前为止，这已经证明是足够快的。位置表的另一个特点是，它们只存储每个位置的子项的集合，而不是绝对位置的字符串表示。这使得有可能为taclet应用程序不支持的公式重用位置表，前提是其布局不更改。不过，这种优化尚未在KeY系统中实现。一旦使用位置表计算出要突出显示的文本范围，就可以使用JAVA库提供的标准突出显示功能完成实际绘制。M. Giese / Electronic Notes in Theoretical Computer Science 103（2004）67-75目标1TacletAppIndex1+getTacletAppsAtPosition（）+formulaAdded（）+formulaRemoved（）+formulaChanged（）*塔克莱*1*TacletIndex+ getString（）图三. Taclets的索引数据结构4.2Taclet应用索引对于愉快的用户体验，当用户点击某处时，以最小的延迟显示特定位置处的可用taclet也是重要的。第一个要素当然是位置表，它产生一个对应于鼠标位置的逻辑数据结构的句柄。可应用的taclet的实际列表是使用多个索引数据结构由此计算的，参见图3。 考虑到JAVA CARD DL的taclet集合包括数百个taclet，在用户等待菜单时浏览整个taclet集合显然不是一个选项。相反，对于每个打开的目标，都会保留一个taclet应用程序索引，该索引将所有可能的taclet应用程序存储在任何位置。taclet应用程序由taclet及其应用位置和多个由位置确定的模式变量绑定。5taclet应用程序索引的组织方式是，可以根据索引中的位置只有taclet应用程序实际上可能是存储的。例如，在SEC中引用的taclet。3，这必须适用于在先行词的含义。只有对于这样的位置，taclet应用程序才被放入taclet应用程序索引中，并且只有这样它才被显示给用户。taclet应用程序索引的好处是，taclet应用程序之间的大多数索引通常保持不变，因此大多数taclet应用程序仍然有效。在每个证明步骤之后，删除涉及更改的公式的taclet应用程序并添加一些新公式是足够的这一优化正在实施中。在KeY证明器的当前版本中，taclet应用程序索引只是在每次5可能还有未绑定的模式变量;交互式地请求这些变量的实例化。76M. Giese / Electronic Notes in Theoretical Computer Science 103（2004）67-到目前为止，这已经足够快了。4.3Taclet指数在每个证明步骤之后，我们可以重新计算taclet应用程序索引的原因当然是另一种索引数据结构允许有效地做到这一点：taclet索引。它包含所有可用taclet的集合，并提供一个操作来确定一组可能适用的候选项，给定一些公式及其在一个数组中的位置。这个想法是通过一个新引入的公式的所有子公式，并要求taclet索引一个（希望是小的）潜在适用的taclet集合。对于该集合中的每个taclet，然后检查是否实际上满足应用的所有条件，如果是，则将对应的taclet应用放入taclet应用索引中什么索引机制对于taclet索引是合理的当然取决于所使用的taclet的集合例如，目前在KeY证明器中使用的许多taclet因此，我们确保索引可以区分不同类型的JAVA语句之间的taclets。我们使用一个哈希表，该哈希表由所讨论的公式或项的顶级运算符索引，并且在程序模态的情况下，由所讨论的程序中的第一个可执行语句的类型索引。这为交互式用途：应用规则、构建新taclet应用索引以及布局和显示新taclet所需的时间大多在半秒以下。通常使用的taclets标准集包括数百个用于命题和谓词逻辑、整数、集合以及最重要的JAVACARD的taclets。当taclets自动应用时，性能范围从每秒20个taclet指数的性能在未来可能变得不可接受，例如由于taclet基数扩大。在这种情况下，我们的课程将逐步优化索引数据结构。事实上，这在过去已经做了两次：最初根本没有taclet指数。随着谓词逻辑规则数量的增长，引入了对顶部函数符号的散列。最后，随着DL规则的增加，对程序语句进行索引变得必要了。另一个可以设想的未来优化是编译taclet：由于taclet具有相当可操作的语义，因此可以为taclet的操作生成JAVA字节码。特别地，匹配部分可能比比较两个术语数据结构的当前方法更快。M. Giese / Electronic Notes in Theoretical Computer Science 103（2004）67-77目前尚不清楚是否有必要这样做，因为该系统迄今的运行情况相当令人满意。5相关工作Taclets首先由Habermalz以图式理论特定规则（STSR）的名义引入[9，10]。通过将鼠标指向规则应遵循的公式来进行交互式定理证明的概念受到定理证明器InterACT的强烈启发[6]。该定理证明器允许对由条件方程组代数指定的抽象数据类型进行推理。然而，它只提供了一套相对固定的规则特定领域的推理只有通过应用条件方程才有可能有趣的是，用户可以点击方程应该应用的术语。有了taclets，就有可能以一种与领域中的人类推理相匹配的方式来进行特定领域的推理，而不是底层的特定语言。使用鼠标手势来控制定理证明器的想法，称为“指向证明”，已经由Bertot，Kahn和T 'er y提出[ 4 ]。该方法的特点是，在某些子公式上单击单个鼠标可以触发一系列规则应用程序，这些规则应用程序分解公式，直到所选的子公式位于子公式的顶层通过指向的证明仅限于固定的微积分，根本没有特定于域的规则从语义上讲，taclets与基于Isabelle [14]或PVS [13]等高阶逻辑的系统中的策略和/或派生规则有明显的相似之处，但也与来自证明规划世界的概念相似，如EMAMEGA系统[15]的方法。事实上，在基于taclet的定理证明器中，taclet经常扮演派生规则或策略的角色，因为它们可以作为单个实体进行复杂的演绎它们还编码了关于特定领域推理的知识，比如方法。Taclet不同于命名概念，因为它们• 包括用于自动化和交互式应用操作语义，• 不提供任何编程结构，因此• 可以通过在对象逻辑中而不是在某些元逻辑中进行推理来相对于其他taclets进行正当化taclet机制经过精心设计，以显示所有这些属性。78M. Giese / Electronic Notes in Theoretical Computer Science 103（2004）67-6结论我们已经从用户界面的角度简要描述了KeY证明器。特别是，我们已经介绍了taclets的概念，它包含了一个XML规则的逻辑内容，以及如何以及何时应用它的实用信息。我们还简要概述了一些涉及的重要实现问题。KeY系统已多次用于本科教育，学生已经能够使用证明器显示JAVA程序的简单属性我们认为这表明我们的用户界面足够好，允许非专家在经过合理的指导后使用。一些更大的案例研究，由更有经验的成员进行的关键小组在[1]。确认作者感谢Richard Bubel提供了一些技术细节，感谢Wolfgang Ahrendt对本文草稿提出了有益的意见，感谢匿名评审员提出了许多建议。引用[1] Wolfgang Ahrendt，Thomas Baar，Bernhard Beckert，Richard Bubel，Martin Giese，ReinerHa？ hn le ， Wolfr amMenzel ， WojciechMostowski ， Andr easRoth ， St e enS ch l ager ，anddPeterH. 施密特钥匙工具。软件与系统建模，2004年。出现。[2] 伯恩哈德·贝克特。Java Card程序形式验证的动态逻辑。 Isabelle Attali和Thomas P. Jensen，编辑，智能卡上的Java：编程和安全。 修订论文，Java Card 2000，国际研讨会，法国戛纳，LNCS第2041卷，第6-24页。Springer-Verlag，2001.[3] Bernhar d Beckert 、 MartinGiese 、 Elma r Habermalz 、 ReinerHüahnle 、 AndreasRoth 、 Phili ppRuümmer和Ste enSchlager。目标：一种新的写作理论方法。RevistaDe La Real Academia DeCiencias Exactas，Fisicas Y Naturales，2004.出现。[4] 你比我聪明，吉尔比我聪明，L比我聪明。我是说，我是说，我是说，我是说，我是说。 在M。我是一个日本人。 C. Mitchell，编辑，Proc. Intl. Symp.计算机软件的理论方面，LNCS 789，第141-160页。Springer，1994年。[5] Erich Gamma，Richard Helm，Ralph Johnson，and John Vlissides. 设计模式：可重用面向对象软件的元素。Addison-Wesley，1995年。[6] R. Geisler，M. Klar和F.科尼利厄斯InterACT：一个用于代数规范的交互式定理证明器。在Proc.AMASTSpringer，1996年7月[7] 马丁·吉泽。Integriertesautomatischendinteraktivesweisen：DieKalkuülebene. D ip lomaTh esis，Faku ltéatfurIn r m atik，Uiver sitéatKarlsruhe，June1998.[8] 詹姆斯·高斯林比尔·乔伊和盖伊·斯蒂尔Java语言规范。艾迪森·韦斯利1997年M. Giese / Electronic Notes in Theoretical Computer Science 103（2004）67-79[9] 他是我的好朋友。EindynamischesautomatissierbarresinarteraktivesKalkuülfürschematischetheorriespezifischeRegeln.PhDthesis，UniveresitütKarlsruhe，2000.[10] Elmar 哈伯马尔兹交互式定理证明与图式理论的具体规则。TechnicalReport2000年19 月 ， Fakultêtfur？ rInformatik ， Universit ？ t2000 年 的 时 候 。 http ：//i12www.ira.uka.de/cnkey/doc/2000/stsr.ps.gz。[11] 格雷格·尼尔森程序验证技术。斯坦福大学博士论文，1980年。还发表了Xerox PARC研究报告CSL-81-10。[12] 德里克·C奥彭印得真漂亮ACM Transactions on Programming Languages and Systems，2（4）：465[13] S. Owre，S. Rajan，J.M. Rushby，N. Shankar和M.K. Srivas。PVS：结合规范、证明检查和模型检查。在Rajeev Zurr和Thomas A. Henzinger，编辑，计算机辅助验证，CAVSpringer，1996年7月/8月。[14] 劳伦斯角，澳-地保尔森Isabelle ：A generic theorem prover，LNCS第828卷。Springer-Verlag，1994.[15] J. S iek m a nn，C. Ben zmüller，V. Brezhn ev，L. Cheikhr o uh ou，A. Fied ler，A. Franke，H.好吧，M. Kohlhase，A. Meier，E.梅利斯，M。莫施纳岛Normann，M. Pollet，V. Sorge，C. Ullrich，C.P. Wirth，and J. Zimmer.用MEGA进行验证开发。 以. Voronkov，编辑，Proceedings of the18 th Conference on Automated Deduction（CADE–149, Springer Verlag，Germany.[16] Sun Microsystems，Inc. Palo Alto/CA. Java Card 2.0语言子集和虚拟机规范，1997年10月。[17] 凯西·沃尔拉斯和玛丽·坎皮奥内JFC Swing GUI：构建GUI的指南。艾迪森·韦斯利1999年