交互式定理证明器用户界面的功能和实用性

理论计算机科学电子笔记103（2004）81-103www.elsevier.com/locate/entcs形式化用户综合数学环境Joseph R. Kiniry1奈梅亨大学Toernooiveld 16525 EDNijmegen荷兰摘要本文介绍了交互式定理证明器的几个用户界面功能。这些功能中的许多都模仿了现代交互中已经存在的功能，并且具有很大的实用性。动态开发环境（IDE）。一个正式的用户上下文的理论模型。 此模型用于形式化地描述的特点。提供的功能包括浏览器的基本数学结构（声明，理论，类型，证明等），快速访问结构定义和使用（快捷工具条、菜单或隐式超链接）、内置上下文帮助、上下文和类型感知的完成和视觉表示（扩展和折叠规范、证明项和序列的结构化元素）、语言元素的图形表示以及用户可扩展的、类型感知的漂亮打印机。基于正式模型的界面设计的研究机会也被识别和讨论。这些特性已经作为概念验证添加到PVS定理证明器中，并将在其下一个主要版本中提供关键词：交互式定理证明器，交互式开发环境，PVS定理证明器。1介绍现代流行的定理证明器的用户界面（UI）提供了编写规范和执行证明所需的所有核心功能Un-1电子邮件：kiniry@cs.kun.nl1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.09.01582J.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-令人惊讶的是，这些功能大多集中在数学，而不是数学家。近年来，证明者尝试的理论和规范的复杂性急剧上升。例如，像Java这样的编程语言的形式语义已经在几个证明器中指定[2]。在这些文章[9]中的一个（作者对此也有贡献）中，证明脚本长达数万行，并且已经编写了数百种策略来证明成千上万的定理相比之下，只有最先进的定理证明器UI提供近似于十多年前的基本编程环境的特征，例如，例如符号完成、语法突出显示和基本文档查找等功能。因此，定理证明器的用户，特别是那些同时也是程序员的用户，现在要求现代集成开发环境（IDE）的许多功能，特别是那些有助于管理复杂软件系统的功能。在高级编程环境中处理复杂性的通用概念和技术设施，如C++和Java编程语言，也适用于现代定理证明器的UI 为此，本文讨论了一些初步的工作，在改善用户界面的PVS，高阶定理证明器可从SRI，通过增加这样的设施。为了正式和一般地表示本文讨论的UI功能，并作为这项工作的主要贡献，提出了一个称为语义上下文的新概念的定义和说明。为了清楚地区分技术，我们在下面将具有第一类语义上下文概念的交互式定理证明器（ITP）称为交互式数学环境（IME）。1.1语义语境语义语境背后的一般概念首先由Chandy [？1996年，在C4I应用领域，主要用于军事和刑事用途，SIS响应管理系统2.然后，用户或应用程序的语义上下文被称为信息圈。信息圈是关于一个代理的信息集-一个人，计算机系统，公司，软件等。任何与外部事件相互作用并作出反应的实体。信息构成一个信息圈，其组成部分是数据和流程，即被动和主动要素。2C4I是Command and Control，Communications，Computers，and Intelligence的J.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-83一个信息圈是上下文相关的，因为信息的焦点是信息圈的中心：它的所有者，代理人。在军事C4I环境中，代理是，例如，将军战舰或坦克他们的信息圈有一些共同的特征：位置、部署、通信等。其他组成部分非常不同;将军与之互动的代理人与战舰与之互动的代理人不同。或坦克相互作用。关于具体规定信息圈的内容，有各种各样的建议大多数是相当特别的，比如文本和XML文档，因此几乎没有正式的语义。因此，人们可以正式推理信息圈的手段很少。由于这项工作的目标是在正式系统中指定信息圈的含义和用途，因此（a）为信息圈提出一个数学模型，并（b）将此模型称为新模型，以将其与其非正式表亲区分开来。信息圈的形式化模型被称为语义上下文，因为正如前面所讨论的，它是上下文相关的，而且，由于它的形式化本质被强调，它具有语义。语义语境理论是用一种称为类理论的形式方法来具体化的[11，12，13]。1.1.1类理论Kind理论用于描述协作环境中可重用构件的语义。在这项工作的上下文中，工件是证明脚本和证明的子组件，而这些子组件又是变量和函数等数学概念的实例。语义上下文的理论形式化，以及这里讨论的UI特性，部分地遵循证明脚本语言的语法使用Kind理论是因为编写数学规范并证明其性质的过程几乎完全是知识重用的过程。例如，导入由其他用户编写和证明的预先存在的定义和理论是知识重用的行为。由于kind理论语义语境的形式化仅依赖于类理论的三个基本这些运算符的初始语义非常简单，可以用集合论和序列来解释。为了避免读者沉浸在一个新的，不熟悉的形式主义，这些更熟悉的领域将在本文中使用。实际的语义是用类理论来具体化的，而不是这些84J.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-更简单的基础，因为它为4.3节中讨论的未来工作提供了基础。有兴趣了解更丰富语义的读者应该看看新的PVS版本和前面提到的论文[12]。1.2PVS中语义上下文的实现为了在现代证明器中实现这一新概念，以便为UI设计提供测试平台，PVS UI已经得到了增强：基于Emacs的前端添加了完整PVS语言的内置词法分析器和解析器。这个基础设施表示高级PVS结构，如声明、理论、类型和证明，以一种通用的语法方式反映证明脚本的理论结构。这种通用的表示被广泛的工具所使用，这些工具以前只对通过这种基于解析器的方法提供的新功能包括构造浏览器、通过快捷工具条、菜单或隐式超链接快速访问构造定义、上下文帮助以及上下文和类型。意识的完成。PVS UI和证明器本身也添加了其他新的非解析器中心功能。首先，添加了可视化扩展和折叠规范和序列的结构化元素的功能。其次，语言元素可以用图形而不是文本来表示，但对剪切和粘贴术语的能力几乎没有影响。最后，一个用户可扩展的，类型感知的漂亮打印机已被添加到PVS证明器。1.3相关工作其他环境提供了本文中讨论的一些功能。没有一个环境具有所有这些特性，也很少有正式的基础开发，也没有任何使用集成的解析器或证明器1.3.1数学环境一些数学环境提供交互式UI。大多数定理证明环境都来自于一个显然，更多的精力花在了数学而不是视觉基础设施上直到最近，随着ProofGeneral [4]的日益普及，接口只不过是美化的命令行[21]。Proof General和PVS被认为是使用最广泛的环境，具有最先进的UI。两者都使用Emacs作为前端，所以他们J.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-85权力只是这种选择的副作用。像语法突出显示、补全和超文本文档这样的特性就是这种令人愉快的副作用的例子. Proof General和PVS都没有下面讨论的功能。一些定理证明环境，如Jape和CtCoq已经被用作UI/HCI测试床[6，7，21]。许多最初在专用环境中引入的创新现在已经进入通用前端。 例如，Centaur和CtCoq中的逐点校对现在可以在ProofGeneral中使用，并且CtCoq基于PPML的布局和漂亮的打印设施在某些工作中部分功能再现。Pcoq是Coq的一个基于Java的用户界面[3]。它具有这项工作的一些功能，包括丰富的图形界面和结构化的编辑和演示机制。特别是，丰富的表示能力是基于证明结构的内部形式化表示。不幸的是，虽然Pcoq遵循了[25]中提出的高尚模型，但它并没有进化，因为它没有用作Coq的UIIsaWin是另一个具有一些高级交互功能的环境[20]。IsaWin从这项工作中受益，因为它专注于用拖放交互式隐喻对数学结构进行图标化的图形表示与大多数图标语言一样，缩放非平凡工件的图形表示存在一些问题。一些商业通用计算环境，特别是像Mathematica、Maple和Matlab这样的优质商业环境，具有丰富的UI。这些工具提供了所见即所得的界面，使用数学字体，并提供了直接编辑的条款与点击，拖放用户界面。虽然这里的意图不是试图复制这样的UI，但它们的视觉特性是引人注目和鼓舞人心的，但它们的编辑特性和可扩展性实际上不如上面提到的那些复杂的环境。将Mathematica这样的高级UI耦合到PVS这样的证明器是一个有趣的实验[1]。但是，由于这两种工具都不是设计为可重用组件，因此这种耦合是很笨拙的。相反，在这项工作中，这些商业数学环境进行了研究，并发现，在日常工作中最有用的方法被定理证明器采用、调整和形式化。86J.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-1.3.2编程环境与定理证明环境相反，现代编程环境提供了大量丰富的UI功能3。不特定于传统非数学编程的常见功能包括代码浏览、自动代码和文档格式化、类型感知和基于模板的完成、一般项目管理和集成帮助、API文档、过程跟踪以及对版本控制系统的支持本文的主要元主张是，每一个新的IDE UI功能，在主流编程社区中取得了一定的成功后，都应该被评估为定理证明UI的潜在补充。这项工作是这种评估的初步结果，主要侧重于帮助用户处理介绍中提到的巨大证明环境的功能。下一节详细描述了语义上下文的形式化模型. 续篇重点介绍了在IDE中被广泛采用的UI元素，这些元素在处理大规模编程的复杂性问题时非常有用。论文的平衡部分讨论了PVS如何被扩展以测试这些想法，并总结了定理证明器UI设计中的一些研究机会。2理论基础类理论有六个基本算子：继承、包含、合成、解释、规范化和实现，但我们只需要其中的三个。2.1基础运营商继承，写为涉及继承的逻辑规则规定：（a）所有工件（类或对象）都有一个父级，（b）如果两个工件之间存在继承关系，则描述它们3一些被评估的工具，以及从中借鉴的想法，包括Borland的jBuilder和Together Studio、Eclipse 、 Ei Studio 、 IntelliJ IDEA 、 jEdit 、 Metrowerks CodeWarrior 、 NetBeans 、Oracle9i JDeveloper、Sun ONE Studio和各种“Visual*”工具（即，微软的VisualStudio，IBM的VisualAge，WebGain的VisualCa）。J.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-87⊃⊗⊕也存在差异4。包含，写作““，读作“has-a”，是一种包含关系，因此也是工件之间的一种反应性、传递性、非对称关系，即成对的种类或成对的对象。包含规则指出，分类器的子结构由分类对象的子结构保持更具体地说，如果一个类K有一个子结构类L（写作最后，组合有两种基本形式：将工件分解为其子组件的能力，写为““，以及从现有子组件创建新工件的逆操作符，写为““。各种逻辑规则将组合关系与其他关系联系起来，特别是继承和包含，但这些规则对本文的讨论并不重要。为了这项工作的目的，人们可以将继承看作是类类型结构的有限格，将包含看作是集合论包含，将组合看作是文本连接（即，文档是通过链接组成的文本子元素的序列）。2.2语法结构为了形式化地表示IME的语义上下文，它的证明脚本语言必须用kind理论进行分类本节中识别的所有分类器的集合称为IME的类上下文由于大多数形式语言都有（E）BNF描述，因此可以使用一个简单的算法来帮助执行基本的分类步骤：• 规范化BNF，注意所有无选择的规则，这些规则通常用于为人类读者阐明语法例如，规则的规则1：：=规则2规则2：：=.等等应予以注意规则1：=.等等• 识别在证明脚本语言中定义特定独立概念的每个规则。为每一个这样的概念创建一个新的种类，让唯一的规则定义每一种。下面我们将对这些定义进行更多的说明。例如，PVS的顶级概念，直接从PVS证明语言4 这个描述对这项工作并不重要，但简而言之，它是两个（总）功能：一种是将父对象转换为逻辑上健全和完整的子对象，另一种是将子对象转换为容易遗忘但相对于父对象的上下文而言健全和完整的父对象88J.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-感应⊗递归递归≡⊕指导，是理论和数据。PVS的第二层概念在语法中更深一层，它们正是用来定义顶层概念的那些概念。它们是：理论形式，理论之间的输入和输出关系，假设，声明，判断和转换。如果在多个级别上看到一个结构，则最顶层是分类的适当位置。例如，在PVS理论中，数据库可以被定义为截至目前，该等已识别分类者之间并无任何关系。• 现在，通过挑选出表现出分类模式的BNF规则来识别所有的继承关系。这种模式在BNF中有两种主要形式，选言选择和名称相似性。选言选择表明父类是其子类的选言组合（““关系）。例如，PVS中的声明分为九个子类别，正如语法和语言参考所强调的那样：库，缩写，类型，变量，常量，函数，公式和字段。因此，这九个种类都是表示声明的种类的子种类，并且声明父类可以分解为它的子种类之一功能正常感应共归纳余递归的Fig. 1. PVS函数是一个层次结构PVS函数分为三个子类别：归纳，递归，既不是归纳也不是递归，其中前两个不是互斥的，因为函数可以是归纳和递归的。归纳法和递归法都可以分为两类，因为上归纳和上递归的对偶概念因此，这些概念在两级分类层次中定义了八种，如图1所示。高级概念有时使用组合根据低级概念来定义。因此，IINDUCTIONIINDUCTIVE COINDUCTIVE意味着一个归纳函数要么是归纳的，要么是共归 纳 的 ， 但 不 能 同 时 是 两 者 。同 样 地 ， 函 数 f（IINDUCTIONfRECURSION）fNNORMAL5这是用于为领域定义本体或元模型的基本过程。 因此，如果所讨论的语言已经定义了这两个定义中的任何一个，那么简单地采用该定义。J.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-89声明函数要么是• 为了推广一个经典的、数学上通用的语义上下文观点，也就是说，脱离所讨论的证明脚本语言的术语，所有核心结构也应该使用[12]中描述的标准数学概念来分类。这允许不熟悉IME方言的用户仍然使用其基于分类的首选项系统，如下所述。• 接下来，通过查找展示包含关系的BNF规则来一般来说，顶部-层次概念具有明确指示子结构的单一注意规则。例如，PVS BNF中描述理论顶层概念的规则是Theory：：= id [TheoryFormals][导出][AssumingPart][TheoryPart]这条规则清楚地表明，一个理论类有五个子结构：一个名称（id标签）、一个理论形式、一个导出子句、一个假设部分和一个理论部分。请注意，这些子规则的名称甚至表明了它们的结构关系（从这个角度分析语法将产生整个语言的包含层次结构。该层次结构将用于本文稍后讨论的几个特性，因此是语义上下文的关键特性。• 最后，通过检查BNF规则的强制文本排序来识别组合子结构。PVS理论的上述规则表明了这样一种强制性规则：导出子句必须在假设之前，而假设又必须在理论部分之前。因此，理论被定义为一个序列名称理论，F标准理论，EX pORTING CLAUSE， ASUMMING PART， PART理论其中逗号运算符（语法中标识的文字序列也是构成子结构的例子。例如，PVS BNF规则TheoryName：：= TheoryName++'，'表示分类器理论名称由逗号分隔的[6]逗号运算符在理论上被定义为复合运算符，因为序列可以用显而易见的方式构造和解构90J.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-理论名称的序列这些序列也用于本文档稍后讨论的许多功能。2.3按类别划分的上一节中定义的分类层次结构主要由UI用于定义基于语义上下文的首选项设置。每个概念都可以在每个UI功能的基础上启用或禁用。如果一个概念被禁用，那么它的所有子概念（在is-a层次结构中位于它之下的概念）也被禁用。使用这样的方案，用户可以直观地向系统描述哪些概念适合于每个UI界面，但是在不知不觉中以正式的方式这样做。例如，如果PVS证明脚本文档将在树视图中被汇总，并且用户仅对理论中做出的假设感兴趣，则启用ASUMPTION构造，并且禁用is-a层级内的所有其他兄弟概念。2.4通过包含和组合进行包含/包容和组合/序列关系通常用于在接下来几页中讨论的各种UI特性中进行迭代。记忆反向嵌套迭代函数是许多UI特性中使用的关键操作符。从本质上讲，必须按照上下文中的实例序列向后移动，每次到达序列的末尾时，都要向上移动到封闭的上下文，但决不能两次返回同一个实例考虑PVS代码的这个片段：存在1 [T：TYPE]：理论开始x，y：VAR 不p，q：VARpred[T]独一无二？(p)：bool = FORALL x，y：p（x）AND p（y）隐含（*）...假设用户反向嵌套的next对象的顺序是什么？序列为：y，x，bool，p，unique？，q，T，存在1.第一个元素是y，因为它是FORALLquantifier实例的封闭序列中的最后一项。变量x跟在后面，因为它是同一级别的前一个实例。此时，当前级别的序列到期，因此我们向上移动一个级别到常量声明实例。在此级别的顺序子结构中只有三个实例：J.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-91独一无二？，p，bool.它们是反向迭代的。当该序列到期时，遵循下一个封闭序列：x，y，p，q，但是由于x、y和p都已经被选择，所以只能返回q。最后，最外层封闭序列的元素存在1，T返回以相反的顺序。这种通用迭代在PVS上下文中是合法的，因为PVS是高阶证明器，因此可以直接引用公式和理论等高阶结构。对于非高阶证明器，初始启用的分类器集可能会更小。本文后面讨论的特性进一步细化了这个迭代算子。例如，类型感知完成使用此迭代来选择要呈现以完成的预期术语，但仅在术语在给定上下文中类型化时才向用户显示每个选择。2.5识别用户用户的语义上下文是由前一部分的过程所识别的底层种类上下文、通过解析文档并识别与所有实例相关联的概念所确定的所有相关联文档的实例以及用户的当前焦点的位置的组合。由使用2.2节的过程识别的所有种类组成的集合是IME的底层种类上下文这个集合对于给定的证明脚本语言和IME组合是固定的一个用户。用户在IME中加载的所有文档都必须进行解析，以识别当前语义上下文中的所有实例。IME的后端证明程序中显然存在解析器，但通常情况下，不存在用于访问此信息的已发布API。因此，许多IME将使用某种类型的前端解析器，如第4节所讨论的。解析器识别的每个结构都有一个起点和一个终点。此范围信息用于通过标识IME内哪个结构包围当前焦点来如果当前点不在任何实例的范围内，则向后移动通过当前文档的最近实例将被视为封闭实例。总的来说，用户的语义上下文是证明者的固定上下文和动态上下文的联合，动态上下文有两个部分：（1）当前使用的所有证明脚本的内容，以及（2）用户注意力的当前焦点92J.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-在下一节中，将讨论利用语义上下文的各种UI工具。3基于语义上下文的UI工具PVS中已经添加了超过六个新功能，它们利用了用户上下文的形式化。虽然这些新设施主要是有益的PVS用户挣扎与非常大的形式化和证明，我们发现，他们也有重大的实用工具，以日常的PVS用户。3.1结构浏览程序员在大规模开发工作中使用的主要接口是某种功能浏览器。浏览器允许用户快速导航结构化信息空间。有多种UI可供选择，用于呈现分层结构化的信息，其中最流行的是菜单、树和窗格。这些备选方案中的每一个都呈现用户的语义上下文的分层包含关系“类”。3.1.1基于菜单的浏览基于菜单的浏览是浏览中小型结构化信息空间的流行方式。这种方法的局限性，例如，存在多个嵌套层，每个层有多个项目等，是众所周知的，而且经常被滥用。因此，菜单PVS用户现在可以使用Emacs的自定义特性，根据其分类类型，指定默认情况下，所有结构都显示在一个分层菜单中，按理论组织。3.1.2层次化快捷方式第二种流行的方式是层次化快捷方式，通常呈现为树来呈现结构化的信息。像Windows和OS X中的文件浏览器就是这样的工具的例子，像VisualStudio和Apple的Xcode这样的IDE层次结构可以以集成或独立（从主显示）的方式呈现。当通过鼠标单击或按键激活摘要树中的构造时，当前buffer中的光标将跳转到J.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-93主窗口中的相应元素。用户可以自定义在以类为中心的基础上在层次结构中总结哪些PVS构造。3.2查找定义扩展隐式超链接是商业开发环境中的一个新特性。例如，Emacs或Microsoft Word中的自动拼写检查功能就是隐式超链接的一个例子。在这样的环境中，源文档（可能是研究论文）直接超链接到一个或多个词典。这种特殊的超链接的目的是单词拼写纠正和定义以及同义词查找。一般来说，隐式超链接的动作可以是信息性的，例如运算符或变量的定义，也可以是纠正性的，例如，修改变量的拼写。在这项新工作之前，PVS支持几种隐式超链接。例如，在PVS中，使用移动的鼠标中键单击来显示在小信息窗口中显示的构造的类型声明。不幸的是，大多数高级功能，如查找声明的使用位置，都不能作为隐式超链接使用，因此需要用户输入长而难记的键序列。通过增加识别的隐式超链接类型的数量，此功能得到了改进。现在可以激活PVS关键字，以显示其完整的定义相关和使用信息。此外，现在可以在PVS注释中使用各种隐式链接类型，包括URL、ISBN编号、嵌入式图像引用、RFC标题、文档交叉引用、邮件地址、各种编译器消息、路径名、大纲节点、手册页、键序列、目录条目、标记位置、参考书目引用和其他一些更深奥的类型。有几种隐式超链接对定理证明器特别有用：URL、嵌入式图像引用、文档交叉引用和键序列。URL对于引用相关论文或其他文档结构的源材料显然很有用。 嵌入式图像可用于显示特定术语、序列或证明结构的精美印刷版本。Info节点可用于交叉引用其他Emacs和PVS文档，特别是PVS发行说明，这是PVS文档中目前唯一使用Texinfo的部分。最后，嵌入的键序列可用于记录PVS UI行为并触发PVS操作这样，例如，PVS教程可以变得更具交互性和自动化。94J.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-3.3获得帮助上下文帮助是通过检查当前光标位置的封闭结构，并在用户可调的延迟（通常是几百毫秒）后显示有关该结构的额外信息来生成的在PVS中，帮助消息显示在用户界面底部的一个小区域中。其他环境通常也有类似的不显眼但始终可见的地方放置此类帮助信息。在新的PVS中，此功能用于记录语法语言结构（一种上下文感知的help-pvs-prover-commands）以及像布尔运算符，条件运算符等序言运算符的使用。3.4完成现代编程环境提供了更好的范围和类型感知完成。这些IDE在用户编辑时解析并检查输入文件的类型。当构造完成时（例如，类型、变量或方法名），则显示所有合法（类型正确且在当前范围内可见）的alter-natives的列表。不幸的是，由于PVS此时，当请求完成时，只显示那些在当前范围中可见并且可能是类型正确的构造。完成选项以由2.4节的算法，内部作用域中的匹配声明显示在外部作用域中的声明之前。3.5信息隐藏大纲用于显示和隐藏文档的各种子结构。PVS UI设计了大纲模式，其中子结构基于文档的包含层次结构进行标识结构是隐藏的，并通过修改鼠标动作显示，就像那些在文档查找中使用的，或通过键序列。一个隐藏的结构是用一个包含四个句点的省略的超文本区域（当被鼠标指针触摸时自动高亮显示）指示的。选择这种表示法是为了使其类似于PVS精美印刷今天所进行的省略，但又足够不同，很明显省略是由于轮廓7目前基于语义包的解析器前端不与PVS的类型检查器通信J.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-95M模式，而不是PVS本身。用鼠标指针长时间触摸隐藏的结构将暂时取消隐藏结构以进行检查。在具有隐藏区域的缓冲器上的增量搜索在隐藏文本中找到匹配，并且使这些匹配暂时可见。如果用户在这样的临时隐藏区域内退出搜索，则文本保持可见。3.6PVS中的精美印刷PVS UI中还添加了一个用户可扩展的、类型感知的漂亮打印机。PVS输入语法目前仅限于ASCII字符。这是相当严格的，但PVS允许操作符被重载，使用类型系统和理论层次来确定任何给定上下文中的操作符。重载是非常方便的，并且在数学中大量使用，因为上下文通常会清楚地说明所指的是哪个运算符。例如，PVS prelude仅针对插入符号操作符（“^“）就有四个声明漂亮地打印具体的PVS语法并不困难。PVS中的Pretty-printing是使用Common Lisp Pretty-Printing工具[24，Chapter 27]来处理的，该工具带有一组在CLOS中实现的方法，这些方法可以遍历PVS抽象项在扩展字符集中，如LATEX和UNICODE中可用的字符集，可用的运算符符号比ASCII中的要多得多。当这样的字符集可用时，最好将ASCII PVS运算符映射到替代字符集的输出运算符例如，我希望用e2来表示e^2（求幂），而Bn对于B^（m，n）（位向量提取）。然而，要正确翻译这些表格，语法是必需的（特别是类型和分辨率）。PVSLATEX打印机源自各种不同的性能。 它都有要进行的替换，并且通过使用解析信息，可以基于arity和声明运算符的理论来区分运算符。为了保持替换文件的简单性，目前没有使用类型8。其他方法可用于漂亮打印，当在PVS中嵌入不同的逻辑时特别有用例如，Skakkebaek [23]为持续时间演算生成了一个新的解析器，将其抽象语法映射到PVS抽象语法的子类。这些类中的大多数都使用了专门的方法，但是类型检查、证明等都要使用超类的方法这很好，但不容易定义一个8为了正确地提供对类型的支持，替换文件的某些部分需要 要进行类型检查，并且确定类型检查上下文并不简单96J.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-PVS9中的新语法。为持续时间演算定义一个新的语法并不太困难，因为它复制了大部分PVS语法，只是添加了一些新的运算符。另一个困难是，随着证明的发展，引入了部分PVS和部分持续时间演算的术语，尽管它们打印得很漂亮，但结果可能会让用户感到困惑在Pombo [22]中，PVS被用来提供Ag规范的语义，定义了一阶动态逻辑和分叉代数的语义，以及允许用户在Ag中推理的规则和策略。这里有定义的转换，比如一个意义函数，以及像克里普克结构的当前世界这样的参数在这种情况下，漂亮印刷应用的函数被修改，以抑制意义函数和世界论证。新的PVS漂亮的打印机是一个优雅的重新设计，可以用来完成上述所有，但在一个更简单，更连贯的方式。现在的pretty-printer允许用户在每种类型的基础上注册pretty-print函数每个函数接受一个术语和术语的类型作为参数。一个函数检查给定的术语是否需要特殊的漂亮打印处理，并在适当的情况下漂亮打印该术语。如果注册的函数都不适用，则使用默认的pretty-printer。预计将提供一些通用功能，使其易于执行常见任务，如抑制参数和识别其运算符是指定理论和类型的常数的应用程序。在它的全部通用性中，这些函数充当任何形式的术语的自定义漂亮打印的语义附件。这种方法适用于许多情况，但并不是所有漂亮的打印工具都可以集成到Common Lisp中。对于非基于Common Lisp的工具，需要提供解析和类型信息。解决这个问题最有希望的方法是提供PVS术语的抽象语法在XML中，大多数编程语言都有读取和操作XML文档的功能。例如，这在OMDOC中完成，它为PVS提供了一个扩展，可以从经过类型检查的PVS规范生成OMDOC抽象语法[14]。未来有计划生成直接反映PVS内部抽象语法的XML，这可以很容易地用于构建新的漂亮打印机。9PVS目前使用Ergo Parser Generator [15]，它有许多怪癖，使其难以使用。J.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-973.7图形表示最后，一些用户更喜欢他们的计算数学环境（语法上）与他们自己的非计算，笔和纸的数学方法非常相似。图二. 在PVS UIPVS用户界面现在能够使用扩展字符集。因此，我们的新PVSUI扩展为所有核心PVS操作此时，重载运算符的所有用法图2显示了PVS前奏的一部分，当使用符号呈现时。98J.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-4扩展PVS虽然在过去的几节中已经提到了PVS的各种新特性，但是关于如何实现语义上下文的底层功能以及新UI如何使用该功能的细节很少。本节将简要讨论当前实现的状态。图三. 集成PVS环境图3示出了新的集成环境10的示例配置。如图所示，集成PVS环境具有多个子组件。这里显示的是当前校样脚本的基于层次树的布局（窗口“W-0”的左上角主窗口显示正在编辑的当前校样脚本10细心的读者会注意到，屏幕截图是在运行操作系统的系统上制作的。X.这种选择的原因不仅仅是美学。 作者还致力于将PVS移植到各种开源Common Lisp实现中，因此我们目前在OS XJ.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-99显示的配置是作者这个集成环境是Emacs源代码浏览器Emacs Code Browser（ECB）的扩展。它显示一组用户可自定义的窗口，可用于浏览目录、文件和文件内容，所有这些都是当前语义上下文的子结构。在未来的左上角的摘要窗格也可以被拆分成一个单独的窗口。Speedbar包用于支持此功能[19]。如前所述，可以使用菜单（图中未显示第3.1.1节。它们是使用Imenu工具实现的，该工具内置于Emacs的最新版本中。这一特性提供了一种通过一组嵌套菜单按名称查找文件中最后，第3.2节中讨论的隐式超链接功能通过重用Hyperbole包的部分来实现[28]。4.1基本实现这项工作中最复杂的部分是将证明脚本中的构造映射到底层的面向对象表示。PVS语言的kind理论模型的底层表示是使用eieio实现的，eieio是Emacslisp（elisp）的CLOS实现[18]。模型的面向对象结构以自然的方式直接映射到CLOS对象。要实现映射功能，需要（a）为Emacs编写PVS特定的功能，或者（b）依赖于一个基于通用语言的框架，该框架允许使用基于该框架的现有和未来工具。为了节省时间，提高可靠性，并利用其他Emacs爱好者的辛勤工作，选择了选项（b）并且，在评估了Emacs可用的各种通用框架之后Emacs的语义包用于在elisp中构建词法分析器和解析器[17]。要在一种新语言中使用语义包，从而启用所有基于语义包的工具，必须编写该语言的语法规范。本质上，通过依赖于通用基础，PVS支持被“自动地”为所有依赖于语义包的工具启用语义包的核心包括一个词法分析器生成器和一个com-100J.R. Kiniry / Electronic Notes in Theoretical Computer Science 103（2004）81-piler编译器，或者在语义包的命名法中称为bovinator。核心工具是语义bovinator，它具有与GNUbison编译器编译器类似的功能[8]。语义包的最新版本（2003年中期）包括第二个编译器，称为wisent，它实际上是一个完整的GNUbison elisp实现。本文中描述的工作最初使用bovine框架，但现在使用wisent。功能的最后一部分，即使用扩展字符集呈现PVS证明脚本（如图2所示），是使用X-Symbol包[27]。4.2未来改进还有一些新的功能和改进需要添加到新的PVS UI中。首先，必须添加一个图形工具栏（如Proof General中提供的工具栏）来表示一些新功能。一些Emacs用户会简单地忽略新功能，直到他们有这样的功能，所以尽快添加这个简单的功能很重要。其次，目前wisent解析器不支持X-Symbol包，因为语法是用ASCII编写的。因此，用户当前可以具有其PVS证明脚本的符号表示，或者可以具有集成环境，但不能两者都具有。我们希望在新的PVS发布之前取消此限制。跟踪PVS理论之间的导入和导出关系是一项复杂且有时耗时的任务。一个新的语义包正在开发中，称为COGRE，可以图形化地表示语义包解析的结构[16]（最初，COGRE的重点是UML图）。在COGRE中，可以操纵图形表示来更改底层关联数据。因此，一些实验与理论关系的图形表示是必要的。最后，涉及参数化理论的UI操作很弱。改进对这种参数化子结构的完成和摘要的支持PVS理论的参数化很可能可以用这类理论复合算子来表征，因此第2节的方法可以继续使用。4.3研究机会许多当前流行的IDE最近都添加了重构功能-[10，26]。重构是改变系统实现的过程，以改善实现的某些方面，同时保持系统的稳定性。