理论计算机科学电子笔记-174：PVS的应用与研究进展

理论计算机科学电子笔记174（2007）47-58www.elsevier.com/locate/entcsPVS#：PVS1的精简战术弗洛朗·基什内尔LaboratoiredC'esarMunZoz3国家航空航天研究所汉普顿VA23666，美国摘要证明语言的语义依赖于应用逻辑规则后证明状态的表示。 从逻辑的角度来看，这些信息通常是没有意义的，但对于描述语言提供的证明搜索的控制机制来说，这些信息是基本的。在本文中，我们提出了一个一元数据类型来表示状态信息的证明，我们说明了它的使用PVS定理证明。我们展示了如何使用这种表示来设计一套新的强大的PVS战术，称为PVS#，有一个更简单，更清晰的语义相比，标准的PVS战术的语义。关键词：单子，证明语言，战术，战术，策略，PVS。1介绍自20世纪70年代初第一个定理证明器被设计出来以来，数学证明的表示一直是计算机科学中一个活跃的研究课题已经提出了证明过程的几种表示，从逻辑公式的简单集合[2]到可类型化的开放项（由于Curry- De Bruijn-Howard同构），其中开放项用于处理不完整的证明[8，9，4]。然而，随着机械定理证明的速度加快，证明的复杂性增加，需要更多的方法来控制证明的构造，从而产生了更大和更精细的证明语言。1这项工作得到了美国国家航空航天局兰利研究中心根据研究合作协议号的支持。NCC-1-02043授予国家航空航天研究所2电子邮件：florent. inria.fr3 电子邮件地址：munoz@nianet.org1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.10.05748F. 基什内尔角Muñoz/Electronic Notes in Theoretical Computer Science 174（2007）47⎪⎪在Coq[3]和PVS[10]等证明助手中，证明语言包含两种证明命令：通过应用逻辑规则修改证明树的策略，以及提供证明搜索控制的策略。在这项工作中，我们主要感兴趣的是战术和它们的语义。我们注意到“tactical”和“tactical”这两个词在PVS中，战术被称为证明规则，战术被称为策略。为了简单起见，我们使用原始的LCF术语。策略是一种策略组合子，其行为取决于应用其参数后证明的状态。证明的状态通常包含非逻辑信息，如成功或失败，表明策略是否解决了当前目标或失败。 复杂的证明语言，如PVS和Coq语言，使用许多其他类型的状态信息。 例如，考虑PVS战术尝试，它同时是一个条件回溯组合子：（try t1t2t3）将其第一个参数t1应用于目标，如果它生成子目标，则将t2应用于子目标，否则应用t3。此外，如果t2失败，例如，因为t2=（fail），那么它启动一个回溯序列，该序列一直传播，直到它被计算为另一个try构造的第一个成员，在这种情况下，它计算它的第三个参数。try[1]的语义需要五种不同类型的状态信息：失败，成功，跳过，子目标，回溯 。 非 正 式 地 ， 如 果 |. | is a semantic evaluator, the semantics of try can beexpressed as follows:⎧⎪|t3|If|t1| ∈{skip，backt rac k}⎪⎪|不|If|不| ∈{f a ilu re，success}⎪1 1⎪backtrackif|不|=subgoals，⎪⎪⎨|为|=⎪1|∈ { f a ilu re，b a cktr a c k}| ∈{f a ilu re,backt rac k}subgoalsif|t1|=subgoals，⎪⎪|t2| ∈{skip，subgoals}⎪⎪⎪successif|t1|=subgoals，⎪⎪⎩哪里|=跳过|= skip|= f a ilu r e.|= fa ilu re.|= suc c e s s，|=success,在以前的尝试中，形式化PVS证明语言的语义[5]，证明的状态是通过简单地添加到证明树的表示中的标记来记录的在本文中，我们展示了如何证明状态信息可以优雅地建模一个简单的一元数据类型。数据类型及其属性在第2节中定义。在第3节中，我们将说明此框架在PVS新战术集设计中的应用，我们称之为PVS#。最后，第4节描述了PVS#中一元数据类型的实现。⎪F. 基什内尔角Muñoz/Electronic Notes in Theoretical Computer Science 174（2007）47492证明状态表示Monad是一种在函数式编程语言中描述命令式特性的流行方式，例如副作用和异常。其主要思想是将程序P视为非纯函数，例如，从A到B，但作为从值的态射A转换为数据类型MB，其中MB表示P中边元素的合取它的返回值是类型B。一元运算符遵循一元法则，与数据类型相关联，并提供了一种构建和编写程序的方法。一般来说，证明命令可以被看作是作用于证明对象的函数程序。 然而，证明助理，如PVS，也提供战术，不是纯粹功能性的，例如，fail和try，引发并捕获异常，分别此外，策略对证明状态的影响也可以看作是对证明对象的侧面影响。基于这些观察，我们定义了一个一元数据类型，它允许我们给出具有命令式特征的策略的指称语义。严格地说，我们的数据类型不是monad，因为它不是完全多态的。这禁止了一元结构的“堆叠”以及映射和连接操作的定义。然而，这些功能并没有在本文的范围内使用，它们的缺失并不妨碍证明语言的表达能力。2.1一元数据类型我们称证明对象为可能不完整的证明树的具体表示。这里提出的形式主义利用了这种表示的粗略抽象：我们只假设证明对象提供了在所有开放目标中区分当前目标集的方法。我们把X作为证明对象的类型，x，y，z作为X的居民，即，证明对象变量。我们定义一元数据类型MX如下：数据类型MX=成功：X→MX| subgoals : N → X → MX| exception : S → MX,其中N是自然数的类型，S是符号的类型。我们使用元变量m，m1，m2，. 在类型为MX的对象上进行排列。数据类型构造函数的预期语义如下：• 成功是指该策略实现了当前的目标;• 子目标n表示策略已经生成了n个子目标。就常规次级目标而言，0意味着当前目标没有修改;• 异常S指示策略已经引发异常S。总的来说，这种表示关注与用户相关的三个基本证明状态：目标是否关闭，目标是否生成，或者是否出现错误。50F. 基什内尔角Muñoz/Electronic Notes in Theoretical Computer Science 174（2007）47单元x=子目标 0x，⎧子目标N Y⎨m*t=（t x）布勒如果m=子目标n x且（t x）=子目标 0y如果m=子目标n x且（t x）/=子目标 0y否则，例2.1在PVS中，策略（split）对应于一个函数，当应用于一个简单合取的目标时，该函数返回子目标2，在分裂这个合取产生两个自动如果目标不是合取，则子目标在 下 文 中 ， 我 们 将 PVS 证 明 命 令 表 示 为 类 型 X →MX 的 函 数 。Morrepreciselley，lett|. |. Be ev aluofP VS pr oofcom m ndinomX类型的对象。这个评估器是为每个特定的证明命令定义的我们是我们是|不|x该值是对该过程的估计，并且该值是对该过程的估计。从这个角度来看，|不|具有X→MX的类型，并且可以被确定为函数t=λx。M. 尽管如此，我们还是将证明命令（如t）与它们的数学表示，即，t，通过强制他们的排版，分别在打字机和数学字体。2.2一元算子图1介绍了我们的monadic数据类型的操作符：• 类型为X→ MX的函数单元将证明对象映射到我们的数据类型的元素中，• 类型为MX→（X→MX）→MX的函数*提供了一种将策略t应用于由应用另一策略而产生的证明对象的Fig. 1. 一元算子这些算子满足单子定律。命题2.2算子满足左单位和右单位性质：（单位x）*t = t xm* λx。单位x =m，运算符*是结合的：m1*（λx.m2* λy.m3）=（m1* λx.m2）* λy.m3。证据 左单位和右单位的性质是微不足道的，人们可以简单地通过展开 * 的定义来检查它们。成功或例外情况下的关联性F. 基什内尔角Muñoz/Electronic Notes in Theoretical Computer Science 174（2007）4751⎪⎪⎪⎪⎪⎪战术是直接的。 在子目标的情况下，它是从零和非零子目标之间的布尔加法的结合性推断出来的。Q在PVS中，单位对应于战术跳跃的语义：|x =单位x。|x= unit x .函数*描述了一个策略的语义，该策略按顺序组合其参数，应用策略n+ 1，除非策略n引发了异常或证明了目标。因此，它对应于二进制序列的语义。 设t1和t2是策略t1和t2的语义评估，|x=（t1x）* t2.|x=(t1x)*t2.我们注意到，这与PVS然后，它基于try。例2.3 PVS try的语义需要两种类型的异常来处理“失败”和“回溯”机制。 设t1，t2，t3分别为t1，t2，t3的语义评价⎧n（t3x）⎪如果（t1⎪x）=异常回溯目标（t1x）=子目标 0y⎪⎪n（t1x）⎪如果（t1⎪x）=异常故障成功（t1x）=成功y⎪⎪异常回溯⎪如果（t1⎪x）=子目标n y，n > 0，⎪⎨|x=0|x=⎪⎪和（t2y）=异常失败or（t2y）=异常回溯子目标n z⎪如果（t1x）=子目标n y，n > 0，⎪and（t2y）=子目标 0z⎪拉吉子目标n z⎪如果（t1x）=子目标n y，n > 0，拉吉and（t2y）=子目标n z⎪⎪成功案例⎪如果（t1与（t2x）=子目标n y，n >0，y）=成功z。try语义的这种形式化显然比⎪52F. 基什内尔角Muñoz/Electronic Notes in Theoretical Computer Science 174（2007）47介绍中提到的那个。这部分是由于异常构造的冗长。但它也反映了这种特定策略的复杂性，它提供了几个功能：排序，进度测试，回溯和错误捕获。这种复杂性被从try衍生的策略继承，例如，thenandelse：|X=|（尝试t 1 t 2 t 2）|X|x|X=|（try t 1（skip）t 2）|X.|x.如图所示，一元数据类型允许对PVS3PVS编号PVS#是一组新的策略，取代了PVS策略try and fail提供的原生回溯和失败机制。新的一套tacti- cals功能的错误处理机制，基于捕获和抛出，典型的编程语言。PVS#中的策略更容易组合，因为它们的语义只需要一种类型的异常状态信息因此，try和fail的功能被分为三种不同的战术：一种是用于抛出异常的战术#throw，一种是用于捕获异常并隐式回溯的战术#catch，还有一种是用于测试进度的战术#ifsubgoals通过尝试和失败定义的PVS出于这个原因，PVS#还提供了基于尝试的PVS策略的替代，比如then和else.PVS#中的所有策略都被设计为在我们的框架中具有简单（如果不是原子的话）的解释。在本节的其余部分，我们将描述这些新的策略，将其传统的非正式描述与正式语义结合起来。假设ti是证明命令的语义评估ti对于任何索引i。3.1异常处理和进度测试（#throw标记）此策略返回未更改的证明对象，证明状态设置为异常标记。语义：|x= e x c e pt i o n t a g.|x=exceptiontag.（#catcht1&可选标记t2）如果t1没有引发异常，则此策略的行为与t1相同。否则，如果结果是一个名为tag的异常，那么它的值为t2. 如果标记与异常的名称不对应，则传播异常。F. 基什内尔角Muñoz/Electronic Notes in Theoretical Computer Science 174（2007）4753⎨1用法：proof script（#catch（#throw“exn”）“exn”（flatten））将导致（flatten）的求值，但是（#catch（#throw“div0”）“exn”（flatten））将传播名为“div0”的异常。语义：⎧如果（t1x）=异常标记，则返回（t2x）|x=0|x=⎩（t1x） 否则。（#ifsubgoaltt1t2）这个策略调用t1或t2，取决于t的进程。 如果t生成子目标，则它将t1应用于所有子目标。否则，它适用于t2。用法：proof script（#ifsubgoal（flatten）（propax）（split））应用（flatten）到当前目标。如果目标确实简化了，那么（propax）将应用于结果子目标。否则，（拆分）将应用于当前目标。语义：⎧如果（t1x）=子目标n y且n>0，则n（t2y）|x=（t 3 y）i f（t 1 x）= sub b g o a l s 0y|x=(t3y) if(t1x)=subgoals 0y⎪在这条路上走得太远了。3.2同一性、测序和重复（#skip）和PVS一样，这个战术没有效果。实际上，（#skip）严格地等于（skip），提供这个别名是为了一致性。语义：|x =单位x =子目标0 x .|x= unit x = subgoals 0 x.（#thent1. tn）这种战术首先将t1应用于当前目标，然后（#thent2... tn）到所有生成的子目标（如果有的话），或者到原始目标（如果t1没有结果）。语义：|(#thent1t2.. . tn）|x=（t1x）*t2*.. . *tn.54F. 基什内尔角Muñoz/Electronic Notes in Theoretical Computer Science 174（2007）47（#repeatt）迭代地将t应用于当前目标，直到它失败，证明目标或什么都不做。这个战术可能不会终止。语义：⎧⎨|（重复次数t）|yif（tx）=subbgoals nyandndn>0|x= 0|x=⎩（t x）否则，3.3其他战术（#ifexprt1t2）与PVS中一样，Lisp表达式expr针对当前目标进行计算。 如果t1和t2是PVS证明语言的元素，则此构造等价于PVS的战术性if。用法：proof script（#if（equal（get-goalnum *ps*）1）（ground）（prop））apply（ground）如果当前目标是其父目标的第一个子目标，否则apply（prop）.语义：⎧如果expr=Lispnil，则返回t1x|x =0|x=⎩（t2x）否则，（#whenexprt1. tn）此策略评估expr，如果结果为nil，则不执行任何操作，此策略的行为为跳过。否则，它适用于t1... 使用#then按顺序t n。用法：proof script（#when（equal（get-goalnum *ps*）1）（ground））如果当前目标是第一个子目标，则应用（基础），否则不做语义：|(#whenex prt1.. . tn）|X=|（#ifex pr（#thent1. tn）（#skip））|X（#first t1. tn）这个战术应用了t1中的第一个战术... tn不引发异常（如果有的话）。否则，它什么也不做。用法：proof script（#first（#throw“fault1”）（bddsimp）（#throw“fault2”））将（bddsimp）应用于当前目标。语义：• 如果n= 1F. 基什内尔角Muñoz/Electronic Notes in Theoretical Computer Science 174（2007）4755⎧如果（t x）=exceptions，则返回子目标 0x|x= 0|x=⎩• 如果n >1，（t x）否则。⎧⎨|（#firstt2.. . tn）|xif（t1x）=excpti ons，|(#firstt1t2.. . tn）|x=0 （t1x）否则，（#solvet1. tn）这个战术应用了t1中的第一个战术... tn证明当前目标，如果有的话。否则，它什么也不做。用法：proof script（#solve（case“y > 0”）（bddsimp））尝试将案例分析命令应用于当前目标，如果它不能完全证明它应用的当前目标（bddsimp）。如果这种策略也不能实现当前的目标，那么它就什么也做不了。语义：• 如果n= 1⎧（t x）if（t x）=successx|x= 0|x=⎩• 如果n >1，子目标0 x否则。⎧（t1x）if（t1x）=successx|(#solvet1t2.. . tn）|x=0 |(#solvet2.. . tn）|xotherwise，4执行本节介绍用于处理在PVS中实现monadic数据类型的内部策略。它们被分为两个不同的类别，MX的构造函数和析构函数。4.1构造函数（piks）这是子目标1x的构造函数。它生成一个子目标，与原始目标相同。语义：|x =次级目标1 y|x= subgoals 1 y其中y是x，当前目标是从自身推断的。（backtrack）这将生成异常回溯证明状态，与try创建的状态相同。语义：56F. 基什内尔角Muñoz/Electronic Notes in Theoretical Computer Science 174（2007）47|x =异常回溯。|x= exception backtrack.4.2销毁函数flag这是一个简单的列表结构，有五个布尔字段：success，subgoal（子目标n≥1的缩写），skip（子目标0的缩写），backtrack（异常回溯的缩写），fail（异常失败的缩写）。它用于记录战术的结果，这些战术通过以下战术进行测试卡尔（图totc）这个helper是析构函数的核心。它将t应用于当前目标，分析其结果，并将其填充到otc（flag的实例）中。然而，如果t证明了目标，则otc不会更新（因为在目标被证明之后无法进行此策略返回成功（如果t是成功）、异常回溯（如果t是子目标0、异常回溯或异常失败）或子目标n≥1（如果t返回子目标n≥1）。语义：⎧异常回溯⎪⎪⎨|x=0|x=⎪⎪⎪⎪if（t x）=subgoals 0yor（t x）=异常回溯or（t x）=异常失败否则，则为n（t x）。（inspecttotc）这个助手应用（figuretotc）到一个虚拟目标，然后丢弃它，完全填充otc中的结果并返回到原始目标。语义：|x= sub b g o a l s 0 x.|x=subgoals 0x.（信息t）这是最简单的战术编写与检查。它模拟了t的应用，填充了一个flag实例，并将其打印出来。语义：|x= sub b g o a l s 0 x.|x=subgoals 0x.（test-casett1t2t3t4t5）这是数据类型的析构函数分析了t使用检查，并根据结果应用其中一个ti。语义：⎪F. 基什内尔角Muñoz/Electronic Notes in Theoretical Computer Science 174（2007）4757⎨⎪45⎧（t1x）if（t x）=成功y⎪⎪n（t2x）if（t x）=subgoalsn y andn > 0|(test-casett1... t5）|x=（t3x）if（tx）=subbgoals 0y⎪（t x）if（t x）=异常回溯⎪if（tx）=exceptionfaiure.（testsuccesstt1t2）（testsubgoalsNtt1t2）（testsubgoals0tt1t2）（testexceptionbacktrack tt1t2）（testexceptionfail tt1t2）这些策略是测试用例策略的实例，它们应用它们的第一个参数。如果它的结果是预期的，他们就应用第二个论点。否则，他们会提出第三个论点。语义：⎧（t1x）if（t x）=成功y|x=0|x=⎩（t2x） 否则。其他测试策略的语义是类似的。5结论我们通过一元数据类型定义了证明状态信息的表示，它与证明对象的物理表示正交这使我们能够给出PVS证明状态的合成表示在我们的形式主义的PVS策略的正式描述揭示了不必要的复杂性PVS证明语言。因此，我们提出了一组新的PVS策略，在现有的证明语言之上实现，称为PVS#，可以说在错误处理和排序方面具有更简单的语义。PVS#的初步原型见[7]。本文的主题是正在进行的工作的主题，特别是包括PVS#的新策略的开发，证明语言中单子的元理论研究，及其在其他定理证明器中的应用特别是，一元数据类型的另一个实现已经在Fellowshipproof assistant中实现[6]。从长远来看，我们相信单子的概念将在过程定理证明器的证明语言的设计和语义中发挥核心作用。引用[1] Ar cher，M.， B. 迪维托和C。吴文龙，“高阶逻辑中的策略与策略设计与应用”，2003年第3期，国立台湾科技大学硕士论文58F. 基什内尔角Muñoz/Electronic Notes in Theoretical Computer Science 174（2007）47212448，NASA LaRC，Hampton VA 23681-2199，USA，2003，pp.16比42[2] 博耶河S. 和j.S. Moore，[3] Coq开发团队，LogiCal项目，INRIA，网址coq.inria.fr/doc/main.html[4] 约伊戈夫湾一、具有结合力的孔，英寸：H。Geuvers和F.Wiedijk，editors，TYPES，Lecture Notesin Computer Science2646（2002），pp.162-181。URLlink.springer.de/link/service/series/0558/bibs/2646/26460162.htm[5] Kirchner，F.，Coq战术和PVS策略：一个小步语义，在：M。A.例如，《高阶逻辑中策略/战术的设计与应用》（Design and Application of Strategies/Tactics in Higher Order Logics，2003）69比83[6] Kirchner，F.， （2005年）。URLwww.lix.polytechnique.fr/Labo/Florent.Kirchner/fellowship[7] Kirchner，F.，“Programmation Tacticals,”URLresearch.nianet.org/fm-at-nia/Practicals/[8] 我是L.，“A L F -A P r o f E d i t or B a s e d o n M a r t in- L o f的M o n o m o r p h i c类型理论与显式替换的实现”，博士学位论文。Chalmers University of Technology andGüoteborgUniversity（1995）.[9] 蒙尼奥斯角，“Uncal cul d es ub s itut i on s pour l a reep r e n tat i o n d e p r e v e s par t i e e e s en t h e ori ed e ty p es s，“The h e sed d o c t o c t t，Uni v e r s i t e P a r i s 7（1997），Eng l is h v e r s i o n a va a le a s I N R I A re s e a r c r e p o r t RR - 3309.[10] Owre ， S. ， J. M. Rushby 和 N.Shankar ， PVS ： A prototype verification system ， in ： D.Kapur ，editor，11th International Conference on Automated Deduction （CADE ）， Lecture Notes in ArtiFicial Intelligence607（1992），pp.748-752[11]Wadler，P.，Monads for functional programming，in：J. Jeuring and E. Meijer，editors，AdvancedFunctional Programming，LNCS925，Springer Verlag，1995 .