没有合适的资源?快使用搜索试试~ 我知道了~
理论计算机科学电子笔记103(2004)3-26www.elsevier.com/locate/entcsProof General会见IsaWin结合基于文本和图形的用户界面大卫阿斯皮纳尔1英国爱丁堡大学信息学院LFCSChristophLüth2柏林大学数学与计算机科学系摘要我们描述的设计和原型实现的组合定理证明接口技术。一方面,我们从Proof General中获得了独立于证明者的交互语言的想法,以及在PG Kit中间件架构中提出的实现。 另一方面,我们从IsaWin中获得了一个复杂的图形隐喻,使用直接操作来开发证明。我们相信,由此产生的系统将提供一个强大的,强大的和通用的环境中开发的证明交互式证明助理,也开辟了研究和实施新的机制,管理交互式证明开发的方式。关键词:定理证明器,中间件,证明助手,交互式证明开发。1介绍Proof General是一个交互式证明助手的通用接口,构建在Emacs文本编辑器上[4,7]。近年来,它被证明是相当成功的,并且受到几个定理证明系统的用户的欢迎。其成功是由于它的通用性,允许特别容易适应各种证明(主要是,伊莎贝尔,科克和乐高),以及它的设计策略,其目标是专家以及新手用户。其核心特征是先进的1网址:http://homepages.inf.ed.ac.uk/da2网址:http://www.informatik.uni-bremen.de/~cxl1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi:10.1016/j.entcs.2004.09.0114D. 阿斯皮纳尔角Lüth/Electronic Notes in Theoretical Computer Science 103(2004)3版本脚本管理,与校对助手的文件处理紧密结合。这为处理大规模的证明开发提供了一个很好的工作模型,将它们与大规模的编程开发类似。Proof General还提供了对高级操作的支持,例如逐点证明,尽管这些操作不太受重视。然而,证明一般有一些缺点从用户的角度来看,尽管界面提供了一些高级操作,并试图隐藏shell窗口进程,但交互仍然牢固地基于编辑用证明助手的命令语言(通常是虽然有一些菜单项和工具栏按钮来帮助启动和完成证明,但很少有提示或模板来帮助构建编写证明脚本时使用的大量策略和声明。从开发人员IsaWin是Is-abelle的通用图形用户界面的实例化[24,23,25]。 它旨在提供一个抽象的用户界面,一个持久的可视化隐喻和直接操纵的概念。由于策略应用程序是自动生成的,用户可以不太关心证明器的语法特性,而是可以集中精力于证明的逻辑内容。这种抽象的方法也允许高层次的操作:例如,支持指向证明(折叠或展开方程),术语注释(系统可以显示子术语的类型)或战术编程(可以从证明的历史中剪切部分虽然IsaWin通常会得到最初的批准,特别是来自Theo- rem证明新手的批准,但它也有一些缺点。从用户从开发人员的角度来看连接到标准ML中未实现的证明器。因此,Proof General和IsaWin可以被认为是互补的,每个人都有自己的优势来弥补对方的缺点。 本文介绍了一种尝试,结合他们的优势,在一个系统的基础上,在PG Kit基础设施上,在[5,6]中介绍。由此产生的系统有一个基于事件的架构,并专注于管理证明脚本作为中央底层文物。一种通用的交互式协议语言允许连接不同的用户界面(称为显示器);因此,IsaWin成为一个D. 阿斯皮纳尔角Lüth/Electronic Notes in Theoretical Computer Science 103(2004)35用户界面在此设置。在本文的其余部分,我们描述了我们想要构建的Proof General和IsaWin的特定方面(第2和3节),然后是新系统的设计(第4节)和原型实现的描述(第5和6节)。最后,我们简要地提到了相关的工作,以及我们对该项目未来发展的愿景2证明一般基本概念Emacs Proof General是Proof General的化身,基于无处不在的Emacs文本编辑器。3对于Proof General,证明由用户可编辑的形式文本(或证明脚本)组成,当被机器处理时,它要么构造一个表示,要么检查形式系统中是否存在证明。目标验证脚本是开发的中心焦点。证明脚本是否包含策略风格的过程证明或声明性证明描述并不重要。该接口依赖于底层的证明助手能够在文本对话中以交互方式和增量方式处理证明脚本:用户发出证明命令,系统响应。在属于文本的正确的校对脚本命令和不正确的命令之间进行了区分。正确的命令包括要被证明的命题的陈述和它们的证明的内容。不正确的命令包括撤销步骤,检查术语和查询可用定理数据库的命令。正确的命令存储在校样脚本文件中,并根据校样的进度进行着色:重要的是,由校样助手处理的区域被着色为蓝色,不应编辑。这就是[12]中描述的脚本管理Proof General提供了一个简单的浏览隐喻,用于重播证明,通过工具栏在证明脚本中导航,请参见图1的屏幕截图。在幕后,这是通过发送命令来发布证明步骤和撤销证明步骤来实现的。撤销行为依赖于证明助手的内置历史,一旦证明完成,它通常会忘记证明步骤之间的历史,即只有整个证明可以撤销,而不是单个步骤。4撤销行为将证明脚本分割为多个区域3支持多种Emacs版本,包括XEmacs和GNU Emacs,可在多种平台上运行。4这对新用户来说一开始是违反直觉的,尽管他们很快就有了感觉。证明一般可以同样很好地与证明人,保持更多的历史。对于Proof General来说,也可以允许撤销到证明器中的任意位置的6D. 阿斯皮纳尔角Lüth/Electronic Notes in Theoretical Computer Science 103(2004)3Fig. 1. Proof General接口,默认配置。 该窗口分为两个窗格,底部显示的输出从证明助理,顶部显示的证明脚本,与背景颜色根据进展。(or跨度)的连续行,这是原子撤消。跨度在文件中被线性处理,尽管它们有一个依赖结构,表达了证明开发本身的依赖关系:可以在界面中显示这种依赖关系,例如突出证明定理时使用的辅助引理。Proof General提供了一个高级的脚本管理实现,可以在双向通信中同步校对助手和编辑器之间的文件编辑文件用于存储证明脚本,代表开发的一部分。如果用户完成处理一个证明脚本文件,Proof General会通知prover,如果prover在处理过程中读取另一个文件,它会通知ProofGeneral,对于文件级别的撤销操作也是如此从技术上讲,Proof General主要是用Emacs Lisp实现的,与其他Emacs包接口,特别是包括用于显示数学符号的X-Symbol [37]一个相当大的努力已经取得了使其易于适应一般证明新的证明助理,它是可能的,该设计缺点在于,与用户期望的“撤消”操作快速相反,执行重放可能花费任意量的时间D. 阿斯皮纳尔角Lüth/Electronic Notes in Theoretical Computer Science 103(2004)37通过设置少量变量来配置,很少或根本没有Emacs lisp编程。但这种机制是特设的:我们试图预测和迎合Proof General中许多不同的证明助手行为,假设证明助手本身不会被修改。这只适用于到目前为止:对于高级功能(例如逐点校对[11]和校对依赖性可视化[26,31]),不可避免地需要来自校对助理的专门支持。为了解决现有Proof General模型的局限性,特别是Emacs Lisp实现的局限性,Proof General(PG)Kit已经被设计出来[5,6]。其中心思想是使用连接到不同的证明者的经验来规定一个统一的交互协议。而不是繁琐地适应证明一般每个证明者,证明一般发号施令,通过强制一个统一的协议,交互式证明,称为PGIP,每个证明者必须支持。作为本文所述工作的一部分,我们已经实现了PG Kit的pro-totype版本。系统架构和PGIP协议的更多细节将在后面的第4.1节中描述。3IsaWin基本概念IsaWin是Isabelle证明助手的通用图形用户界面Gen- GUI的实例化。它基于记事本的视觉隐喻,为Isabelle(和相关的证明器)提供了一个更抽象、更少面向语法的接口[24]。所有感兴趣的对象,如证明,定理,策略,重写规则集等都通过记事本上的图标可视化,并使用鼠标手势进行操作。更复杂的对象,如证明,可以通过在单独的子窗口中打开它们来操作。IsaWin o提供自包含的历史支持、点校对、依赖管理和会话管理。该界面基于直接操作的概念:用有意义的视觉隐喻和增量的无语法操作连续表示感兴趣的对象和动作,即,用户手势,例如将对象放到另一个对象上、弹出菜单或鼠标点击。 对象通过记事本上的图标可视化(见图2)。图标由对象的类型给出,这决定了可用的操作。因此,当用户看到由定理图标可视化的对象时,他们知道如果他们将该对象放到另一个定理对象上,定理证明器将尝试通过前向解析来组合它们,而如果定理被放到正在进行的证明上,则将尝试使用该定理的后向解析的新证明步骤。对象的类型进一步决定了操作8D. 阿斯皮纳尔角Lüth/Electronic Notes in Theoretical Computer Science 103(2004)3图二. IsaWin接口。 主窗口在顶部显示记事本和文件夹导航栏,下面是正在进行的校对。这里打开两个辅助窗口,允许搜索定理,并显示证明的历史出现在其弹出菜单中,以及是否(以及如何)可以打开单独的子窗口。该接口还跟踪依赖关系,即,如果一个对象被用作构造另一个对象的参数, 更改或过时,所有依赖对象也会过时拖放是通过一个表来解决的,该表分别用拖放对象和接收对象的类型来索引。历史在内部表示为用于构造对象的操作序列。这有一些优点,因为它允许对证明进行抽象操作;例如,我们可以从证明脚本中删除一些部分,并将它们变成可重用的策略。但它也有严重的缺点:由于证明脚本是历史的外部表示,一般的脚本管理不是很容易实现,实际上IsaWin只提供有限的脚本管理,与Proof General相似。IsaWin有自己的格式来保存和读取证明,虽然它对以Isabelle的本地格式生成证明脚本的支持有限,但它不能解析它们。这使得很难在没有使用IsaWin开发的证明脚本上使用IsaWin,我们可以加载和重放它们而不操作包含的证明。从技术上讲,IsaWin是通用图形用户的实例化-D. 阿斯皮纳尔角Lüth/Electronic Notes in Theoretical Computer Science 103(2004)39GenGUI 与特定的 Isabelle 特定模块的接口。GenGUI 完全在标准ML(SML)中实现;要对其进行自定义(添加或更改图标、快捷按钮或菜单项),必须更改实例化模块。 为了使GenGUI适应另一个证明助手,实现了一个具有给定签名的不同模块,包含对象类型,操作和拖放表。这需要对签名(和SML)有很好的理解,并且还使得对未在SML中实现的证明器的适应变得很麻烦。对我们来说,GenGUI和IsaWin的经验表明,即使在相同的编程语言中,接口作为证明助手的附加组件的实现也会导致模块化程度较低的架构,这使得接口难以重用。这也使得接口的健壮性降低:如果证明器出现分歧或返回一个运行时错误,接口也会出现分歧或停止。由于这些原因 , GenGUI 没 有 太 多 不 同 的 适 应 性 , 并 且 与 Proof General 相 比 ,GenGUI没有完全实现其通用性的承诺。一个更好的架构是保持接口和证明助手的分离,并以一种独立于语言的方式清晰地指定它们的交互--这正是PGIP所做的。证明脚本,广义上理解为导致目标的证明步骤的序列,是用户在使用证明助手时正在构建的主要工件,因此应该显式地表示和操作,而不是像GenGUI那样隐式地表示4Proof通用套件架构本文所述工作的新颖性是双重的。我们提供了第一个实现的证明独立的协议进行交互式证明,并在此之上,我们引入了一个新的用户界面,这是一个综合的两个现有的设计,结合基于文本的脚本处理与图形直接操作。本节描述了架构背后的思想;第5节和第6节描述了实现和用户界面。4.1交流交互式证明组件Proof General Kit的精神是使用轻量级协议将一系列用于进行交互式证明的组件连接在一起。组件是松散耦合的,可以在不同的机器上运行。设计的细节旨在与现有的定理证明器一起工作。因此,我们的一些设计决策看起来相当保守,这是因为我们希望允许现有定理证明器的逐步迁移,10D. 阿斯皮纳尔角Lüth/Electronic Notes in Theoretical Computer Science 103(2004)3校对助理PGIP图形用户界面证明助理调解人文本编辑PGIPWeb浏览器文件系统理论存储我们的架构,同时保持互操作性。根据我们的经验,这对于用户和定理证明器开发人员的接受至关重要。图三. 证明通用套件架构图3说明了基本计划。调解人具有核心作用:它将各种其他组成部分与证明助理和文件夹连接起来。可能的其他组件包括用于以图形方式显示和开发证明的GUI,用于编辑证明脚本的文本编辑器,以及用于探索理论存储或远程跟踪证明开发的Web浏览器。我们希望其他组件除了通过中介之外无法访问证明助理。其他组件可以直接访问理论存储,但是(特别是在写访问的情况下)这必须由中介器仔细批准。这种分离允许中介器组织交互式开发所需的同步消息,例如,维护一组锁定文件。4.2PGIP:一种交互式证明图 3 所 示 的 主 要 连 接 协 议 称 为 PGIP ( ProofGeneral InteractiveProof),其语法被指定为XML格式。PGIP的设计始于隔离和澄清目前在Proof General中实现的机制。PGIP消息可以分为两类:发送给证明者的消息和源自证明者的消息。 发送到证明器的消息包括 配置命令、用于检查校对辅助状态的各个方面的命令以及实际校对命令。从证明器发送的消息包括状态显示或错误对话框以及用于配置(证明助理专用)用户级菜单和首选项的消息。5或网络理论商店,如果支持的证明者D. 阿斯皮纳尔角Lüth/Electronic Notes in Theoretical Computer Science 103(2004)311apply(rule allI)/proofstep>/pgip> pgml> statedisplay>proof(prove):step 1goal(lemma(Foo),1 subgoal):1. atom kind=“bound”>x/atom>.<原子种类=“绑定”>x/atom> =原子种类=“绑定”>x/atom>/pgml>/proofstate>/pgip> /pgip>见图4。 一个真实的PGIP消息交换:上面是发送给证明者的证明命令,下面是 证明者图图4显示了一个证明器和接口之间的PGIP交换示例:接口发送一 个 证 明 命 令 ( ) , 证 明 器 用 一 个 新 的 状 态()进行响应。命令和响应被包装成包,包含诸如唯一标识(id)和序列号(seq)之类的元信息,这允许响应引用先前的请求(具有refseq属性)。请注意,我们概括了典型的RPC方案,这些方案是单请求单响应,允许对一个请求可能有许多响应。这样做的原因是为了证明者可以逐渐地向接口发送信息,也许是在长时间证明的过程但是,我们不允许证明者在没有事先请求的情况下发起响应来自证明器的第二条消息表示它已经完成了对证明命令的处理我们希望主要的证明过程是单线程的,更新证明状态是交互式开发的重点更一般地,可能的是,辅助线程将可用于检查加载的理论,或者其他进程将被用于卸载某些PGIP命令的处理。使用辅助进程的一个例子是处理和消息。我们假设PGIP命令可以直接由接口生成,或者由用户输入证明器的母语文本生成因此,需要有一种方法将证明脚本命令解析为PGIP12D. 阿斯皮纳尔角Lüth/Electronic Notes in Theoretical Computer Science 103(2004)3命令并将parse和unparse命令可能由证明器本身处理,或者由一个附加组件处理。 例如,对于足够简单的证明脚本语言,我们可以实现一个基于正则表达式的通用解析器;这类似于当前Emacs Proof General的工作方式。4.3PGML:一种用于打样显示的标记语言源自证明器的消息可以包含证明状态的表示,例如要解决以完成证明的子目标的为了传达这些信息,PG Kit包含了另一种XML格式,PGML,即Proof General Markup Language。标记语言是用来显示具体语法的。它包括数学符号的表示,以及表达术语结构的隐藏注释的可能性。这些注释可用于实现子项剪切和粘贴、指向证明或类似功能[11]。图中的证明者响应4显示了一个PGML消息嵌入在证明状态显示,与注释表示不同种类的变量。已经有基于XML的文档格式设计用于显示数学(MathML,[35])和在应用程序之间传输数学内容(OpenMath,[30])。以后,我们希望将这些语言与PGML一起使用。但是,这些格式需要来回发送术语的抽象语法,并在中介器(甚至显示器)中将标记转换为具体语法。虽然我们相信这是最终正确的方式,但现有的证明系统不能以通用的方式轻松地容纳它,因为这些系统通常有自己的(非常复杂的)规定来呈现具体的语法。这些机制立即得到PGML的支持,与此同时,它还提供了一条迁移路线;这是上面提到的保守设计决策之一。4.4增量验证开发PGIP假设了一个增量证明开发的抽象模型,我们假设证明器有四个基本状态,状态之间的转换由不同类型的证明命令给出。图5示出了基本的证明器状态以及它们之间的转换。所示的四种状态是:(i) 最高级别的状态,其中还没有打开任何东西;(ii) 当前正在处理文件的文件打开状态(iii) 理论开放状态,即理论正在建立的状态;D. 阿斯皮纳尔角Lüth/Electronic Notes in Theoretical Computer Science 103(2004)313OpenFile顶层TheoryStep打开Theory撤消TheoryStepOpenProof文件打开理论开放ProofStepUndoProofStepCloseFileCloseTheory证明打开CloseProof延期Proof放弃Proof中止Proof图五. 增量验证开发。(iv) 打样打开状态,此时打样正在进行中。区分状态的原因是,在每个状态下不同的命令是可用的,并且在每个状态下证明器例如,在理论状态中,我们可以发布理论步骤,将声明或定义添加到理论中,或者我们可以撤销添加。在证明状态下,我们可以发出证明步骤并撤消这些步骤,或者以多种方式完成当前的证明尝试。这些基本状态也产生了对象的层次结构:顶层可能包含许多文件,文件可能包含理论,理论可能包含证明。Proof命令可能需要额外的参数。OpenTheory命令通常会传递要构建的理论的名称,可能还有父理论(取决于证明者),而OpenProof则需要一个目标有待证实大多数证明命令直接对应于(通常)出现在证明脚本语言中的文本元素;这些是前面提到的正确不正确的命令用于控制证明器的状态,并且不会出现在正在开发的证明脚本中。这些命令包括图1中所示的三个斜体的撤销命令五、证明开发通过遍历基本状态、构建证明脚本来进行这个增量式开发模型是一个典型的prover中发生的事情的抽象,基于Proof General中使用的当前模型有些证明器可能没有实现所有这些(例如,有些证明器对文件一无所知;其他人识别理论和文件),有些证明器可能提供PGIP中没有捕获的更丰富的概念(例如,嵌套证明或通用证明)这里有一个证明器之间的差异,其证明脚本基本上记录了单独的交互命令(例如,Isabelle和Coq),而那些最终证明脚本可能采取稍微不同的形式。为14D. 阿斯皮纳尔角Lüth/Electronic Notes in Theoretical Computer Science 103(2004)3例如,在HOL中,脚本被鼓励包含为了处理第二种可能性,我们将使用两种形式之间的自动转换(尽管有经验的HOL用户可能希望能够手动优化他们的直接证明)。第一个PGIP版本中的另一个(有意的)限制是只允许顺序的单线程移动通过图1所示的增量证明部署状态五、这幅图不允许同时打开几个文件,或者在同一理论中进行几个开放的证明。这简化了协议(及其在证明器中的实现),但它并不排除中介器实现更灵活的开发机制,对用户隐藏底层上下文事实上,这在第5节描述的原型中实现了。5实现PG Kit架构PG Kit系统架构背后的思想已经在上面概述。该架构在其他地方有更详细的描述[6,8],包括PGIP和PGML语言的XML模式(用RELAX NG[32]编写)。本节描述我们的设计原型实现中介器维护整体状态,包括构造中的证明脚本、它们的依赖关系和证明代理的状态的抽象。它向校对助手发送命令并从校对助手接收状态消息;同时,它从显示器接收用户输入,并使显示器保持最新。原则上,我们可以同时连接到多个证明助手,但目前我们不能在证明者之间交换任何数据(如证明或定理)。一个显示引擎(或简称显示器)将证明助手到主经纪人,有不同的显示。一个简单的面向行的显示器显示文本行并传递用户输入的命令行;这对应于Emacs Proof General。稍微复杂一点的是,图形显示将用户手势(拖放等)转换为文本证明器命令;因此,IsaWin成为该架构中的另一个特定显示模块。其他可能的显示可以包括web界面(通过在浏览器中运行小应用程序的客户端,或者通过经由诸如servlet、ASP或CGI的技术将中介器嵌入web服务器我们进一步区分有源和无源显示器。主动显示器允许用户输入命令,而被动显示器主要D. 阿斯皮纳尔角Lüth/Electronic Notes in Theoretical Computer Science 103(2004)315校对助理PGIPTcl图形用户接口校对助理PGIPLispEmacsPG媒体历史显示:Emacs验证器封装事件代理器显示器:文件系统理论存储可视化证明,可能使用超链接文本。见图6。 系统架构图6示出了所实现的系统的架构。圆形框表示单独的组件,方形框表示中介体的不同模块。实现是基于事件的。事件由用户输入或证明器中的状态更改生成。中介器是中央事件代理;它接收输入事件,更新其内部状态,并在必要时将更改事件发送到系统的其他部分。事件是结构化的:它们包含PGIP消息。我们将中介器实现为一组Haskell模块,通过Unix管道松散耦合中介器包含一个中央事件代理,以及每个模块的一个事件处理模块,例如显示器和证明助理(参见图6)。 这种架构是可扩展的和可移植的(为了支持Windows操作系统,可以用套接字代替管道,或者使用兼容性软件包,如MinGW)。另一种选择是组件框架,它要么限制我们在操作系统 中 ( 例 如 , DCOM 或 .NET 仅 适 用 于 Windows , DCOP 不 适 用 于Windows)或编程语言(例如JavaBean)或权重太大(例如,CORBA)的目的。5.1事件和消息中介器在Concurrent Haskell中实现,使用Glasgow Haskell编译器,事件作为Haskell中的第一类值[33]。也就是说,我们有一个多态的事件数据类型,包含任何类型的值,具有同步事件的操作,对事件的操作进行排序,通过确定性选择组合两个事件,等等:事件a16D. 阿斯皮纳尔角Lüth/Electronic Notes in Theoretical Computer Science 103(2004)3sync:: Event a -> IO a(>=)::Event a->(a-> IO b)->Event b(+>)::Event a-> Event a->Event a这使得我们可以用进程代数的一个符号来编写并发函数程序,例如π演算[28]。事件包含PGIP消息。为了在Haskell中忠实地建模PGIP,我们使用HaXML [36]。从给定的DTD,HaXML生成一系列Haskell数据库,每个元素一个,以及读写XML的函数。这样做的好处是,DTD提供的类型安全性扩展到我们的程序中,使得发送包含无效XML的消息几乎不可能,并且可以立即检测到无效XML的接收。代理对消息进行进一步的验证,但它会尽可能地健壮;例如,如果响应没有引用有效的请求,则会悄悄地丢弃它(并写入日志文件条目)。有不同类型的事件,对应于PGIP DTD中的不同元素,由中介器中的不同类型表示。其中包括:• 证明器命令事件(ProverCmd)是发送到证明器封装的命令,可以从命令事件生成,也可以在重播证明脚本时生成。• 证明器消息事件(ProverMsg)是来自证明助理的响应于证明命令的消息,包含例如新的证明器状态或证明程序返回的错误,或来自证明助手的配置消息,添加或更改菜单、快捷按钮、图标或拖放表。 它们由事件代理解释,事件代理更新 其内部状态,并更新连接的显示器。• 显示命令事件(类型DispCmd)是用户输入的命令命令由活动显示器生成,通过解释手势或通过用户键入命令行(或两者的混合),然后由事件代理处理。• 显示消息事件(DispMsg)包含要显示的消息,例如新校对助手状态、错误或警告消息。显示事件是由事件代理从证明响应事件中生成的,或者作为一个答案生成的 对于用户输入(例如,试图浏览历史的末尾为了说明事件概念,图。图7显示了一个典型的交互序列:用户输入一个命令,它被证明者解析,一个新的对象出现在桌面上,当证明者计算命令的结果时,代理更新其内部状态和显示。D. 阿斯皮纳尔角Lüth/Electronic Notes in Theoretical Computer Science 103(2004)317显示经纪人证明器DCUSercmd解析脚本DispNewObject/DispHistUnparseCmdProverCmd(Proofstep.)DispState结果结果DispState见图7。 典型的事件序列。如交互序列所示,证明器可以在几个PGIP消息中发送对一个请求的响应,报告证明的进度。交互式证明器可能需要很长时间,有时甚至会出现分歧;因此,一旦收到这些消息,就立即显示,以使用户了解情况,这一点很重要。为了考虑到发散的可能性,我们必须能够打断证明者。目前,证明器在同一台机器上的子进程中运行,因此我们可以使用信号。对于一个分布式设置,其中证明器可能运行在另一台机器上,我们将需要提供传输带外中断信号,例如通过将证明器作为监听实际套接字的进程的子进程运行。5.2显示引擎所有的显示引擎,即使是像Emacs和PGWin这样看似不同的引擎至关重要的是,显示消息和用户输入可能会引用较早的消息。例如,在以后的证明中,用户通常希望使用他们以前证明过的定理。为了在一个统一的框架中支持不同的显示引擎,我们使用由通用图形用户界面引入的对象的概念(参见上面的第3节)。对象是系统需要跟踪的任何东西:最突出的是理论、定理和正在进行的证明,还有辅助对象,如策略、重写规则等。类型包括基本类型(如理论、定理和证明)和可证明者定义的类型(如辅助对象,它们因证明者而异)。每个显示器必须至少可视化基本类型,但可以不18D. 阿斯皮纳尔角Lüth/Electronic Notes in Theoretical Computer Science 103(2004)3想象所有其他类型。 因此,虽然PGWin表示所有对象, 通过它们的图标(图标是类型定义的一部分),Emacs将只表示与span对应的那些类型,span是特定文本框中的特定行范围。所有显示引擎都必须实现某些操作,例如显示警告、错误和状态消息;创建新对象;更新先前显示的对象;使对象过时;接收用户输入;等等。从技术上讲,我们定义了一个类型类Display,它定义了显示器必须实现的操作,例如创建和更新对象,生成命令事件(DispCmd),以及接收显示消息事件(DispMsg):class Display % d,其中newObject:: d-> ObjId -> ObjType -> DispAttr -> IO()updObject:: d-> ObjId -> ObjText -> IO()bind:: d-> IO(Event DispCmd)send:: d-> DispMsg-> IO()每一种显示引擎都是由不同的类型建模的,但都是显示类的实例:实例显示IsaWin,其中--函数的定义. instance显示Emacs--函数的定义.所有显示都保存在一个异构列表中(使用存在类型[22]):显示事件被发送到该列表的所有元素,并且由所有显示器生成的命令事件是每个显示器的命令事件与二元选择运算符(+>)对事件列表的明显扩展相结合。注意,在接口中实现对象的概念允许我们保持与指定依赖关系的对象的上下文信息:有效地,在线性PGIP协议中的位置。 这意味着用户可以在打开的校样之间切换,例如,通过用鼠标选择对象。在幕后,理论可以通过中止当前打开的证明并关闭其理论和文件来切换,然后再打开新选择的证明的文件和理论。这就是为什么显示器必须支持对象上的过时和更新操作:如果先前的定义被撤消,或者祖先理论被收回,代理将使所有依赖对象过时,并在接口中标记为暂时不可用目前,我们已经实现了一个主要的显示组件,PGWin。下文第6还有一个控制显示器,可以启动其他显示器。目前正在Emacs版本的ProofGeneral中进行工作,以支持Emacs的PGIP和Lisp接口D. 阿斯皮纳尔角Lüth/Electronic Notes in Theoretical Computer Science 103(2004)319如图所示。六、5.3支持PGIP的Isabelle我们的原型实现所需要的另一个部分是一些证据本身。通过设计,我们希望与现有的定理证明器进行接口,但认识到它们需要一些定制。在Isabelle开发团队的帮助下,一个支持PGIP的Isabelle/Isar [38]的实验性尝试已经开始。该实现包括一个500行扩展到现有的标准ML模块,用于与Isabelle已经提供的Proof General接口已经在其他Isabelle模块中也有一些微小的变化目前,我们使用Isabelle的(有些有限的)内置XML解析器和XML输出函数。与中介器中使用的强类型方法相反,这种实现不能自动保证生成(或解析)符合PGIP模式的XML,因为我们没有HaXML等应用工具来自动转换为SML数据类型。一旦PGIP的设计确定下来,我们将手工实现一个合适的SML数据类型。在Isabelle内部的PGIP实现基本上是简单的,尽管有一些棘手的问题已经暴露出来。为了生成正确的XML,我们必须小心转义特殊字符;这需要检查Isabelle输出消息的所有地方,特别是为了避免双重转义的可能性,因为我们已经为Isabelle术语调整了pretty-printer以生成PGML格式。为Isar语言提供解析器也是令人惊讶的困难,因为Isabelle内部的解析器是使用解析器组合子构建的,它不构建解析树或记录输入位置信息。最后一个开放的问题是在术语打印机中为Isabelle术语配备子术语结构信息的问题。虽然这已经作为IsaWin e Deborort的一部分实现[25],但不幸的是,代码是为Isabelle的旧版本编写的。希望在伊莎贝尔进一步开展关于PGIP支助的工作将解决这些问题。6PGWin显示引擎在PG Kit系统架构中,PGWin是一个特殊的显示器。它的设计是ProofGeneral和IsaWin的综合,产生了一个新颖的界面,将Proof General基于文本的交互与IsaWin的图形用户界面相结合这个想法是显示图标和包含对象的文本表示的文本。因此,我们在桌面上显示一个图标,一个已证明的定理,以及包含证明的文本以来20D. 阿斯皮纳尔角Lüth/Electronic Notes in Theoretical Computer Science 103(2004)3文本本质上是线性排序的,记事本上图标的无序显示被线性排序的分层树显示代替见图8。 PGWin显示引擎的界面(原型)。图8示出了原型的屏幕截图。我们可以看到左边的图标显示的对象,右边的编辑器中的实际校样文本。用户可以直接在编辑器中编辑校样文本(使用与Proof General相同的脚本管理技术),或者操作图标。用户的手势通过一个以对象类型为索引的表格转换为命令。该表以及校样助手的类型、图标和视觉外观的许多其他细节由显示配置消息确定,这些消息构成PGIP的一部分因此,当将证明助理连接到中介时,证明助理发送配置消息,该配置消息告诉系统证明所知道的对象的类型以及由拖放触发的命令。还有更多的显示配置消息,用于添加、更改或删除自定义菜单图9示出了由Is-abelle/Isar发送的PGIP配置消息的示例(没有周围的packet)。这些消息中的第一个设置接口,以便如果一个定理被丢弃到另一个定理上,则执行前向分解。为此,操作命令(在元素中给出)被扩展,以便为第一个参数(%1)插入第一个定理的名称(比如sym)D. 阿斯皮纳尔角Lüth/Electronic Notes in Theoretical Computer Science 103(2004)321第二个定理的第二个参数(比如refl)被替换为第二个参数(%2)。由这个扩展生成的字符串(sym THEN[refl])然后被发送到中介器,并从那里发送到证明助手。图9中的第二个配置消息设置后向分辨率。 空的目标类型()意味着它是一个证明操作。当一个定理(比如allI)被放到正在进行的证明中时,会生成命令apply rule(allI)/proofstep(,因为这是一个证明操作)并发送。<联系我们>theorem theorem/opsrc>定理optrg>%1 [THEN%2]/opcmd><联系我们定理/opsrc>/optrg>apply(rule %1)/opcmd>/opcmd><联系我们<联系我们图9.第九条。配置拖放:向前分辨率和向后分辨率用户可以自由地混合图形和文本交互(例如,键入一个校对步骤,并使用拖放功能进行下一个)。这种混合有一些明显的优点:它使用户习惯于命令语言的语法,因为他们会看到它出现在历史中,它提供了对所有证明器命令的完全访问PGWin显示引擎在HTk中实现,HTk是图形用户界面库和工具包Tcl/Tk到Haskell中的功能性扩展[18
下载后可阅读完整内容,剩余1页未读,立即下载
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://profile-avatar.csdnimg.cn/default.jpg!1)
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
我的内容管理 收起
我的资源 快来上传第一个资源
我的收益
登录查看自己的收益我的积分 登录查看自己的积分
我的C币 登录后查看C币余额
我的收藏
我的下载
下载帮助
![](https://csdnimg.cn/release/wenkucmsfe/public/img/voice.245cc511.png)
会员权益专享
最新资源
- ANSYS命令流解析:刚体转动与有限元分析
- ANSYS分析常见错误及解决策略
- ANSYS在隧道工程中的应用与实例解析
- ANSYS在桥梁工程中的应用与实例解析
- ANSYS动力学分析:模态、谐波与瞬态分析
- ANSYS结构分析模块详解:功能与特点
- ANSYS结构分析详解:从线性到非线性,包括静力、屈曲和接触分析
- ANSYS结构非线性分析基础:屈服准则解析
- ANSYS基础命令详解:操作与应用
- ANSYS命令详解:全面材料定义与单元操作指南
- ANSYS新手入门:从建模到求解与后处理
- ANSYS基础命令解析与操作指南
- ANSYS实体建模与网格划分技巧
- ANSYS结构分析详解:涵盖七种类型与单元选择
- ANSYS实体建模与有限元分析技巧
- ANSYS超单元详解:从模型生成到应用实例
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035711.png)
![](https://img-home.csdnimg.cn/images/20220527035111.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)