证明器接口的设计与工程考虑

可在www.sciencedirect.com在线获取理论计算机科学电子笔记285（2012）3-16www.elsevier.com/locate/entcs设计Prover接口霍尔格·加斯特德国图宾根大学信息学院gast@ informatik. uni-tuebingen。de摘要实际的证明器接口是相当大的软件，其构造和维护需要大量的资源和资源。本文论述了这种发展的工程方面。使用非功能属性作为软件的质量属性，我们讨论了哪些属性是特别是相关的证明接口和演示，以伊莎贝尔的I3 P接口为例，如何明智的建筑和设计决策导致具有这些属性的接口软件。通过与其他建议的接口的比较，我们认为，我们的考虑可以适用于以外示例项目。关键词：prover接口，软件工程，软件质量1引言过去对证明器接口的讨论主要集中在用户可用的证明脚本的方便管理[11，8，1，3]是目前使用Isabelle和Coq等交互式证明器的基础。在这种设置中，证明器可以支持用户编写证明脚本[5]，或者检查接近数学文本的证明文档[16]。通过指向证明[10，9，31]，图形证明隐喻[27]或特定于证明者的交互模型[23]承诺改善用户体验。合作证明开发是由网络接口的证明[26]。用于特殊应用的集成验证环境或更复杂的证明器接口[24，13，15]。尽管提出了中型到大型的软件系统，但令人惊讶的是，引用的研究忽略了构建这些系统所需的工程考虑相反，他们专注于广泛的软件结构：代理用于将接口组件与证明器组件解耦[4，32]。Web接口的构建侧重于客户端/服务器通信的技术方面[26]。指向证明接口展示了证明器和接口之间的交互，但不是UI的实现[10，27]。通用接口[24]描述了一个1571-0661 © 2012 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2012.06.0024H. Gast/Electronic Notes in Theoretical Computer Science 285（2012）3具体的Java接口，但省略了主要的插件，Eclipse插件的插件。虽然人们可以争辩说，这种高层次的呈现模式是必要的简洁性，它仍然留下开放的中心问题，在研究用户界面的定理证明器：给定一个理想的功能，如何可以手工制作一个软件系统，将提供这种功能可靠，并尽可能少的编程和维护工作？有一个迹象表明，这个问题确实值得更多的考虑，那就是大多数引用的系统只是作为原型存在，或者没有维持很长时间。本文通过将用户界面构建的标准方法应用于定理证明器的特定领域来解决识别问题。我们基于证明器接口软件的理想非功能特性来讨论工程考虑[6]（第2节）。I3P的具体示例，Isabelle Prover的交互式接口（[21];第3节），然后用于演示工程目标的实现（第4节）。在整个过程中，我们强调定理证明接口的一般原则的相关性。相关工作的讨论（第5节）然后将我们的推理应用于现有系统。2理想的非功能特性软件系统总是有两种可能的观点：它的用户主要对可用的功能感兴趣，以及他们在继续工作时得到的支持;它的开发人员，维护人员，财务人员和项目经理必然对软件的质量提出强烈的要求，这可以通过使用非功能属性来捕获[6]作为质量属性。本节讨论与证明器接口最相关的那些属性，从而为随后提出的工程考虑事项设定目标。软件系统需要随着时间的推移而改变，无论他们的环境或用户需求如何变化。因此，无论是优雅地适应变化在证明器接口的情况下，这种必要性特别明显：因为证明器是研究工具，它们倾向于非常迅速地采用最新的发展，通常需要牺牲向后兼容性。因此，当证明器改变时，接口也可能改变。可维护性软件开发总支出（和成本）的主要部分虽然可维护性与易变性有关，但它的重点是保持现有系统的稳定，而不是改变它以满足特定的需求。对于证明器接口来说，可维护性是很重要的，因为花费在接口上的任何资源都会因为证明器本身的开发而可追溯性可追溯性表达了软件的功能需求H. Gast/Electronic Notes in Theoretical Computer Science 285（2012）35通过建筑和设计，可以追溯到具体的实现。因此，它是可维护性和可更改性的先决条件，因为它明确了哪些部件需要修改以实现特定效果。事实上，使用ProofGeneral/Emacs代码库的经验表明，这是维护运行系统的最大障碍之一[33]。可测试性敏捷软件过程[7，28]已经传播了这样一种见解，即程序员只有在确保不破坏现有功能的情况下，才有信心进行必要的更改。这可以通过在开发期间频繁运行的自动测试来确保。然而，软件必须编写成可测试的：它必须能够独立地访问单个组件，以轻松地识别故障源。由于标定器的快速变化会导致其接口的快速变化，因此可测试性是至关重要的。此外，证明器用户不会容忍仅在请求特定功能时发生的引入故障-他们对接口不感兴趣，而只对证明器本身感兴趣。可重用性开发一个证明器接口需要大量的工作。因此，希望它可以在不同的环境中重复使用，例如在集成验证环境中[24，13，15]。可扩展性如果软件提供了定义良好的机制来集成新功能而不修改现有的代码库，则该软件是可扩展的。特别是，证明器的用户界面必须是可扩展的，以反映新开发的证明器功能，从而为用户带来最大的好处重要的是要注意，这些属性本身并不是目标，而是由一些抽象的软件设计制度规定的。通过确定它们与证明器接口的相关性，给出了真正的目标非功能属性作为实现这些目标的垫脚石，因为软件工程文献提供了实现这些属性的技术，而没有给出证明器接口的任何建议。将一般原理转化为具体应用是本文的一个重点我们还注意到，可用性的属性被故意从列表中省略，因为它是对所包含的属性的补充：它涉及软件对用户的外观，而上述属性则涉及软件的内部结构和质量。虽然可用性是任何界面软件的一个重要方面，并相应地被广泛对待的用户界面的证明者的文献中，本文侧重于内部质量属性。3系统描述本节从用户I3 P编译了当前标准接口Proof General/Emacs（见图1）中已知的主要组件：理论和ML文件的编辑器，处理结果的查看器，以及当前选定理论的树形结构概述6H. Gast/Electronic Notes in Theoretical Computer Science 285（2012）3Fig. 1. 运行系统我们现在将简要地总结它们的功能。理论编辑器组件允许用户编辑证明文档的文本。它提供了一个数学符号的输入工具，模拟Emacs XSym模式。文件像往常一样以编码的XSymbol名称保存。自动缩进遵循的嵌套级别的证明。理论编辑器提供语法突出显示，并处理新Isar关键字的动态定义。该系统的高灵敏度和自动识别功能还能识别嵌入式LATEX和ML源。已处理的命令按预期锁定并突出显示，并且由证明器加载的文件也被锁定理论浏览器组件根据嵌套的Isar证明结构排列当前理论中的命令。它提供了一个上下文菜单用于直接操作[30]，例如：执行或撤消命令，或跳转到编辑器中的结果查看器允许用户检查存储在单个命令状态中的证明器消息（第4.5节）。显示分为正常输出、错误和警告以及跟踪消息。由于保留了先前处理的命令的消息，因此用户可以在证明脚本中返回SML编辑器提供语法突出显示和自动缩进。同样，由证明器加载的文件被突出显示为I3P使用户能够管理不同的已安装证明程序和启动选项（图2）.每个配置都包括一个安装，选择的prover驱动程序（第4.6节）和启动选项，这是Is- abelle的逻辑映像。向导允许用户通过选择prover安装、要应用的驱动程序和要提供的启动选项来定义新的配置。向导是通用的，这样单个的证明器驱动程序就可以确定选项可用。I3P提供了一个用于编辑Isabelle的运行时选项的对话框H. Gast/Electronic Notes in Theoretical Computer Science 285（2012）37图二、在I3P中编辑配置和选项的对话框图三. I3P体系结构概述存储会话之间的设置此外，选项设置可以作为命令本地选项附加到单个命令，然后仅在执行这些特定命令时启用这样的功能是可取的，特别是在工具（如Isabelle的simplifier）没有按预期执行的情况下跟踪它们的行为4架构本节介绍了I3 P的体系结构，该体系结构是为了实现第2节中确定的理想的非功能属性而开发的。通过这种方式，它解释了工程考虑如何导致第3节中提出的整个系统。每个小节都描述了一个特定的设计决策或组件，然后继续讨论所产生的非功能属性。对于可追溯性的属性，我们事先注意到组件，斜体的类型设置，对应于实现的具体类。为了简洁起见，这里省略了更多的结构，但是在可用源代码的JavaDoc注释中提供了这些结构。4.1概述图3概述了I3 P的主要组件。该系统分为三层。在顶部，用户界面层包含用户与之交互的第38H. Gast/Electronic Notes in Theoretical Computer Science 285（2012）3基础设施层包含了I3 P的全部功能：它存储了证明文档和ML文件，以及不同的安装和运行时选项。证明器管理器控制证明器的生命周期，即根据要求启动和停止证明器。文件资源跟踪由prover加载的文件，以使UI层能够在必要时防止修改证明器通信层封装对证明器进程的访问。证明器驱动程序使证明器管理器能够启动特定安装和选项集的进程。驱动程序还允许安装管理器检查安装，例如列出可用的逻辑。当一个prover启动时，prover实例隐藏进程间通信，特别是正在使用的物理协议。4.2文档视图分离4.1节中的概述强调了I3 P体系结构的一个中心特征：基础结构层和用户界面层之间的严格划分。我们将讨论这种分离及其对所产生的非功能特性的影响，然后再进一步讨论，因为它会影响许多后来的设计决策。该决定基于模型-VIEW- C控制器模式的DOC-VIEW变体[14]。此模式中的“视图”是一个仅允许用户访问此功能的组件。在另一个方向上，基础设施和UI层之间的划分可以产生几个理想的非功能属性[14]。首先，可测试性大大增强，因为应用程序的核心逻辑包含在普通的非UI类中，这些类可以通过自动化单元测试访问。此外，测试驱动开发（TDD;[7]）是启用的，因为基础设施和其他人一样，我们发现TDD可以大大提高生产力。可测试性使我们能够为不同的部分编写大约350个单元测试对于大的测试覆盖率，可测试性的含义是可变性（第2节）：我们可以确信进行更改，因为任何引入的故障都会在下一次运行自动化测试时被发现。特别是，重构软件[17]倾向于澄清整体结构，并反过来增强可追溯性和可维护性。文档-视图分离还为可变性带来了另一个好处：由于主要功能独立于UI，因此使UI适应用户的期望变得简单请注意，这种可能性主要依赖于这样一个事实，即测试的目标是基础设施层，而不是UI层。最后，这种分离使可重用性和可移植性成为可能，因为实现的主要部分仍然独立于具体的用户界面。例如，I3 P基础设施已经成功地被重用，以获得基于Eclipse的Isabelle接口[22]，从集成验证环境的角度来看，这是理想的[24，13，15]。H. Gast/Electronic Notes in Theoretical Computer Science 285（2012）39这个非功能属性的列表清楚地表明，严格的文档-视图分离是至关重要的，因为它已经实现了第2节中设定的许多目标。此外，我们发现，分离带来的好处远远超过了开发时间的开销。4.3基于事件的设计I3P的设计始终坚持的第二个原则是依赖于事件.图3中的所有组件都有一个通用的通知机制，可以通知它们状态的变化（参见OBSERVER[18]）：文件资源为新打开的、加载的和关闭的文件触发事件，证明器管理器发出关于启动和关闭证明器的通知，证明文档有一个详细的用户和证明器访问模型（第4.5节），等等。在这种情况下，中心指导方针是让组件根据自己的规范定义它们支持的事件，而不考虑通知的可能接收者基于事件的设计产生了几个好处：软件变得可测试，因为定义事件的组件可以独立于应用程序中的上下文接收事件而使用。在另一个方向上，可以通过直接在单元测试中生成事件来测试事件的接收者。然后，可测试性实现了可更改性和可维护性，就像以前一样。基于事件的设计的另一个贡献是它在支持可扩展性方面的作用，如下所述。4.4启用可扩展性I3 P采用了为面向对象框架[25]和I接口模式[29]开发的概念，这可以被视为框架要点的简明总结，以实现可扩展性。 在这些方法中，框架是一个平台，它提供了一系列软件产品通用的机制。特定应用程序是作为该平台的扩展创建的。框架及其扩展之间的接口是以基于事件的方式定义的：框架指定了一些抽象状态，例如4.1节中的文件资源或证明文档。它还将事件定义为该状态的变化，并通知有关它们的感兴趣的扩展。可扩展性的先决条件是编程平台支持某种形式的运行时可扩展模块，这些模块可以以定义良好的方式进行交互。Netbeans平台[12]是I3P的基础，它提供了一个特别轻量级的模块系统.模块可以将普通的Java对象放入中央系统文件系统。然后，其他模块可以通过几行代码从系统文件系统中检索这些对象，并直接与它们交互。因此，提供扩展点就像在文件系统中指定扩展对象必须存放的路径，并定义这些对象所期望的接口一样简单。每当后来提到扩展点时，都会采用这种机制。因此，可扩展性本身是以一种可跟踪的方式实现的：图3中的所有组件都定义了事件模型，从而实现了组件级的可扩展性。超出10H. Gast/Electronic Notes in Theoretical Computer Science 285（2012）3即，中央事件调度器从系统文件系统中的事件的子文件夹中检索感兴趣的事件接收器因此，它反映了一个框架的概念，该框架定义了一个由特定于应用程序的扩展使用的全局事件模型最后，我们强调，如第3节所述，I3P的核心功能也采用了这些扩展机制来实现。因此，这些机制已经在实际场景中得到了验证，它们不仅仅是在开发的后期阶段进行评估的设计思想4.5证明文件可跟踪性要求建议的解决方案的概念元素映射到设计和实现中这一原则的一个中心例子是在I3 P中对证明文档的处理。下图描述了所采用的模型：证明文档是一个普通的文本文档，它被划分为一系列命令，这样每个命令都可以单独发送到证明器命令附加了一组插槽，这些插槽将任意数据与命令有效地关联起来。插槽解决了扩展性问题，因为其他模块可以注册新类型的插槽并以类型安全的方式访问它们。例如，prover驱动程序通常希望用命令存储私有信息，而theory explorer（第4.1节）将文档的树结构存放在另一个槽中。插槽支持事件驱动的设计，从而通过通用的插槽更改事件实现其所描述的好处其中一个插槽是命令状态，它对证明器对命令的处理进行如[20]中所述，状态区分空闲命令（可以由用户编辑）和已发送命令（已经发送到证明器）。处理本身被进一步划分为排队、正在处理和完成的子状态，这些子状态又被划分为成功和错误。命令状态还包含了在处理过程中由证明器生成的消息序列（参见4.6节）。当UI想要执行或撤销某些命令时，将其状态设置为发送或撤销就足够了[20]，这简化了UI级功能的实现和添加。I3 P定义了一种一致的轻量级机制，用于维护文档到命令的系统中的证明文档通知结构化任务关于发生的文本更改，以及它们发生的命令结构化任务在单独的线程中运行它委托处理H. Gast/Electronic Notes in Theoretical Computer Science 285（2012）311发送到与每个证明文档相关联的结构维护器。维护者负责更新命令分区。由于它只能分割和连接命令，因此命令总是形成分区。为了决定更改，结构维护者可以访问整个证明文档，例如在一次运行中处理注释或检查相邻的命令。在一个单独的线程中执行结构维护器允许它花费任意数量的处理时间，而不会停止用户界面。与早期的即时反应方法相比，这个决定降低了维护者的复杂性[20]但是，用户和结构维护者现在并发地访问文档，这需要适当的I3P通过文档镜像生成通用解决方案.镜像收集文档中的文本编辑，并相应地翻译结构化任务访问的任何位置。如果检测到与编辑冲突，则重新启动维护程序1证明文档是I3 P中事件的主要来源：结构修改和状态更改被报告给已注册的证明文档监听器;结构监听器和状态监听器接收各自的子集。当然，这个基于事件的设计的特殊例子产生了4.3节中讨论的一般好处。此外，证明文档发送的通知已被证明足以实现与所有其他组件的连接，包括整个UI层和证明器（第4.6节）。此外，使这些事件可用可以通过显示命令状态的UI组件实现可扩展性。4.6验证器交互一个主要的设计考虑是证明器和接口之间的预期交互，以及它们之间功能的相对分布。一种可能的观点是，证明器基本上可以执行和撤销命令[2，24]，并且可以相应地参数化接口。更进一步，可以探索在没有证明器支持的情况下，接口可以实现多少有用的功能[19]。这些方法无意针对证明器的进一步能力。另一方面，I3P从一个前提出发，即接口的主要作用是使证明程序中存在的功能对用户可用。因此，I3 P中心链接点是prover驱动程序，它创建一个prover实例1当结构化任务的变更通知异步发送并排队时，文档镜像的变更通知必须同步发送，同时编辑器持有文档锁。否则，结构化任务可能会在镜像接收到更新之前在错误的位置获得锁和访问文本。12H. Gast/Electronic Notes in Theoretical Computer Science 285（2012）3当校准仪启动时（第4.1节）。prover实例封装任何通信，特别是使用的协议。这允许驱动程序以特定于prover的方式访问特殊和新功能I3P所做的主要但非常薄弱的假设是，通信是基于消息的，即证明器实例发送命令并接收消息作为回报。支持不同类型的消息，其中包括正常输出（例如目标），错误和警告消息以及调试和跟踪消息。这些都是模仿伊莎贝尔消息由消息文本和一组标记组成，这些标记可能指示不同类型的标识符。当然，驱动程序可以自由地使用内部消息来实现特殊功能，而不必将它们转发给I3P为了支持广泛的功能，I3 P定义了证明器功能的概念。特性被定义为证明器的特定功能的代表（参见PROXY[18]），它与后台的证明器通信以访问功能。接口中的其他组件则可以通过简单地请求对应的特征来依赖于不同的证明器能力我们将现在使用当前Isabelle-2009-1驱动程序提供的功能进行演示。Executor功能表示在证明文档中执行命令。除了连接和断开执行器和框架的生命周期方法（参见C组件C配置器[29]）之外，它还允许证明器接收与证明文档（第4.5节）和编辑器中打开的文件（第4.1节）相关的所有事件。证明器实例可以自由地以任何适当的方式做出反应，通过更改命令由于基于事件的设计，UI层将通过突出显示和锁定理论编辑器中的命令来对这些状态更改做出反应。Isabelle-2009-1驱动程序模拟了传统的线性处理模型多理论支持。作为命令执行的补充，FileReporting功能在证明程序加载或释放文件时都会发出通知。文件资源组件（第4.1节）请求此功能，StructureMaintainer 特 性 是 一 个 用 于 附 加 到 证 明 文 档 的 结 构 维 护 器 的 FAcTORY[18]。如4.5节所述，这些维护者接收有关文本更改的事件，并重新检查命令以拆分和合并它们。Isabelle-2009-1驱动程序支持动态关键字识别，因此无需维护外部配置文件。ProofHierarchyClassification特性允许接口将命令分类为不同的类别（证明开始、证明结束、顶级等）。例如，这用于为理论浏览器重建树结构H. Gast/Electronic Notes in Theoretical Computer Science 285（2012）313并在理论编辑器中调用命令（第4.1节）。DynamicKeywords功能允许访问所有当前定义的关键字及其隔离分类。理论的语法突出显示（第3节）使用此功能来相应地调整演示。RuntimeOptions功能定义了运行时选项和操作员代理对象的层次分组，以方便地设置选项值。它可以通过本地选项和选项对话框访问（第3节）。这些功能演示了如何在接口中表示特定的prover功能，而无需固定协议。它是可扩展性的基石：当Isabelle获得用户应该可以访问的新功能时，prover定义并提供一个新功能，然后由合适的UI层扩展请求。与此同时，可测试性也得到了增强，因为单元测试可以单独为每个特性I 3 P也可以通过新的驱动程序进行扩展，因为证明程序管理器从系统文件系统的Drivers目录中检索安装的驱动程序（第4.4节）。类似地，安装管理器（第3节）在Installations目录中查找安装类型。因此，驱动程序和安装类型都可以由独立于I3P核心开发的模块提供.5相关工作本文中讨论的工程考虑因素-除了可重用性之外- 在文献中还没有明确提到。因此，本节从我们的角度分析现有的用户界面。有趣的是，我们发现相关研究中的许多建筑决策原则上可以用来实现理想的非功能属性。Proof General项目[1]旨在证明器接口的可重用性。通过对Isabelle、Coq、LEGO、PhoX和其他几个实验驱动程序的支持，这个目标已经非常成功地实现了。调整接口的方法是定制约150个变量[2]，这些变量表征与证明器的通信。相比之下，I3 P并没有对证明协议的精确性质做出假设，而是允许证明驱动组件封装通信。与功能的概念（第4.6节）相结合，这种方法更灵活，因为可以实现不同的方式的证明交互和新的功能，除了撤销/重做的理论命令可以提供。此外，I3P有趣的是，在Isabelle的情况下，编写I3P驱动程序和定制Proof General的工作量大致相同（大约3000行代码）PGKit框架[4]为证明器和显示组件提出了一个基于XML的通信协议。代理组件协调证明器和接口之间的通信，管理开放的证明文档，并同步用户编辑和证明器执行。这种架构的目标是可重用性，正如Proof General所做的那样，但也解决了新显示组件的可扩展性。14H. Gast/Electronic Notes in Theoretical Computer Science 285（2012）3但是，该协议不包含访问prover-specific功能的机制。此外，PGKit中的显示组件是重量级的，因为它们需要实现PGPIP协议，而I3 P UI扩展可以直接访问基础结构层中的对象。原则上，所定义的协议应该能够实现单个组件的可测试性，以及它所带来的属性和好处，但这在已发表的工作中没有讨论Charles和Kiniry [24]通过提供一个最小的接口来解决可重用性问题，该接口可以通过prover-plugins适应不同的prover它们的接口/证明器通信仅限于传统的命令撤销/重做，并且在广义上遵循Proof General/Emacs的适应模型[2]。没有机制在接口中公开特定于prover的功能。没有讨论基于文档的接口本身的架构，因此忽略了可跟踪性;如果在实现中遵循文档-视图分离，则可以为软件带来相应的好处。虽然证明器插件的清晰接口的定义使其具有独立的可测试性，但测试没有讨论。LuthandWol[27]考虑为Isa belle提供一个真正的图形界面的可重用性。它们的通用实现[27，§4.2]作为SML函子给出，集成到Isabelle堆映像中，可以为不同的逻辑和应用实例化。函子实现了文档-视图的分离（4.2节），但这个决定的潜在好处没有讨论。Kaliszyk [26]建议通过Web服务访问prover。虽然详细讨论了所采用的AJAX和DOM API的技术基础，具体的协议是私有的还是固定和公开的，目前还不清楚。在后一种情况下，将启用服务器组件的可测试性。此外，文档视图分离的好处，这是隐含在使用Web服务，也可以在这个系统中实现Bertot和T'ery[11]描述了一个通用的，可重用的方法来构建复杂的图形用户界面，包括点式验证机制。它们的呈现非常清楚地展示了文档-视图分离（特别是[11，§2.1，§3.1，§6.4]），并且可扩展性被确定为目标，尽管是通过数据配置通用机制的受限形式[11，§3.2，§4.3]。总之，在第2节中确定的证明器接口的目标已经在以前的各种研究中讨论过，尽管大多是隐含的然而，实现这些目标的方法总是来自特定的应用程序，而不是来自理想的质量属性和一般的软件工程原则，因此，应用这些原则的潜在进一步好处被忽视了。作为一个相对的贡献，本文因此显示了如何从软件工程的一般原则和策略可以应用到证明接口，以实现这些好处。6结论我们已经从工程的角度分析了构造证明器接口的任务：从证明器接口必须达到的一组目标开始，H. Gast/Electronic Notes in Theoretical Computer Science 285（2012）315已确定界面软件应具备的相关质量属性或非功能属性。其中，可维护性和可更改性可能是实际开发中最紧迫的问题，而可重用性和可扩展性则解决了如何在投入之后获得最大收益的问题。然后，我们已经证明，这些属性可以实现的用户界面软件的例子中的I3 P，一个新开发的界面Isabelle。基于文档-视图分离和基于事件的设计原则，I3P因此，本文讨论了与任何严重的证明器接口的开发然而，我们对相关工作的概述表明，对工程问题的考虑也可能导致其他接口的引用[1] 阿斯皮纳尔，D.，Proof General：一种用于证明开发的通用工具，收录于：系统构建和分析的工具和算法（TACAS[2] 阿斯皮纳尔，D.和T.Kleymann，AdaptingProofGeneral，http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral/doc/PG-adapting.pdf（2008）.[3] Aspinall，D.，C. Lu′th和A. Fayyaz，ProofGeneralinEclipse：Systemandar chitecturreoverview，in：2006年，OOPSLA 2006上的Eclipse技术交流研讨会。[4] A spinall，D.， C. Lu′th 和D. Winterstein ， Aframeworkforinter ractivep roof， in ：Calculemus'07/MKM'07：Proceedingsofthe14thsymposiumonTowardsMechanicalMathematicalAssistants（2007），pp. 161-175.[5] Aspinall ，D.， C. Lu 和B. Wolf， Assist edp roofd ojournal authoring ， in ：Mathematic alKnow wledgeManagement 2005（MKM '05），number 3863 in Springer LNAI，2005，pp. 65比80[6] Bass，Clements和Kazman，[7] Beck，K.，“Extreme Programming Explained: Embrace Change,” Addison-Wesley Longman,[8] Bertot，Y.，CtCoq系统：设计和架构，计算的形式方面11（1999），pp。225-243[9] Bertot，Y.，G. Kahn和L. 这是一个很好的机会，我想我可以在这里找到你。 Hagi ya和J. C. 妈的，编辑们，Theoretical Aspects of Computer Software，No. 789 in LNCS（1994），pp. 141-160[10] Bertot，Y.，T. Kleymann-Schreiber和D.Sequeira，实现无结构编辑器的指向证明，技术报告ECS-LFCS-97-368，爱丁堡大学计算机科学系（1997）。[11] Bertot ，Y.和L. 这 是一个通用的应用程序，为用户构建 用户 界面 ， J。 Sym BolicComputation 25（1998），pp. 161-194.[12] Boudreau，T.，Tulach和G. Wielenga，[13] 伯蒂湖， A. 请求和J. - L. Lanet，Java applet correctness：A developer-oriented approach，in：K. Araki，S.Gnesi和D.Mandrioli，editors，FME，LNCS2805（2003），pp.422-439[14] Buschmann，F.，R. Meunier，H. Rohnert，P. Sommerlad和M. Stal，16H. Gast/Electronic Notes in Theoretical Computer Science 285（2012）3[15] Chalin，P.，P. R. James和G. Karabotsos，JML4：Towards an industrial grade IVE for Java andnext generation research platform for JML. Shankar和J. Woodcock，编辑，VSTTE，计算机科学讲义5295（2008），pp.70比83[16] Dietrich ， D. ， E. Schulz 和 M.Wagner ， Authoring verified documents by interactive proofconstruction and verification in text-editors ， in ： Intelligent Computer Mathematics ， LNAI5144（2008），pp.398-414[17] Fowler，M.，[18] 伽马，E.，R.赫尔姆河Johnson和J. Vlissides，[19] 加斯特，H.，一个可扩展的Click'n Prove接口的体系结构Schneider和J. Brandt，编辑，高阶逻辑中的定理证明：新兴趋势论文集，364/07，凯撒斯特恩大学计算机科学系，2007年。[20] 加 斯 特 ， H.，Managing proof documents for asynchronous processing ， in： User Interfaces forTheorem Provers（MIPs 2008），ENTCS226（2009），pp. 49比66[21] 加斯特，H.， I3P网页，www-pu.informatik.uni-tuebingen.de/i3p（2010）。[22] Gneiting，A.，“I 3 P/Eclipse”，硕士论文，威廉-S c hi c k ard-Institut，图宾根大学（2010年）。[23] Hane b e rg，D.，S. Büaumler，M. Balser，H. Grand y，F. 奥特迈尔，W. 赖夫湾 S chellhorn，J.SCHmitt和K. Stenzel，KIV验证系统的用户界面-系统描述，在：定理证明器研讨会用户界面会议记录（CUP2005），2005年。[24] J·查尔斯，J·K·，Eclipse的轻量级定理证明器接口，见：User Interfaces for Theorem Proving，2008。[25] 约翰逊河，巴西-地E、组件，框架，模式（扩展抽象），在：1997年软件可重用性研讨会论文集（1997年），pp。10-17[26] Kaliszyk，C.，Web interfaces for proof assistants，in：Proceedings of the 7th Workshop on UserInterfaces for Theorem Provers（CUP 2006），ENTCS174（2007），pp.87比107[27] Luth， C.和 B. Wol ， Functionaldesignandimplementationofgraphicaluserinterfacesfortheoremprovers ，Journal of Functional Programming19（1999），pp.167比189[28] 马丁河，巴西-地C.的方法，[29] Schmidt，D.，M. Stal，H.Rohnert和F.Buschmann，[30] Shneiderman ， B. ， “DesigningtheUserInterface:StrategiesforEffectiveHuman-ComputerInteraction,” Addison-Wesley, 1998, 3rd[31] L.，Y. Bertot和G. Kahn，Realtheo remp roverdeservesrealuser interfaces，in：Proceedin gsof the fifthACM SIGSOFT symposium on software development environments，1992，pp. 120-129.[32] Wagner，M.，S. Autexier和C.Benz müller，PlatΩ：一个由文本编辑器和辅助系统程序员组成的编辑器，在：第七届定理证明器用户界面研讨会论文集（PARP 2006），ENTCS 174（2）（2007），pp. 87比107[33] Wenzel，M.，个人交流