Maude：支持重写逻辑和隶属方程逻辑的应答语言

理论计算机科学电子札记124（2005）11-15www.elsevier.com/locate/entcsMaudeFranciscoD ura′n2Dp到。deLenguajesyCienciasdelaComputacio'nUniversidadeMa'laga马拉加、斯帕因摘要Maude是一种同时支持重写逻辑和隶属方程逻辑的应答语言。Maude系统地利用了推理，赋予语言强大的元语法能力，包括指导推理过程的陈述性策略。保留字：执行策略，Maude，重写逻辑，反射，元编程。1介绍Maude[3，4]是一种高级语言和高性能系统，支持广泛应用的等式和重写逻辑计算。重写逻辑[13]是一种变化逻辑，可以自然地处理状态和高度不确定的并发计算。在重写逻辑中，分布式系统的状态空间被指定为一个代数数据类型，用一个等式指定（E，E）表示，其中E是一个排序（类型）和操作的签名，E是一组（条件）等式公理。在Maude中，基本的等式逻辑是隶属等式逻辑[14]，一种Horn逻辑，其原子语句是等式t = tJ和形式为t：s的隶属断言，声明项t具有排序s。Maude的功能模块和系统模块分别是隶属度方程理论和重写理论。函数模中的方程，1由TIC 2001-2705-C 03 -02项目支助。2 电子邮件地址：duran@lcc.uma.es1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.11.02212F. Durán/Electronic Notes in Theoretical Computer Science 124（2005）11被认为是从左到右方向的规则，被假定为Church-Rosser和终止。因此，无论应用的顺序虽然Maude中的（等式）约简基本上是最内层（或渴望）的，但Maude能够通过使用策略注释来解释特定运算符参数的最外层（或懒惰）行为[10]。重写理论是一个对（T，R），其中T是隶属关系方程理论，R是涉及T的签名中的项的重写规则（标记的和可能有条件的）的集合。（T，R）中的重写以T中的等式公理为模发生。[3]R中的规则不需要是Church-Rosser的，也不需要是终止的，以这种方式打开了一个全新的应用世界当规范成为可执行时，这种通用性需要一些控制，因为用户需要确保重写过程不会朝着不希望的方向发展。在那些我们只想测试可执行性的情况下，或者考虑系统的发展，而对具体的执行路径没有特别的兴趣，Maude提供了两个内置策略：重写命令遵循自上而下的懒惰规则公平策略，而frewrite命令遵循自下而上的Maude还提供了一个搜索命令，用于那些我们有兴趣从满足某些属性的状态的起始项开始探索所有可能的执行路径的search命令对可能重写的树进行广度优先探索然而，一般来说，我们可能对其他形式的执行感兴趣，并且选择适当的策略对于执行重写理论至关重要。在Maude系统中，这种提供控制重写过程的策略的需要已经通过在元级上开发策略而得到满足。策略是在预定义模块META-LEVEL的扩展中定义的，通过使用其中的预定义函数，如MetaReduce，MetaApply，MetaXapply等作为构建块。通过这种方式，可以在元层次上定义各种内部策略语言[2，5]，也就是说，策略语言是在同一个重写逻辑框架内定义的，而不是被定义为附加的外部逻辑特征。2反射和META-LEVEL模块非正式地说，反应逻辑是这样一种逻辑，在这种逻辑中，其元理论的重要方面可以以一致的方式在对象级表示，以便对象级表示正确地模拟相关的元理论，3Maude支持对结合性、交换性和恒等式的所有组合进行模重写。F. Durán/Electronic Notes in Theoretical Computer Science 124（2005）1113pects.特别地，重写逻辑是反射性的[2]，Maude的语言设计和实现系统地利用了重写逻辑是反射性的这一事实。预定义的功能模块META-LEVEL有效地实现了普适理论U的关键功能。META-LEVEL具有排序Term和Module，因此项t和模块R的表示分别是排序Term的项t和排序Module的项R。模块META-LEVEL还提供了用于在元级重写和评估项的关键元级函数，即，元应用、元Xapply、元重写、元归约等。例如，函数元归约将模块R的表示和该模块中项t的表示作为参数，并使用R中的方程返回项t的完全约简形式的表示，以及其对应的排序或种类：op metaReduce：Module Term -> ResultPair [special.] . op{_，_}：Term Type -> ResultPair [ctor].操作metaXapply在任何可能的位置上对术语应用规则。前四个参数是模R的元表示，R中项t的元表示，R中某些规则的标签l，以及定义这些规则中变量的部分替换σ的赋值集（可能为空）最后一个自然数列举了解决方案，因为可以有不同的重写与不同的替代和不同的位置。另外两个数字参数指示可以应用规则的术语的最小和最大深度。操作MetaXapply：模块项Qid替换Nat绑定Nat ~> Result 4 Tuple？【特殊……】.操作{_，_}：术语类型替换上下文-> Result 4 Tuple[ctor]。metaXapply返回一个排序为Result4Tuple的元组，该元组由一个术语、相应的排序或种类、一个替换以及重写发生时给定术语内的上下文组成。3内部战略在Maude内部，定义许多不同类型的策略，甚至许多不同的策略语言都有很大的自由。这可以通过一种完全用户自定义的方式来完成，这样用户就不会受到固定和封闭的特定策略语言的限制。重写逻辑作为一种逻辑和语义框架具有很好的性质，许多其他逻辑和语义形式化都可以在重写逻辑中自然地实现。14F. Durán/Electronic Notes in Theoretical Computer Science 124（2005）11有代表性[11，15]。在Maude中，重写逻辑的元理论以清晰和有原则的方式被用户访问，作为逻辑和语义框架，Maude具有非常好的属性，其中可以表达和执行许多不同的逻辑和形式主义。事实上，Maude最有趣的应用是元语言应用，其中Maude用于为不同的逻辑、定理证明器、语言和计算模型创建可执行环境。重写允许使用理论中的重写规则来完全控制给定项的重写这种表达能力已被用于不同的应用程序。例如，在Real Time Maude [17]模块中，渴望规则和惰性规则之间存在差异，只有满足惰性规则仅在没有渴望规则可以应用时才应用的要求的重写路径才对此类模块有意义;在MobileMaude [6]中使用对象公平策略很久之后，这种策略才在Maude中可用（这种内部策略实际上是aude中当前可用的对象公平策略的原型规范）;Dura′n，Es cobar和Lu c在[ 7 ]中提出了Full Maude的扩展，其中包括计算命令（构造函数）初始表达式的范式，即使使用策略注释和Maude的内置计算策略不能获得它们;相同的作者在[ 8 ]中提出了另一个扩展，为Maude提供了处理按需策略注释的能力; Braga [1]扩展了Full Maude，以支持在Maude中可用的规则条件下重写，以便能够表示动作语义[16];Pita和Mart’s-Oliet在[18]中提出使用元对象来控制一组规则的执行，这些规则必须按照特定顺序应用;等等。虽然非常强大，但在许多应用中，简单的策略就足够了，因此希望提供避免进入元级的概念复杂性的方法。在这条线上，Mart 's-Oliet，Meseguer和Verdejo在[12]中提出了一种对象级的基本策略语言，用于Maudeveryclo s etto theELAN'strat egie s，而Dura'n，Rold'an和Vallecillo提出了一种通用的策略，通过保证给定的不变量得到满足来控制系统的执行[9]。这两个建议都已在Maude中实现（第一个是Full Maude的扩展），这表明Maude定义策略的反应能力的表达能力Maude系统、其文档、示例和案例研究的集合以及相关论文的列表可在http://maude.cs.uiuc.edu上获得。F. Durán/Electronic Notes in Theoretical Computer Science 124（2005）1115引用[1] C. O. Braga. 重写逻辑作为模块化结构操作语义框架。 PhDthesis，Pont i c iaUn iversid adeCat'olicadeRiodeJanneiro，Brasil，2001.[2] M. 克拉维尔在一般逻辑和重写逻辑与Maude语言的应用中的反思。纳瓦拉大学博士论文，1998年。[3] M. Clavel，F. 杜兰，S。 Eker，P. Lincoln，N. 我的天啊-我的天啊。梅塞格尤尔和J。你好。Maude：重写逻辑的规范和编程。理论计算机科学，285：187-243，2002。[4] M. Clavel，F. 杜兰，S。 Eker，P. 林科林，N。 妈的-哦，J。 我是你，还有C。 Talcott. 马友德2.0手册. 可在www.example.com上查阅http://maude.cs.uiuc.edu，2003年6月[5] M. Clavel和J. Meseguer。条件重写逻辑中的重写。理论计算机科学，285，2002。[6] F. 杜兰，S。 Eker，P. 林科林和J。 Mesegu er. M o b i l e Maud e的Pr incipl es。 在PROCS。2000年 ASA/MA联合研讨会，LNCS科学第1882卷。斯普林格，2000年。[7] F. 杜兰，S。 Escob ar，andS. 陆克文。 新的版本要求使用fulmude。在Procs.第五国际重写逻辑及其应用研讨会（WRLA'04），ENTCS。Elsevier，2004年。[8] F. 杜兰，S。埃斯科巴和S。 Lu cas. On-demandevaluationforr maud e. 在PROC S。5小时后。基于规则的编程研讨会（规则Elsevier，2004年。[9] F.杜兰先生。 Roldda'n ，anddA. 你好 Invariant-driventrategiesforr maud e.在 PROC S 。of4thIntl.重写和编程中的减少策略讲习班（WRS'04），ENTCS。Elsevier，2004年。[10] S.艾克Term重写与操作者评价战略在C.Kirchner和H. Kirchner，编辑，Procs.的第2国际机场讲习班对重写逻辑及其应用（WRLA'98），ENTCS第15卷。Elsevier，1998年。可在www.example.com上http://www.elsevier.nl/locate/entcs/volume15.html。[11] N. 我的天啊-我的天啊。Meseguer. 重新写入日志icalogi InD.M. Gabbay和F. Guenthner编，哲学逻辑手册，第9卷，第1-87页。Kluwer Academic Publishers，第二版，2002年。[12] N. 天啊-哦，撒谎，J。 Meseguer和A。我来了。 这两个是一个非常有趣的故事。InN. 妈的-哦，撒谎，撒谎，Proc s。5小时后。 WorkshoponRewritingLogi c anditsApplications（WRLA'04），ENTCS. Elsevier，2004年。[13] J. Meseguer。条件重写逻辑是并发的统一模型。理论计算机科学，96：73[14] J. Meseguer。隶属代数作为一个逻辑框架的方程规格。在F. Parisi-Presicce，编辑，《代数发展技术的最新趋势》，第1376卷，LNCS，第18-61页。 Springer，1998年。[15] J. Meseguer 。 重 写 逻 辑 的 研 究 方 向 。 在 us Berger 和 H.Schwichtenberg ， editors ，Computational Logic. Springer，1999年。[16] P. 苔藓动作语义学剑桥大学出版社，1992年。[17] P. C. OülveczkyanddJ. Meseguer. 在重写逻辑中，不存在真正的抽象和复杂的系统。理论计算机科学，285，2002。[18] I. Pitand N. 我的天啊。一种适用于电信网络的非阻塞性模块化的Maudespeion理论计算机科学，285，2002。