模块化结构操作语义与策略的应用

理论计算机科学电子笔记175（2007）3-17www.elsevier.com/locate/entcs模块化结构操作语义与策略阿尔贝托·贝尔德霍2FacultadeInform'ticaUniversidadComplutense de Madrid摘要在基于规则的系统中，策略是控制规则应用的有力机制。例如，可以定义不同的转换关系，然后通过策略进行组合，从而产生一种有效的工具来定义编程语言的语义。 我们赋予了Maude MSOS工具（MMT），一个模块化结构操作语义的可执行环境，通过将MMT与Maude策略语言解释器原型相结合，可以在其转换规则上定义策略。由于莫德的反应能力，这种组合是可能的。 MMT与策略的一个可能用途是执行有序SOS规范。我们展示了如何定义一种特殊形式的策略来表示一个OSOS订单，并因此执行，例如，具有负前提的SOS规范。在这种情况下，我们还讨论了两种已知的技术，用于表示负前提的OSOS在我们的设置中变得简单。保留字：模块化SOS，策略，有序SOS，负前提1引言策略是编程语言和系统规范的强大机制策略语言描述了如何通过基本策略的组合在给定的基于规则的规范中应用规则。在Maude的策略语言[ 7 ]中策略组合子是测试、条件、分解（即应用于子项的策略）和搜索。也可以定义递归策略。Maude策略语言用于实现结构化操作语义的重要例子* 由MCyTSpanishprojtMIDAS（TIC2003-0100）和RamonyCajal进行检索程序.1电子邮件：cbraga@fdi.ucm.es' www.example.com '（来自巴西联合国大学的O n l e a v e。）2电子邮件：alberto@sip.ucm.es1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.10.0244C. 布拉加A。Verdejo/Electronic Notes in Theoretical Computer Science 175（2007）3语言，它有几个可以通过策略[5]指定和组合的过渡关系，以及环境演算，其中策略[14]用于控制通信，复制和终止。我们通过将Maude MSOS工具（MMT）[2]（MSOS的可执行环境）与Maude的策略语言（MSL）[ 7 ]结合在一起，为模块化SOS（MSOS）[10]规范赋予了策略组合工具，名为MMT+MSL，实现为Maude的可扩展模代数在Full Maude [ 4 ]中实现的保守扩展为了说明我们的建议的有用性，我们展示了有序SOS（OSOS）[15]规范如何在MMT+MSL中直接表示，其中转换规则相同，顺序表示为策略。然后，使用这种表示，通过应用[15]中给出的技术，否定前提作为一个具体的例子，我们扩展了CCS的模块化SOS规范的优先级。本文的组织结构如下。第2节概述Maude第3节解释了有序SOS规范如何被表示为MMT+MSL中的规范第4节简要回顾了负前提如何在OSOS中表示。第5节扩展了第2节中的CCS规范，增加了优先级运算符。第6节以我们的最后评论结束本文2MMT+MSL2.1Maude重写逻辑中的重写规则既不需要是连续的，也不需要是终止的。当规范成为可执行时，这种理论上的普遍性需要一些控制Maude重新编写一个术语[7]。最简单的策略是常量基本策略包括应用规则（由相应的规则标签标识），一个给定的术语，并有可能为规则中的变量提供替代在这种情况下，规则被应用于术语中任何它匹配满足其条件的地方。当所应用的规则是在条件中具有重写的条件规则时，策略语言允许控制如何通过搜索表达式来解决重写条件还提供了一个操作然后将基本一些策略组合子是典型的正则表达式结构：concatena-tion（' ; '），un i o n（'|'），并添加关系（' * '用于0或更多，' + '用于1或更多，和'！对于“重复直到结束”迭代）。另一个策略组合子是典型的通过使用这个组合子，我们可以定义许多其他有用的策略组合子C. 布拉加A。Verdejo/Electronic Notes in Theoretical Computer Science 175（2007）35作为派生操作：例如，只有当第一个参数失败时才应用第二个参数策略的二元“orelse”组合子，以及当其参数成功时失败的一元“not”组合子，反之亦然。该语言还提供了一个还提供了扩展的“matchrew”，“xmatchrew”，其中重写模公理结合性、交换性、恒等式和当声明时，考虑幂等性。递归也可以通过给策略表达式命名并在策略表达式本身或其他相关策略中使用此名称来实现。使用Maude元级，我们实现了策略语言的原型，作为Full Maude的扩展[7]。目前，该语言正在被整合到Maude系统中。2.2MMT+MSL中的CCS模块化SOS是SOS的一个变体，它允许通过将转换规则中的标签结构化为可扩展记录来使规范模块化。给定构造器的语义规则使用来自记录结构的某些索引，使得新添加的规则可以在（现有的或）新的索引上变化，从而允许在需要新的语义实体时不改变因此，语义规则可以一次性声明。例如，用于功能性片段的规则可以从标签结构访问环境，而用于命令性片段的规则可以访问存储器组件。MMT [1]是MSOS的一个可执行环境，并且在[3]中提出的精确意义上被实现为一个形式化工具，也就是说，作为模块化SOS和重写逻辑之间的语义保持映射的实现模块化SOS定义形式主义是MMT支持的规范。它允许MSOS规范以非常简洁的语法编写，包括：支持BNF语法中的语法规范，隐式模块包含，现在让我们讨论如何在MSDF中指定和执行CCS。我们还提出了一种策略，解决了深度优先搜索的规则前提。声明具体的标签和进程标识符来测试我们规范的执行论文中没有显示运行，但是可以从http：//maude-msos-tool.sf下载该工具和该示例。净/mm t+ms l/.我们遵循的语义描述的建设性方法提出的[11]中的苔藓，因此将每个构建体作为MSDF中的单独模块呈现。 模块' LABEL '声明了一个The moduleclares包含标签和（不可观察的）“tau”动作的集合(msos标签为（msos操作为Label.行动上标签：：=~标签|一|B |C.操作：：=标签|τ的6C. 布拉加A。Verdejo/Electronic Notes in Theoretical Computer Science 175（2007）3sosm）模块(msos 过程就是过程。进程：：= 0。sosm）下面的模块中使用的MSOS标签结构有一个表示进程跟踪的索引“trace "中的引号MSDF中的转换规则非常直接地代表了转换规则的标准数学表示。然而，一些解释可以澄清标签的标记。 Labelsmayhaveellipsis（. ）或a（-）来表示未明确提及的标签中的所有索引。当使用省略号时，它意味着它所指的标签部分可以在过渡中改变破折号用于其他用途。当它们在同一规则中出现多次时，它们引用索引的同一子集。元变量，如X1和X2，也可以用来引用标签的索引子集，并用于区分同一规则中的两组模块' PREFIX '声明了一个请注意，对于可能为空的操作集，尚未显式声明集合“Action*”。 它是由模块“ACTION”中的集合“Action”的声明自动派生的，该模块由“PREFIX”自动导入。(msos前缀Process：：= Action; Process [prec20]. 标签={trace '：Action* ，.} .[prefix]（Action; Process）：Process-{trace ' = Action，-}-> Process.sosm）求和（注意，只需要一个规则，因为操作符被声明为可交换的，在BNF声明中使用关键字（msos总和为过程：：=过程+过程[asp_prec 30]。标签= {trace'：Action*，.} .流程1-{...}-> 过程1 '[总数]（进程1+进程2）：进程-{...}->进程1 '。sosm）Parallelism（'||“）所有这两个过程都是在系统同步的情况下执行的，即，一个执行”Action“，另一个执行”~Action“。 CCS语义不指定同步在出现副作用时的行为在我们的语义中，同步时不会产生副作用。(This是Reppy的λ cv中C. 布拉加A。Verdejo/Electronic Notes in Theoretical Computer Science 175（2007）37(msos PARALLELISM是看动作。过程：：=过程||过程[assumption prec 25]。标签={trace '：Action*，.} .流程1-{...}-> 过程1 '[par1]（流程1||过程2）：过程-{...}-> 过程1 '||过程2.进程1-{trace[par2]（流程1||过程2）：过程-{trace ' = tau，-}->过程1 '||进程2'。sosm）重新标记（(msos重新命名是看到行动。Process：：= rel（Process，Label，Label）[prec20]. 标签={trace '：Action*，.}.进程1-{trace' =进程1，...}-> 过程1 '[rel 1]- （rel（Process 1，Process 2，Process 1））：进程-{trace' = 102，...}-> 进程1 '。进程1-{跟踪' = ~进程1，...}-> 过程1 '[rel 2]- （rel（Process 1，Process 2，Process 1））：进程-{trace' = ~ 102，...}-> 进程1 '。进程1-{trace ' =进程3，...}-> 进程13 =/=~[rel 3]- （rel（Process 1，Process 2，Process 1））：进程-{trace' = 103，...}-> 进程1 '。sosm）最后，动作的限制（(msos 限制就是行动。Process：：= Process\Label [prec25]。标签={trace '：Action*，.} .进程1-{trace ' = Label 2，...}-> 进程1标签2 =/= ~标签1[res]-（Process 1\ Label 1）：过程-{trace' = Label2，.}-> 进程1 ' \标签1。sosm）MSDF在MMT中实现为Full Maude的保守扩展。因此，功能模块（用于等式规范）和系统模块8C. 布拉加A。Verdejo/Electronic Notes in Theoretical Computer Science 175（2007）3(for等式和基于规则的规范）可以与MSDF规范一起使用。标签的双重否定被指定为功能模块CCS系统模块中的MSDF模块(fmod标签一致性是（mod CCS是包括标签。包括PROCESS。包括前缀。包括求和。eq ~ ~标签：标签=标签：标签。 inc PARALLELISM. inc RELABELLING.endfm）inc限制。 包括标签一致性。endm）在我们解释策略模块的细节之前，需要先介绍一下如何在Maude中表示模块化SOS计算。Maude实现了重写逻辑演算，它有四个由自反性给出的推理规则（一个项可以是重写为自身）、传递性（如果t重写为tJ且tJ重写为tJJ，则t重写为tJJ）、同余性（规则可应用于t的子项）和替换性（规则可应用于种类保持替换）。 SOS没有这样的微积分本作者与其他人一起提出了几种技术（例如，[16，8]）在重写逻辑中表示模块化和普通SOS计算，并在Maude中实现了它们然而，使用策略，这些技术是不必要的，因为可以完全控制规则应用程序。重写性和传递性由基本策略控制，也就是说，如果应用一个基本策略，它代表一个（重写）步骤。然而，一致性需要控制，也就是说，基本策略的应用应该在顶级运营商处进行，而不是它的子项。这就是为什么取代推理规则是期望的，因此不需要被控制。除了使用它简化了策略，但向生成的Maude模块添加了与“step”规则相关的额外声明因此，选择“顶级”操作员可以产生更干净的当应用一个带有前提的规则时，策略应该指定解决每个前提的策略。为了使策略具有可扩展性，我们使用了一个3（stratdef PREM-STRAT是sop prem-strat。（完）另一个实现细节是，在这里我们明确地指出，策略另一种选择是使用广度优先搜索，如果使用上下文允许无限递归战略的定义也是模块化的。对于每个结构，我们定义一个策略，将语义规则应用于每个术语的顶部，并将3我们真正需要的是一个参数化的策略模块，但目前正在研究用参数化模块扩展Maude策略语言。C. 布拉加A。Verdejo/Electronic Notes in Theoretical Computer Science 175（2007）39如上文所述，关于房地的一般战略。我们在下面说明了前缀和并行结构的策略定义。（stratdefPREFIX-STRAT包括PREFIX。sopprefix-strat.seq prefix-strat = top（prefix）. （完）（stratdefPARALLELISM-STRAT是包括平行论。包括PREM-STRAT。sopparallelism-strat.seq平行性策略=top（par1{dfs（prem-strat）}）| top（par2{dfs（prem-strat）dfs（prem-strat）}）。（完）完整的策略，在模块' CCS-STRAT '中指定，由union str a t e g y'|“ofthe b a s i c s t r ategie s for ea chop e r ato r.（stratdef CCS-STRAT包含CCS。包括前缀-STRAT。包括SUMMATION-STRAT。包括并行-STRAT。 包括RELABELLING-STRAT。包括限制-STRAT。sop ccs-strat.seq ccs-strat= prefix-strat|求和层|平行性策略|重贴标签策略|限制策略（完）注意，这个策略可以通过检查语义规则自动生成。它反映了MSOS派生机制，但不依赖于CCS。而且，只有在具体化策略之后才能使用策略ccs-stratprem-strat就像下面的模块一样。（stratdef CCS-STRAT+包括CCS-STRAT。seq prem-strat = ccs-strat.（完）这种机制允许对策略进行模块化定义，当CCS在第5节中扩展为优先级操作符时，将在下面进一步举例说明。2.3MMT+MSL的实现MMT+MSL的当前版本依赖于在Full Maude中实现的MMT和MSL的原型。正如我们之前提到的，Full Maude为Maude实现了一个可扩展的模块代数。它提供了一个基本的基础设施，即一组元函数，以扩展Maude，这依赖于Maude的元编程接口. （例如，Maude预定义的“LOOP-MODE”模块定义了一个10C. 布拉加A。Verdejo/Electronic Notes in Theoretical Computer Science 175（2007）3为了定义Maude扩展的命令行界面，应该扩展。 它定义了一个三元组，包含输入（排序为' QidList '），系统的当前状态（排序为' State '）和输出（排序为' QidList'），由infix操作符' [，，]：QidList State QidList -> System '给出。然后，上面的下降函数应该操作这些值。这就是Full Maude所做的，如下所述在提醒中，我们首先评论扩展Maude的一般技术，然后移动到Full Maude。应该完成以下步骤：定义一个模块M，表示想要在Maude中表示的语言的语法;定义一个元函数，给定M的元表示中的元项，在Maude模块的元表示中产生一个元项;定义一个接口，封装M捕获的语言中的命令如何被翻译成M的Maude表示上的命令;以及Maude系统给出的“答案”如何Full Maude提供了实现所有这些步骤的基础设施。 有转换基础结构，其给出结构化的Maude模块，即具有包含的Maude模块，将其转换为单个Maude模块;一个数据库，也就是说，一个术语，它包含了所有加载在Full Maude中的模块，以及执行Full Maude命令所需的信息（数据库结构可以扩展到“缓存”信息，这可能是用M中的项（的表示）进行计算所必需的）;最后是一个漂亮的打印基础设施。FullMaude已经使用这个基础设施来指定参数化模块，例如面向对象的模块。MMT和MSL分别作为Full Maude扩展实现。（关于这两种工具如何在元级实现的具体细节，请参见[2，7]。） 这个组合很简单：我们编写了几个模块来连接这些部分，即解析、转换、数据库处理和漂亮打印。 模块(that它本身扩展了Full Maude在模块' MSDF-SIGNATURE '中定义的MSDF语法的语法fmod MMT+MSL-SIGN包含META-STRAT-SIGN。操作MMT+MSL-GRAMMAR：-> FModule。eqMMT+MSL-GRAMMAR = addImports（（包括'MSDF-SIGNATURE .），STRAT-GRAMMAR）。endfm模块由于Full Maude的规则和MMT+MSL之间不存在非确定性，因此它取代了Full Maude的输入输出模块。首先，它包括扩展文法，然后是MSL和MMT的数据库处理模块，MMT的预定义单元，最后是循环模式模块。mod MMT+MSL为prMMT+MSL-SIGN。数据库处理策略。prMMT数据库处理。prPREDEF-UNITS。包括循环模式。C. 布拉加A。Verdejo/Electronic Notes in Theoretical Computer Science 175（2007）311三个规则处理MMT+MSL的读取-评估-打印循环。下面标记为“init”的规则完整Maude它使用Maude面向对象表示法。数据库结构由MSL和MMT扩展。MSL使用属性对于深度优先搜索或队列，具有未解决的术语，对于广度优先搜索），表示策略定义的元模块，表示到目前为止找到的解决方案的一组术语，以及用于显示或不显示重复结果的选项的标记。属性内置技术来处理MSOS计算（rl [init]：init=>[nil，，(’\n ’\t ’\s ’\s ’\s ’\s ’\s ’\s'MMT '和'Strategy '完整'Maude '2.1.1 '组合'\s'\n）]。规则还有一个crl [in]：[QIL，，QI L ' ]=>[nil，，QIL'']=>[QIL，，（QIL ''QIL '）]如果QIL' =/= nil。恩德姆最后，在将实现MMT和MSL的模块以及上述两个模块3有序SOS的策略在本节中，我们将展示如何定义Maude策略来执行[15]中定义的有序SOS规范。一组具有排序（任何二元关系）的规则被称为有序SOS（OSOS），如果它只包含正GSOS规则（即没有规则具有负前提）。在[15]中表明，GSOS和OSOS具有相同的表达能力，12C. 布拉加A。Verdejo/Electronic Notes in Theoretical Computer Science 175（2007）3K动力. GSOS规则是以下形式， αij，Xi→Y ij、、、Xβ~kli∈I，j∈Jik∈K，l∈Lkγf（X1，.，X n）→C [X，Y]其中I和K是{1，.，n}，且所有的Ji和Lk都是IN的有限子集;X是序列X1，.，Xn和Y是所有Y ij的序列;并且C是上下文。例如，下面的规则定义了一个假设运算符的行为f，对于常数a和b：X→af（X）→aYR1f（Y）X→bf（X）→bY g（Y）r2{r11个前提，那么策略s应该在花括号内重复m次。如果m= 0，则r不被参数化。在[15]中，考虑到规则上的排序的转移关系→是与过程语言（A，R，<）相关联。 形式上，=→l中的跃迁定义如下l ω →l，其中p→α.PJ∈→l，如果d（p）= l且ρr∈R，ρ.ρ（con（r））=p→αpJ和Σρ（pre（r））KL→k和<$rJ∈higher（r）.ρ（pre（rJ））/<$k< l →k。定理3.1由OSOS规范诱导的转移关系由具有由上述算法构建的策略的相关联的SOS规范保持。素描证明。通过归纳法对过程项的深度进行了研究.基本情况是当过程是常数时，因此规则r没有任何前提andndhig her（r） =1. 由所有这些要素组成的流程替代品. 对于归纳情形，由于<$rJ∈higher（r）.ρ（pre（rJ））/<$r，k l→k成立，则通过归纳假设，策略not（union（higher（r）成功因为每个规则rJ的应用失败;并且，ρ（pre（r））KLk成立，因此通过归纳假设，应用于r的递归的策略成功，这使得策略r{s}的应用成功。Q4代表否定前提在这一节中，我们首先回顾如何在OSOS中表示具有负前提的GSOS规范，然后如何使用策略。我们改编了[15]中的材料，同时回顾了负前提在OSOS中的表现。对于没有关于规则排序的任何约束的OSOS规范（除了规则之间的简单二元关系之外），给定具有否定前提的规则，在规则顺序中在给定规则之上生成新规则。它的单一前提是给定规则中否定前提的肯定版本。至于它的结论，它与给定规则的结论有相同的左边，但过程0在右边。此外，生成的规则不应在其前提成立的情况下，可以启用配置，因此，它应该高于在规则的秩序中。让我们考虑由以下规则给出的假设算子fX→b YX~aR1f（X）→b TJ在OSOS中，这个规范可以简单地通过从规则r1中删除否定前提，在下面声明规则r2，以及r2在r1之上的顺序来编写。的14C. 布拉加A。Verdejo/Electronic Notes in Theoretical Computer Science 175（2007）3具体化然后变成如下，其中Y是r2中的新变量。X→b YR1X→aYr2{r1α X~βrθθ（X）→αθ（X J）给定一组有限的动作，上述方案可以用许多规则来表示，如rθ，但没有否定前提 ， 并 且 它 们 之 间 有 一 个 顺 序 r θ的一 个 示 例 策 略 是 s = not （ r θ c { s}|rθb{s}）;r θa{s}| not（r θc{s}）;r θb{s}|rθc{s}<<<以及标记为rθa、rθb和rθc的优先级运算符的规则。（同样，为了简单起见，我们没有使用抽象策略技术。）然而，这种规范可以进一步简化。策略可以应用于特定的替换。因此，在这个例子中，我们可以指定一个带有动作变量的规则rθ，而不是三个规则，该动作变量可以绑定到三个不同的标签动作，从而产生策略。egy' s = not（r θ [A ← c ]{ s}|r θ[A<$b]{s}）;r θ[A<$a]{s}| not（rθ[A ←c]{s}）;r θ[A←b]{s}|r θ[A←c]{s}'，其中' A '是动作变量。对于任意大的（但有限的）动作集合，策略可以通过表示给定动作标签之上的动作标签的动作标签列表来参数化。 如果我们考虑下面的函数forall，它从一个动作标签列表中产生一个策略，那么函数applica- tionhigher（a）返回一个动作标签列表的动作标签a对于所有的rθ（l，ls）= r θ[A ← l]|对于所有rθ（ls）对于所有rθ（nil）=空闲5.2MMT+MSL中带优先级算子的CCS鉴于第5.1节中优先事项作为战略的表述，第2.2节中CCS的具体说明可以很容易地扩展。首先，必须用优先级操作符扩展进程的语法，并且必须用第5.1节中的新的优先级转换规则（如r θ）扩展转换规则集，但不我们之前解释过的否定前提。还定义了Maude模块(msos优先级排序是16C. 布拉加A。Verdejo/Electronic Notes in Theoretical Computer Science 175（2007）3过程：：= theta（过程）[prec20]。标签={trace '：Action*，.} .进程-{trace ' = Action，...}-> 进程的[theta]theta（Process）：Process -{tracetheta（过程）。sosm）如第5.1节所解释的，该策略必须用新策略来扩展，以表示负前提。（stratdef PRI-STRAT包括PREM-STRAT。索普普里斯特拉特。seqpri-strat = not（top（theta[Action<-c]{dfs（prem-strat）}）|top（theta[Action-b]{dfs（prem-strat）}））; top（theta[Action-a]{dfs（prem-strat）}）| not（top（theta[Action<-c]{dfs（prem-strat）}）; top（theta[Action-b]{dfs（prem-strat）}）|top（theta[Action<-c]{dfs（prem-strat）}））。（完）替换“CCS-STRAT+”的模块（stratdefCCS-PRI-STRAT是包括CCS-STRAT。 包括PRI-STRAT。一等索普seq ccs-pri = ccs-strat|普里斯特拉seq prem-strat = ccs-pri.（完）6最后发言在[13]中，作者使用元级别在Maude中提出了GSOS规范的原型。我们的方法使用对象级别表示OSOS，它相当于GSOS [15]当然，从否定前提到命令再到策略的自动化翻译仍然是必要的此外，代表OSOS（从而代表GSOS）也是战略的一种可能应用。Maude（with strategies）可以直接用于表示任何具有策略的应用程序，包括OSOS。然而，如果想使其规范模块化，重写理论必须扩展以满足模块化要求。当前版本的原型不支持包含策略模块，尽管在[7]中有它们的符号（和语义）。所有的策略定义都必须在一个模块中声明。我们未来工作的一部分是全面支持战略语言。除了将否定前提转换为策略的自动化之外，我们希望在不久的将来进行的一个案例研究是E-LOTOS语义的实现[6]，其中使用否定前提以保证在时间流逝之前发生紧急行动C. 布拉加A。Verdejo/Electronic Notes in Theoretical Computer Science 175（2007）317致谢我们要感谢Fabricio Chalub对MMT+MSL实施的支持，感谢Narciso Mart的鼓励，感谢匿名裁判的深刻评论，感谢Peter Mosses的仔细审查。引用[1] Chalub ， F. ， “http://www.ic.uff.br/AnImplementationofModularStructuralOperationalSemantics in Maude ， ”Master's thesis ， Universidade Federal Fluminense （ 2005 ） ，www.example.com/dissertation.pdf.[2] Chalub， F.和C. Braga，Maude MSOS 工具，in： G. Denker和 C. Talcott，编辑，Proceedings SixthInternational Workshop on Rewriting Logic and its Applications，WRLA 2006，Electronic Notes inTheoretical Computer Science（2006）。[3] Cl avel，M.， F. 杜兰，S。 Eker，J. 我和M都是。-O. Stehr，M adeasaf or ma t ol，in：J. 黄，J. Woodcock和J. Davies，编辑，FM1684-1703年。[4] 杜兰，F.，“A R E M E D U L E A L G E B R A R E M E L G E R A R E M E L G E R A R E D U L E AL G E R A R E D L G E R A R E D U L E A L G E R A B R A P lA P LA D. 《我是你》（Universi dad eM'alaga，1999年）。[5] H i dal go-H err ero ， M. ， A.我 是 你 的 朋 友 。或 者 ， 例 如 -M all l'en ， LookingforEde nthroughMaudeandditstrategiess，in：F。L'opez-Fraguas，editor，VJornadassobreProgramaci'onyLengua j es，PROLE2005（2005），pp. 13比23[6] ISO/IEC，信息技术-LOTOS增强（E-LOTOS），国际标准ISO/IEC FDIS 15437（2001）。[7] M art's-Olie t，N.， J. 我的意思是。 因此，对于Madde，Towardsastrategylage，n：N。 M art't-Oliet， 编 辑 ， Proceedings Fifth International Workshop on Rewriting Logic and its Applications ，WRLA 2004，Barcelona，Spain，2004年3月27日至 4月4日，Electronic Notes in Theoretical ComputerScience 117（2005），pp. 417-441[8] Meseguer，J.和C.程序设计语言的模块化重写语义，在：C。拉特雷，S. Maharaj 和 C. Shankland ， editors ， Algesthetics Methodology and Software Technology ： 10thInternational Conference ， AM