一阶求解器API的工具构建

理论计算机科学电子笔记144（2006）15-26www.elsevier.com/locate/entcs一阶求解器API的工具构建要求吉姆·格伦迪1美国俄勒冈州希尔斯伯勒英特尔公司战略CAD实验室汤姆·梅尔汉姆2英国牛津大学计算实验室Sav aKrsti'c1美国俄勒冈州希尔斯伯勒英特尔公司战略CAD实验室肖恩·麦克劳克林3美国宾夕法尼亚州匹兹堡卡内基梅隆大学计算机科学学院摘要有效的形式验证工具要求将一阶逻辑和可满足性模理论的自动过程的鲁棒实现集成到逻辑演绎的表达性交互框架中，例如高阶逻辑定理证明器。本文阐述了决策程序的实现，使他们非常适合集成到这样的框架中的一些务实的要求。其目的是与决策程序软件的设计者展开对话，这将导致验证用户更大、更容易地接受其实现。关键词：抽象语法，CVC Lite，决策过程，一阶逻辑，forte，高阶逻辑，reFLect，工具集成1Email：{jgrundy，skrsti c}@i chi ps. 在te l。COM2 电子邮件：tom. comlab.ox.ac.uk3 电子邮件地址：seanmcl@cmu.edu1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.12.00316J. Grundy等人/理论计算机科学电子笔记144（2006）151引言英特尔公司[13]采用了一系列用于高性能处理器设计正式验证的证明技术验证框架（目前称为forte3，4）是围绕reFLect功能流程构建语法语言[7]。 几种验证技术被集成到forte3框架中，包括BDD，SAT过程，模型检查器和类似于HOL的高阶逻辑定理证明器[6]。reflect语言是用于协调集成工具的部署，以解决大型和挑战性的验证问题，以及通过符号执行探索规格和硬件设计它也是高阶逻辑定理证明器的基本术语语言在这个框架中有许多一阶推理的应用，并且已经完成了一些将决策过程集成到reFLect中的实验我们的目标是为一阶证明自动机提供支持系统的高阶逻辑定理证明器中的模理论例如，我们已经集成了Harrison模型消除过程的实现我们还集成了CVC Lite [2]，并在实验项目中使用它。基于这一经验，并没有声称原创性，我们给出了一些务实的要求，顺利集成的决策过程实现到一个系统，如反射等。我们首先检查我们的应用背景：forte3工具的性质以及我们如何在其中使用一阶求解器。然后，我们评论的一阶语言的设计与决策过程组件的然后，我们提出了我们的要求，通过应用程序接口（API）支持内存集成。我们意识到，我们的一些要求是相互竞争的，也许似乎是相互矛盾的。因此，其中一些被更试探性地表述为“欲望”。但我们希望，通过提出这些问题，我们可能会与决策程序软件的设计者展开对话，这将导致验证用户更容易地接受他们的实现。我们还将这些观察结果作为对SMT-LIB [12]讨论的贡献，SMT-LIB是一项旨在为一阶满意度模理论中的基准问题生成标准语言的倡议。4forte3可以下载用于学术用途。http://www.int el. 两个工作/生产/操作系统1/v的并发数J. Grundy等人/理论计算机科学电子笔记144（2006）15172应用程序上下文我们有兴趣在高阶逻辑的交互式推理工具的背景下应用一阶逻辑的求解器和简化器在我们的例子中，工具是英特尔开发的定理证明器，但一般情况是常见的。具有商业价值的验证超出了自动工具的范围，因此需要一个交互式证明构建框架和一个富有表现力的通用逻辑然而，同样重要的是，这些验证任务太大，无法完全手动完成，因此应用于选定子问题的自动推理也是必不可少的。在这种情况下，交互式推理工具通常采用类型化高阶逻辑的某些变体，因为它有助于捕获需求和设计抽象。逻辑的类型系统促进了数据建模，类型检查防止了微小的另一方面，最成功的自动推理工具是一阶逻辑。幸运的是，验证问题通常用高阶逻辑的一阶片段表示，或者简化为一阶子问题。即使是高阶性质，如果编码得当，有时也可以通过一阶推理来证明[9]。这显然导致了将一阶求解器集成到交互式高阶推理工具中的愿望。2.1内存集成在我们的交互式证明系统中，用户可以调用求解器来尝试手动地将公式简化为似乎是可解形式的证明对于这样的应用程序，检查公式有效性的命令可以写入外部工具具体语法中的文件，然后可以在该输入上调用。然而，当我们考虑更自动化和速度敏感的应用程序时，这种通信方法就不那么可行了例如，我们的定理证明器的重写子系统遍历example，搜索它可以从用户提供的条件方程集合中应用重写的站点在找到与等式左侧的匹配之后，它试图根据从匹配站点的上下文积累如果条件被解决，则执行重写无论哪种方式，该过程都将继续，直到满足某些用户指定的标准，通常是在不再进行重写这类应用程序可以产生对求解器的许多调用，在子项和公式的调用之间具有高度的通用性基于文件的通信似乎不适合这里。要求1我们需要一个内存中的API，用于一阶逻辑工具的原生数据结构中的术语和公式。API还必须允许18J. Grundy等人/理论计算机科学电子笔记144（2006）15我们调用解决和简化程序的条款和公式，这样构建。2.2接口中的状态交互式推理工具通常是用函数式编程语言实现的，而那些用于高阶逻辑的工具总是用ML的某种方言实现的。例如，我们的高阶证明工具是在reFLect中实现的，ML语言的一种方言，具有类似于LISP语言的反射特性。函数式语言通常采用急切求值策略，并支持纯函数式和有状态编程。但在实践中，由功能性风格所决定的简单性使工具设计者倾向于内部设计。最小化修改可见状态的操作数量的面。我们对函数式风格的偏好在reFLect中甚至更强，因为它使用了惰性求值，使得状态更改发生的顺序难以预测。愿望2：一阶工具的API应该最小化修改可见状态的操作数量。在适用的情况下，应该可以撤消状态修改操作。如果有一个状态修改API，我们总是可以通过提供一个monadic接口来恢复代码的透明性[14]，就像我们在与CVC Lite的集成中所做但是monadic风格的开销只是强调了我们对最小化状态修改的API的偏好。如果一个API提供了撤销状态更改操作的工具，那么我们可以创建纯函数，在内部执行状态更新，只是在返回结果之前撤销它们考虑上一节中描述的上下文重写当重写器遍历一个项时，它会通过上下文，在上下文中可以使用局部假设来解决重写的条件。CVC Lite API包括状态修改操作，以向证明状态添加假设并回滚到早期状态。当重写器进入上下文时，它可以将本地假设添加到CVC Lite证明状态，并在退出时再次删除它们当然，在上下文中也有上下文，但这些假设表现出一种后进先出的行为，这种行为与CVC Lite接口相适应，并最大限度地减少了重写过程中需要完成的操作数量当重写终止时，CVC Lite返回到其原始状态，因此重写器可以被视为纯函数。3逻辑设计问题大多数著名的决策过程和实现它们的可用SMT求解器因此，SMT-LIBJ. Grundy等人/理论计算机科学电子笔记144（2006）1519标准语言是具有相等性的多排序一阶逻辑，并通过一些非标准结构（如条件和局部let）进行增强。另一方面，在英特尔（和其他地方）捕获硬件及其属性以进行形式验证的逻辑是高阶逻辑的变体在这两个逻辑系统之间进行平稳和健全过渡的必要性引起了一些问题，我们仅提及其中两个问题。3.1类型和多态性赫德提出了一个从高阶逻辑到一阶逻辑的转换方案，可以表示任何高阶表达式[9]。该方案将λ-项编译成组合形式，并将所有函数应用替换为一个二元未解释函数·的应用。以n + m为例.在高阶逻辑中，两位函数+是curried的，并且具有高阶类型int→（int→int），所以我们的项实际上是一般来说，赫德在现实中，我们需要解释和非解释翻译的混合：当一阶证明器对函数符号有合适的解释时（如上面例子中的+），我们应该使用直接翻译;否则，我们翻译成·-terms。在这种转换方案中，类型信息被简单地丢弃了，使得这种方法通常不可靠。危险在于，一阶工具可能会使用高阶逻辑中无法键入的表达式为翻译后的公式找到赫德通过尝试在高阶逻辑中重放为翻译公式发现的任何证明来防止这一点他估计，在一百次尝试中，失败的证明不到一次他还探索了一种更精细的翻译，其中类型信息以一阶逻辑编码。这解决了任何逻辑问题，但代价是更大的一阶项。赫德这很方便，因为运算符另一方面，如果目标一阶逻辑是单态类型的（就像多排序的SMT-LIB一样），那么将·表示为单个运算符就会有问题我们需要引入一系列操作符，每个操作符对应于要翻译的表达式中出现的不同函数类型。然而，请注意，如果我们的一阶逻辑带有参数多态性，就有可能对“·”运算符进行编码，并且不需要重放证明或对类型进行编码以确保可靠性。20J. Grundy等人/理论计算机科学电子笔记144（2006）15letRNDpc rc s sgf=letL= Lsbpc sgf inletG= Guard pc sgf inletRS= RoundS pc sgf inlet rbit=（rc| （rc'='TO_POS_INF）=>（（NOTs）AND（GORRS））| (rc ’=’ TO_NEG_INF) => (s AND (G OR RS))| （L和G））|(L AND G))| 结果rbit pc sgf中的F;Fig. 1. 局部让在规格中增加清晰度。要求3一阶证明器组件的输入逻辑应该是无类型的，或者最好支持参数多态性。这一要求还有一个更简单的动机。一个工业验证问题通常会同时使用几种结构相似的数据类型--多种列表（整数列表、布尔列表）或不同的数组类型。将所有这些作为特殊情况编码到单态类型逻辑中是不方便的，可以通过多态来避免CVC Lite允许一些解释函数，例如。数组操作，就像参数类型一样，大概是为了适应这种实际问题。但我们希望对这类人给予普遍支持3.2当地LET在高阶逻辑中，公式只是布尔类型的项，而不是像一阶逻辑那样是一个独特的语法类别一个单一的let结构，如我们希望在我们要转换成的一阶逻辑中有这样一个构造，至少有两个原因。首先，它提供了一种简洁的表达形式，这在任何允许用户在推理过程 使用reFLect，我们可以自由地使用本地let来提高可读性，如图1中给出的在实际处理器验证中使用的浮点舍入操作的规范[1]。第二，具有本地let有助于节省空间地共享其他大型公式的o行（文本）表示。期望4逻辑应该包括let构造，用于在项和公式中引入局部项和局部公式。出于类似的动机，SMT-LIB具有（单独的）let构造，用于在公式中引入局部项和公式然而，没有构造来引入局部定义的术语，所以从高阶逻辑的更自由的syn- tax翻译到这种语言可能会很尴尬。另一方面，将另外两个let构造添加到SMT-LIB中，对于术语中的术语和J. Grundy等人/理论计算机科学电子笔记144（2006）1521公式中的术语，似乎相当混乱。我们在4.3节中简要地考虑了一种替代方案。4逻辑API要求在本节中，我们将给出一些关于API设计的指导，用于构造和操作术语和公式，并考虑逻辑本身描述的后果4.1构建逻辑结构由于其不同的优势，多个一阶求解器-CVC Lite的补充-将被考虑与forte 3集成。我们预计，随着工具的快速到来和现有工具相对性能的变化，SMT-COMP可能会使该领域类似于SAT求解器这是令人兴奋但令人担忧的;我们喜欢越来越强大的集成工具的前景，但如果它们都有不同的API呢？SMT-LIB标准通过提供用于与一阶工具通信的通用文本格式来解决这一问题我们希望有一个标准来解决内存通信的公共API需求求解器的内部数据结构将因工具而异，并且将随着人们探索优化而改变，但实现的逻辑的抽象语法应保持不变。因此，它是标准API的最佳指南要求5我们需要一个标准的 API来与一阶求解器进行内存通信。用于构造术语和公式的API应该遵循逻辑的抽象语法考虑来自HOL定理证明器家族的开发人员的经验[6]。由HOL的各种版本实现的逻辑的抽象语法-包括HOL 88，HOL 90，HOL 98，HOL 4，HOL-Light和Proof Power-是相同的，并且本质上与Church的简单类型理论的原始形式化相同这些系统都保留了相同的API来操作术语，基于这些术语的通用抽象语法他们已经做到了这一点，尽管在ML的四种不同方言中实现（在HOL88的情况下还有一些LISP），并探索了对术语表示的各种底层优化，包括de Bruijn与名称携带表示和延迟替换机制。与此相反，用于操作CVC Lite中的术语的API不仅受到逻辑的抽象语法的限制，而且还受到用于该逻辑中的推理的理论和决策过程的限制一个函数22J. Grundy等人/理论计算机科学电子笔记144（2006）15例如，应用程序的构造取决于该函数是元组构造、更新还是选择;记录构造、更新还是选择;未解释函数，还是原语解释函数之一因此，CVC Lite术语操作API在不同版本的工具之间会发生重大变化，并且不太可能在另一个一阶逻辑工具中复制。4.2检查逻辑结构我们对可以作为简化引擎和求解器的工具特别感兴趣。我们与CVC Lite的集成将CVC Lite简化器打包为转换，这是一种可信表达式转换的一般形式，我们的定理证明器的用户可以将其传递到我们的重写引擎[11]。用户可以通过将CVC Lite可以简化的每个子表达式替换为简化的结果来为了实现简化，我们遍历逻辑中的表达式，并在一阶工具的逻辑中构造翻译，调用一阶简化器，并遍历简化的表达式以将结果翻译为了翻译回来，我们必须能够区分一阶工具的项和公式的每种句法形式，并访问这些形式的任何子项要求6API还应支持对术语和公式的区分和解构。接 口 应 该 遵 循 McCarthy 描 述 的 抽 象 语 法 树 的 构 造 和 操 作 风 格 [10] 。McCarthy随着LISP函数式编程的出现而发展，麦卡锡的抽象语法方法与用于实现交互式定理证明器的函数式它可以很好地适应面向对象的风格，通常用于实现一阶求解器，表达式类的子类用于每个语法形式，动态转换用于区分语法形式，然后访问它们的组件。4.3一个简单的抽象句法的复杂性可以留给具体的句法和将其翻译成抽象的句法。这个设计抽象语法的指导原则对于我们这些工具集成者来说尤其重要。为了轻松地构造和操作集成的数据结构值，我们需要最简单的J. Grundy等人/理论计算机科学电子笔记144（2006）1523可能的接口，同时希望接口遵循逻辑的抽象语法。期望7逻 辑 的抽象语法应该尽可能简单。为SMT-LIB提出的抽象语法力求简单，但仍然可以更简单。特别是，在某些方面，CVC Lite的抽象语法比SMT-LIB提出的更简单，并且通过不进行区分而更接近于我们的主机工具的高阶逻辑在公式和项之间。这样就不需要像3.2节中考虑的那样需要多重let结构。5数据API要求在本节中，我们将讨论内存中积分所需的项和公式的一些低级操作，以支持到目前为止讨论的更明显5.1内存管理API要求再次考虑使用集成的一阶工具来释放重写器中的条件多次调用求解程序会显示出子项和公式的高度通用性为了避免重新构建公共结构，我们必须在调用之间保留对它们的引用这就需要对一阶工具的内存管理策略进行一些公开要求8一阶工具的API必须允许我们传达我们正在保留对术语或公式的引用，以及何时停止保留。根据一阶工具采用的垃圾收集策略，此要求有许多含义最简单的情况发生在工具使用引用计数方案时。我们只需要能够增加和减少引用计数。如果引用通过封装引用计数的智能指针进行通信，那么API特别容易使用。CVC LiteAPI就是这样工作几个与reFLect集成的命题工具使用标记和扫描垃圾收集。这样的工具需要API来分别公开调用，以启动标记和扫描操作，允许我们在扫描之前标记reFL ect引用的结构以及工具引用的结构。24J. Grundy等人/理论计算机科学电子笔记144（2006）15我们假设标记和扫描将由基于reFLect的集成框架调用集成工具必须提供一个API来注册一个方法，以通知reFLect它需要垃圾收集。如果集成工具可以需要立即垃圾收集，那么它必须提供例程，通过这些例程，我们可以为它注册方法，从而启动reFL等的标记和扫描操作。5.2数据索引API要求当集成一阶工具并支持简化时，我们将高阶项转换为一阶项和公式，并在简化后转换回来。在回来的路上，我们希望避免重新翻译不变的或共同的子术语和公式。我们也希望分享。我们可以通过将高阶项与它们的一阶平移相关联的表来做到这一点为了在任何一个方向上进行翻译，我们都要查找以前任何一次翻译的结果，只有在没有翻译的情况下，我们才执行翻译并存储结果以供重用。对于子项和公式，我们递归地这样做。要求9我们需要语法相等测试和哈希函数的条款和公式。不应为共享结构重新计算哈希。基于查找的翻译可以最小化翻译时间和翻译值的大小。CVC Lite系统提供了散列术语和公式的函数，用于确保最大共享。但是，仅仅依靠这样的功能并不能确保最小的重新翻译错误。即使是最少的重新翻译也不能确保最短的翻译时间。计算散列的时间和执行转换的时间都与要转换的结构的大小成比例除非散列比翻译快，否则不会实现保存为了实现节省，一阶工具必须在构建时存储带有项和公式的散列代码，或者缓存散列代码，以便它们不会为共享结构重新计算考虑在API中包括术语和公式的任意总排序函数可能是有用的，允许它们用作基于树的结构中的键当然，散列可以简单地概括这一点，因为我们可以比较散列代码，但是如果散列不是预先计算的，那么只测试两个项的相对顺序可能会更快。Desire 10我们想要关于项和公式的语法的全序函数。哈希和比较函数可以识别一些语义相同的术语和公式，前提是这些函数的行为一致。例如，如果阿尔法等效公式被认为是相同的，那么它们应该共享J. Grundy等人/理论计算机科学电子笔记144（2006）1525同样的hash。虽然工具可以识别一些语义相同的术语和公式，但它不应该在进行演绎时扩展它所识别的这些结构的集合这样做会使积累的翻译要求11基于语法的哈希和比较函数的结果不应改变。6结论我们已经说明了将一阶求解器集成到验证工具中的一些实用要求。我们从英特尔开发验证工具的角度撰写本文，专注于将一阶求解器集成到用函数语言编写的高阶逻辑定理证明器中。但提出的问题适用于更普遍的情况;许多问题都是在设计PROLOGIC工具包[5]时遇到和解决的，Prologic工具包是一个用于高阶逻辑数据的内存和分布式通信的集成框架。其他人也有类似的经历，从Boyer和Moore开始[3]，最近是PVS [4]。本文旨在强调和更精确地指导其他工作。我们的要求集中在需要一个合适的API来表示求解器的一阶语言的数据结构理想情况下，API是SMT-LIB等标准的一部分。人们可以想象这个标准包括一个使用API的解析器，并且可以链接到支持它的证明工具。像SMT-COMP这样的竞争对手将作为库提交，以链接到股票基准分析器和测试台。确认我们感谢杰里米·卡萨斯和约翰引用[1] Mark D. Aagaard，Robert B. Thomas F.作者：John W. O'Leary和Carl-Johan H.西格大规模硬件验证的一种方法。在Warren A. 小亨特 和史蒂芬D。Johnson，editors，Formal Methods inComputer-Aided Design：3rd International Conference，FMCAD，Volume 1954 ofLNCS，pages 263斯普林格，2000年。[2] 克拉克·巴雷特和谢尔盖·贝雷辛。CVC Lite：协作有效性检查器的新实现。在Rajeev Zurr和DoronA. Peled，编辑，计算机辅助验证：第16届国际会议，CAV，LNCS第3114卷，第515-518页。Springer，2004.[3] Robert S. Boyer和J Strother Moore。将决策过程集成到启发式定理证明器中：线性算术的案例研究。在J. E. Hayes，Donald Michie，and J. Richards，editors，Machine Intelligence：11thConference，pages 83-124.牛津，1985年。26J. Grundy等人/理论计算机科学电子笔记144（2006）15[4] 莱昂纳多·德·科雷亚、萨姆·奥雷、哈拉尔德·鲁埃什、约翰·拉什比和纳塔拉扬·香卡。整合验证组件：接口就是消息。 在Monterey软件工程工具研讨会：兼容性和集成，2004年。[5] 路易丝·A Dennis，Graham Collins，Michael Norrish，Richard J. Boulton，Konrad Slind，andThomas F. 梅 尔 汉 姆 PROSPER 工 具 包 。 International Journal on Software Tools forTechnology Transfer，4（2）：189[6] 迈克尔·J·C Gordon和Thomas F.梅勒姆编辑们介绍HOL：高阶逻辑的定理证明环境。剑桥，1993年。[7] 吉姆·格伦迪汤姆·梅勒姆和约翰·奥利里一种用于硬件设计和定理证明的函数式语言。Journal ofFunctional Programming，16（2），2006.[8] 约翰·哈里森。在模型消除中优化证明搜索。在Michael A. McRobbie和John K.Slaney，编辑，自动演绎：第13届国际会议，CADE，LNCS第1104卷，第313-327页Springer，1996年。[9] 乔 · 赫 德 。 高 阶 逻 辑 定 理 证 明 器 中 的 一 阶 证 明 策 略 。 In Myla Archer ， BenDiVito ，andC'esarrMunNouzoz ， editors ， DesignanddApplicationofStrategies/TacticsinHigher OrderLogics，number CP212448 in NASA Technical Report，pages 56[10] 约翰·麦卡锡关于计算的数学科学。在Cicely M. Popplewell，editor，Information Processing：Congress，pages 21-29.爱思唯尔，1963年。[11] 劳伦斯角，澳-地保尔森重写的高阶实现。Science of Computer Programming，3：119[12] 西尔维奥·拉尼斯和凯撒·蒂内利。 SMT-LIB标准，1.1版，2005年。[13] 汤姆·舒伯特下一代微处理器的高级形式验证。在设计自动化：第40届会议，DAC，第1-6页。ACM，2003年。[14] 菲利普·瓦德勒 函数式编程的Monads。 在Johan Jeuring和Erik Meijer，编辑，高级函数编程，LNCS第925卷，第24-52页，1995年