模块化重写语义的实践

理论计算机科学电子笔记117（2005）393-416www.elsevier.com/locate/entcs模块化重写语义的实践克里斯蒂安诺·布拉加UniversidadeFederalFlumminense，Niter'oi，Brazil我是梅泽格尔美国伊利诺伊大学香槟分校摘要我们提出了一个通用的方法来实现模块化的语义定义的编程语言指定为重写理论，使语义规则不必重新定义的语言扩展。我们通过两个语言案例研究来说明这种方法的实际使用：CCS的两种不同语义和GNU bc语言的三种不同语义。关键词：重写逻辑，编程语言语义，模块化1介绍从早期开始，重写逻辑就被理解为一种语义框架，特别适合于定义编程语言的数学和操作语义[22，27，19]。一个专业的定义语法语言L采用重写理论RL的形式。L的语法语义由初始模型TRL提供，L的操作语义由理论R L中重写逻辑的演绎推理提供。给编程语言一个重写语义实际上是开发可执行的编程形式定义的一种简单方法语言，然后可以进行不同的工具支持的形式化分析，现在是一个公认的事实[40，2，41，37，36，25，38，8，35，39，14，15]。程序设计语言的重写逻辑语义与代数语义和结构操作语义都有关系，1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.06.019394C. Braga，J.Meseguer/Electronic Notes in Theoretical Computer Science 117（2005）393两者的结合和延伸[28]。由于等式逻辑是重写逻辑的子逻辑，因此重写语义是代数语义的自然概括（参见，例如，[42，18，5]对于早期的论文，[31]对于与动作语义的关系，[17]对于最近的教科书），其中编程语言L的语义被公理化为等式理论（EML，EL），因此L它的操作语义通过用（典型地Church-Rosser）方程EL的方程简化给出。这种概括的要点是，等式逻辑非常适合于指定确定性语言，但不适合于确定性语言。适合并发语言规范。在重写逻辑中，确定性特征由等式描述，而并发性特征则由具有并发转换语义的重写规则从早期阶段就已经知道[22，27，19]，是结构操作语义（SOS）定义到重写逻辑的自然语义映射。本质上，SOS规则被映射到条件重写规则[19，38，39，26，28]。重写逻辑语义结合了代数语义和SOS的最佳功能，在一个广义的框架中，增加了这两种形式主义中缺少的此外，数学语义和操作语义之间的一致性被扩展到这种一般设置，采用重写逻辑的完备性定理的形式[22，6]。重写逻辑中等式和规则之间的区别不仅仅是学术上的兴趣。问题在于，由于用规则R重写是以方程E为模进行的，所以只有规则R对系统的状态空间的大小有贡献这一观察，结合重写逻辑有几个高性能的实现[1，16，11]和相关的形式验证工具[12，20]的事实，意味着我们可以使用重写逻辑语言定义来获得实际的解释器和语言分析工具，基本上是免费的。例如，在JavaFAN形式分析工具[14，15]中，Java和JVM的语义被定义为Maude中的重写理论，然后用于执行形式分析，如符号模拟，搜索和Java程序的LTL模型检查，其性能优于其他Java分析工具。重写逻辑内部的进步已经大大提高了它对编程语言语义的表达能力，导致了非常简洁和表达性的语义规则，可以在当前的语言实现中执行。这方面的相关发展包括：C. Braga，J.Meseguer/Electronic Notes in Theoretical Computer Science 117（2005）393395• 表达型方程逻辑，如隶属方程逻辑（MEL）[24];• 在非常一般的假设条件下重写规则的可执行性[10];• 通过允许某些参数被冻结来精细控制重写[6];• 语言支持重写策略，无论是在对象级别[1，21]，并在元级别[13，9]。本文提出了一个进一步的进展，即一个通用的方法，使重写语义的编程语言模块化，在这个意义上，扩展一个语言的新功能不需要重新定义以前的语义规则。我们的工作受到Peter Mosses的模块化结构操作语义（MSOS）[32，33，30]的启发重写逻辑[3，2，4]。与MSOS方法相比，我们的方法有一些相似之处，也有一些不同之处。一方面，我们与MSOS分享了使用记录继承的想法，可以轻松地将新的语义实体添加到语言定义中，而不必更改语义规则;在我们的例子中，这是通过关联-交换匹配来实现的，该技术已经被用于使重写规则模块化，并且在Maude的面向对象模块中是可扩展的[ 23 ]。另一方面，与MSOS存在一些差异。首先，MSOS是一个实质性的和新颖的语义框架，以非常重要的方式扩展了原始的SOS框架[34]。相比之下，我们只提出了一个模块化的方法，它不会以任何方式改变重写逻辑框架。第二个不同之处来自我们对抽象接口的系统化使用，这一主题在SOS中发展得相当少。本文的目的是相当温和的，即：（1）解释我们的方法和它的一般原则;（2）通过具体的案例研究来说明它的实际用途。其他重要的主题被忽略了，包括：（1）详细讨论SOS和重写逻辑之间的关系（我们参考[19，38，39，28]和我们的同伴论文[26]）;（2）MSOS和我们提出的方法之间的精确关系，在[26]中详细讨论。然而，我们可以通过声明存在语义保持映射τ：S<$→τ（S）将nMSOSs具体化为满足我们的模块性要求的重写理论τ（S在实践中，翻译τ可以用来为诸如Maude [11]之类的语言构建MSOS396C. Braga，J.Meseguer/Electronic Notes in Theoretical Computer Science 117（2005）393我LL本文的结构如下。第二节给出了有关MEL的前提条件和[6]中MEL上的广义重写逻辑第3节解释了我们的方法;第4节讨论了我们详细开发的两个语言案例研究，即CCS的两个不同的模块化语义[29]和GNU bc语言的三个模块化语义 。完整的 可执行规 范，以 及两种语 言的程序 的示例 评估，可 以在www.example.com中找到http://formal.cs.uiuc.edu/meseguer/modular。2MEL与广义重写逻辑这一节收集了关于成员关系方程逻辑和广义重写逻辑的基本前提。Maude 2.0[11]是用于指定我们的案例研究的语言，支持MEL的所有逻辑功能和本节中描述的重写逻辑，其语法几乎与数学符号相同。隶属方程逻辑（MEL）[24]是一种类型化的方程逻辑，其中数据首先按种类分类，然后进一步按排序分类，每个种类k都有一个相关的排序集合Sk，因此具有种类但没有排序的数据被理解为错误或未定义的元素。给定一个MEL签名n，我们写Tn，k和Tn（X）k分别表示X中变量的k类基n-项和k类n-项的集合，其中X ={x1：k1，.，xn：kn}是一组kinded变量。原子公式有t=tJ（n-方程）或t：s（n-隶属度）的形式，其中t，tJ∈Tn（X）k，s∈Sk; n-语句是这样的原子公式上的普遍量化Horn子句。 一个MEL理论则是一对（E，E）其中E是一组句子。我们给出了在[6]中定义的MEL理论上重写理论的一般版本重写理论是一个元组R =（E，E，φ，R），包括：（i）MEL理论（E，E）;（ii）一个函数φ：k →kf（N），它将一个集合φ（f）k {1，. n}的冻结参数位置;（iii）（普遍量化的）标记条件重写规则q的集合R，具有一般形式（X）q：t→tJ如果 i∈Iui =uJj∈Jvj ：sjl∈Lwl →wJ（一）其中对于K中的适当种类k和kl，t，tJ∈T<$（X）k和wl，wJ∈T<$（X）k对于l∈L.函数φ指定函数符号f的哪些参数不能重写，这些参数被称为冻结位置。注意，如果f的第i个位置被冻结，则在f（t1，.，tn）t i的任何子项也变为冻结。的LC. Braga，J.Meseguer/Electronic Notes in Theoretical Computer Science 117（2005）393397J1JM我L1mJR• 回复性。对于每个t ∈ T<$（X），（<$X）t−→ t（X）u−→vE（X）u=uJE（X）v=vJ• 平等的（X）uJ−→vJ• 一致性。 对于每个f：k1. k n−→ k in n，其中{1，...，n} − φ（f）={j1，.，jm}，其中ti∈T<$（X）k，1 ≤i≤n，且其中tJ∈T（X）k，1≤l≤m，（X）tjijljl−→tJ.（X）tj−→ tJ1j1mjm（X）f（t1，.，tj1，.，tjm，... ，tn）−→ f（t1，. ，tJ，...，tJ，... ，tn）• 更换.对于每个有限代换θ：X−→T（Y），假设X={x1，.，xn}，且θ（xe）=pe，1≤e≤n，且对于R中的每一规则，q：（<$X）t−→tJ如果（u我=uJ）（vJ：sj）（wlL−→wJ）其中Z ={x，j，.，xj}中的未冻结变量的集合，则，J（（Y）pjr−→p）R（（1）（2）（3）（4）（5）（（1）（2）（3）（4）（（Y）θ（w）−→θ（wJ））iiijjjlll（Y）θ（t）−→θJ（tJ）其中对于x∈X−Z，θJ（x）=θ（x），对于xj∈Z，θJ（xj）=pJ，1≤r≤m。• 及物性R RJR（X）t1−→t2（X）t2−→t3（X）t1−→t3Fig. 1. 重写逻辑的演绎规则。冻结的思想延伸到子项，特别是变量。给定两个项t，tJ，我们可以定义它们的冻结的集合φ（t，tJ）和ν（t，tJ解冻结）变量（参见[6]）。给定重写理论R =（x，E，φ，R），R的一个n是一对相同类型的（统一量化的）项t，tJ，记为（nX）t→tJ，其中X ={x1：k1，. ，xn：kn}是一类变量的集合，对k，t，TJ∈ T<$（X）k.我们说R包含<$（<$X）t→tJ，并写作R <$（<$X）t→tJ，如果<$（<$X）t→tJ可以通过图1中的推理规则获得。相关性、传递性和相等性是通常的规则对于空闲重写、串联重写和以MEL为我J398C. Braga，J.Meseguer/Electronic Notes in Theoretical Computer Science 117（2005）393理论E. 同余允许重写广义运算符的参数，但条件是冻结的参数必须保持空闲。然而，任何未冻结的参数仍然可以被并发重写，正如前提中的重写所表示的那样。替换的特点是重写规则在其最一般的形式（1）的并发应用。它表明，对于任何重写规则q∈R和任何（保持类的）替换θ，只要满足q的条件，那么就可以将重写q应用于θ（t）。此外，如果θJ是X中变量的第二个（保持类的）替换，使得θ和θJ在所有冻结变量x∈φ（t，tJ）上一致，而重写（Y）θ（x）→θJ（x）对于未冻结变量x∈ν（t，tJ）是可证明的，那么这样的嵌套重写可以与q并发应用。3模块化重写语义模块化只有在增量规范的上下文中才有意义，其中语法和相应的语义公理被引入相关特征的组我们可以将编程语言L的语法的增量表示描述为语法定义的索引族{Li}i∈I，其中索引集I是具有顶元素T的偏序集，使得：（i）如果i≤j，则Li∈ I， Lj，以及（ii）LT= L.一种增量重写语义 为L则是重写理论的索引族{RLi}i∈I，其中RLi定义为语言片段L i的语义。增量重写语义{RLi=（Ei，Ei，φi，Ri）}i∈I的模块性本质上意味着两件事。首先，它应满足以下单调性性质：如果i≤j，则存在理论包含RLi <$RLj。这在SOS中并不容易实现，因为典型的SOS定义通常是非单调的（见[30]）。然而，人们总是可以实现单调性的后验，一旦一个人已经达到顶部模块RLT。然后，我们可以为每个语言片段Li划分RLT的新子模块，这些子模块将具有“正确”的这是一个骗局，因为可以通过典型的无法继承这些当一个非常不同的新功能被添加到进一步的扩展公理。这就是为什么除了单调性之外，我们还需要扩展性的第二个要求。 可扩展性意味着重写规则已经定义 以尽可能抽象和一般的方式，这样当我们用新的特征扩展一种语言时，以前的规则不必修改，因此扩展可以以单调的方式进行。通过这种方式，每个语言特征的语义都可以一劳永逸地定义，这样我们就不必在后来的语言扩展中收回早期的语义定义C. Braga，J.Meseguer/Electronic Notes in Theoretical Computer Science 117（2005）393399当然，这也意味着模块化的语义定义可以在一个特征接一个特征的基础上重用，这样一种新语言的大部分（或全部）语义就可以很容易地定义，只需根据选择的具体语法来重命名定义其特征语法的模块。 因此，人们感兴趣的是开发尽可能模块化的编程语言的增量重写语义定义的方法，在单调和可扩展的意义上。我们提出的方法使用对，称为配置;第一个组成部分是程序文本，第二个是具有不同语义实体的记录，这些语义实体随着程序的计算而变化。 也就是说，我们将与程序计算相关的所有语义实体组织在一个记录数据结构中。例如，记录的字段之一我们可以在Maude中用下面的隶属关系等式理论来指定配置（一个函数模块，在保护模式下导入后面显示的RECORDfmod CONF正在保护RECORD。排序程序会议op<_，_>：Program Record -> Conf [ctor].endfm第一个关键的模块化技术是记录继承，它是通过模式匹配模结合性，可交换性和身份来实现的。后来添加到语言中的特性可能需要向记录中添加新的语义组件;但是旧特性的公理可以这些原则将以完全普遍的方式一劳永逸地给出：它们将同样适用于记录中的新组件。这是莫德对记录的隶属度方程理论的说明。注意Maude的约定，即用子排序包含偏序集中的连通成分来标识类，并将它们命名为这些成分中排序的等价类。例如，[PreRecord]表示由连接组件确定的类型{字段，预记录}。fmod记录是排序索引组件字段预记录记录真值。子排序字段<预记录。op tt：->真理。opnull：-> PreRecord [ctor].op _，_：PreRecord PreRecord -> PreRecord [ctor asynchronid：null].op _：_：[Index] [Component] ->[Field] [ctor].op {_}：[PreRecord] -> [Record] [ctor].重复操作：[PreRecord] -> [Truth]。var I：索引。vars C C '：组件。var PR：PreRecord.400C. Braga，J.Meseguer/Electronic Notes in Theoretical Computer Science 117（2005）393eq重复（（I：C），（I：C '），PR）= tt. cmb {PR}：记录是否重复（PR）=/= tt。endfm一个字段被定义为一对索引和一个组件。 对于任何排序，比方说Field，括号中的排序，比方说[Field]，表示包含该排序和在子排序包含顺序中与之相关的任何其他排序的相应种类。不能给出排序的有意义的表达，例如，7/0，有一种。例如，非法的索引-组件对将是[Field]类型的表达式。PreRecord是一个可能为空（null）的字段的多重集合，由联合运算符形成，它被声明为关联（asynchronous），可交换（commutative），并将null作为其标识（id）。然后Maude将应用所有的方程和规则模这样的方程公理[11]。请注意，条件成员资格（cmb）将记录定义为没 有 重 复 字 段的 “ 封 装 ” 预 记 录 。记录继承意味着我们总是可以将具有更多字段的记录视为具有更少字段的记录的特殊情况。例如，一个记录的环境组件由env索引，而存储组件由st索引，这可以看作是只包含环境组件的记录的一个特例。匹配模结合性、可交换性和身份支持记录继承，因为我们总是可以使用一个额外的变量PR排序PreRecord来匹配记录可能具有的任何额外字段。 比如说，提取环境组件的函数get-env可以定义为：eq get-env（{env：E，PR}）= E.并将应用于具有PR匹配的任何额外字段的记录。第二个关键的模块化技术是抽象接口的系统化使用。也就是说，指定关键语法和语义实体（例如，Program，Store，Env）的排序是抽象排序，我们：• 只指定操作它们的抽象函数，即抽象排序和函数的给定符号或接口;在抽象排序没有关于这些函数的公理;• 在语言的具体化中，没有具体的句法或语义分类与抽象分类相一致：它们总是被具体化为相应的抽象分类的子分类，或者被抽象子映射到抽象分类;只有在这种具体分类的层次上，关于抽象或辅助函数的公理才被具体化。这意味着我们对句法或语义实体的本质不作先验的本体论承诺。这也意味着，由于所做的承诺总是发生在具体种类的层面上，人们永远可以自由地在任何语言中引入新的含义和结构C. Braga，J.Meseguer/Electronic Notes in Theoretical Computer Science 117（2005）393401nn扩展名.第三种模块化技术涉及规则的形式。我们要求重写理论RLi中的重写规则是语义规则n（t1，. ，t），u∈ −→ u ∈tJ，uJ∈如果C，其中f是语言特征，例如，if-then-else，u和uJ是记录表达式，u包含一个PreRecord类型的变量PR，代表未指定的附加字段，允许规则通过记录继承进行匹配。此外，在u，u，j和C中出现的任何记录表达式中，都应遵循以下信息隐藏原则：除了基本记录syn- tax之外，只有出现在某些记录字段的抽象接口中的函数符号才能出现在记录表达式中;任何辅助函数定义为这些领域的具体组成部分永远不应该被提及。这种信息隐藏使得规则具有高度的可扩展性，因为辅助语义实体的具体表示可以在根本不改变规则的情况下被改变或扩展。这三种技术的结合可以极大地帮助语义定义模块化和易于扩展。也就是说，我们可以用这种方式为语言L开发模块化增量语义定义，作为重写理论包含的偏序集索引层次{RLi=（Ei，Ei，φi，Ri）}i∈I，完整的语言定义作为层次中的顶层理论，而包含RECORD的理论CONF作为层次的底层。通过遵循上述方法，这样的模块化定义将比不遵循这些方法更容易扩展。我们通过第4节中两个案例研究来说明这种易扩展性。我们方法的一个重要变体是选择重写逻辑的MEL子逻辑作为定义语言语义的逻辑框架这给了我们代数语义作为重写逻辑语义的特殊情况。当然，在这种情况下，语义不再由重写规则给出，而是由以下形式的条件方程给出n（t1，.，t），u_j =u_t_J，u_J_j若C.这个变体使我们的模块化技术也可用于代数语义。事实上，正如在引言和[28]中所解释的那样，重写逻辑语义的最佳方法是将刚才描述的模块化语言规范方法的等式和重写变体结合起来这在重写逻辑上下文中是最自然的，因为它明确区分了方程和规则。它允许我们使用正确的公理402C. Braga，J.Meseguer/Electronic Notes in Theoretical Computer Science 117（2005）3931n我对于每个功能：确定性功能的方程，并发性功能的规则3.1控制条件正如4.1节中的CCS例子所示，有时人们对为编程语言给出一个非常详细的“小步”语义感兴趣。在这种情况下，在规则的条件下控制重写的步骤的数量请注意，在重写规则中，Q−→QJ，如果P1−→PJ我... Pn−→PJ，由于重写逻辑的重显性和传递性推理规则（见第2节中的图1），条件中的重写Pi-→PJ相当一般：它们可以有零个、一个或多个重写步骤。关键是，根据定义，在重写逻辑中，所有无穷计算总是可导出为序列。假设我们想给一种语言一个我们如何在一般情况下实现这一点？我们提出了一种方法，将工作的任何重写理论指定根据我们的模块化方法：(i) 我们将模块CONF扩展为系统模块（重写理论）：mod RCONF是对CONF的扩展。op {_，_}：[Program] [Record] -> [Conf][ctor].op[_，_]：[Program] [Record] -> [Conf][ctor].vars P P '：Program. vars R R '：记录。crl[step]：<如果{ P，R} => [ P '，R' ]，则P，R> =<> P '， R' >。恩德姆(ii) 每个语义重写规则的形式是，{t，u} −→ [tJ，uJ]如果{v1，w1} −→ [vJ，wJ]. <${v，w} −→[vJ，wJ]<$C，1 1nnn n（二）其中n≥0，C是一个（可能是空的）仅涉及方程和成员的方程条件。注意，重写理论R只包含RCONF和以下形式（2）将是这样的，任何重写的证明R v，w − →vJ，wJ可以表示（直到[6]中定义的证明的等式等价）为等式和相关性推理规则的应用，或者表示为C. Braga，J.Meseguer/Electronic Notes in Theoretical Computer Science 117（2005）393403n反复应用（如果n= 1，则不应用）传递性规则（见第2节）来证明形式的重写v，w vn−1，wn−1，w=wvJ，wJ，（三）其中序列中的每个重写通过将替换推理规则应用于步骤规则并通过相等来获得。当然，步骤规则的任何这样的应用都精确地模仿了在其条件下使用形式为（2）的规则的一步重写，因此序列（3）是无限次计算。当然，我们现在有了一种本质上更有表现力的方式来控制条件中的步骤数量，这样我们就不局限于用一步重写条件来指定条件规则。例如，我们可以指定一个规则，它在第一个条件中需要一个步骤，在第二个条件中需要一个或多个步骤，在第三个条件中需要零个或多个步骤（x是排序变量Program，y是排序变量Record）：JJ{f（t 1，.，tn），u}−→[t，u]如果J J J J J J J{v1，w1} −→[v1，w1]x，y。4模块化重写语义的实践布丁好不好，吃了才知道。方法学的实际应用必须通过令人信服的案例研究来证明。在这里，我们讨论两个非常不同的例子：CCS [29]和BC。GNU bc语言本质上是C语言的一个子集，非常适合Linux发行版中的数值计算，因此是一种真正的中等规模的语言。关于使用我们的方法的另一个重要案例研究，即并发ML的重写逻辑语义，可以在[7]中找到。4.1CCS的模块化重写语义我们在我们的框架中为CCS [29]提供了一个简单的语义。我们的规范有两个特点值得注意。首先，它不需要对CCS进程的语法进行任何扩展，而在之前的CCS重写逻辑规范中使用了一个超级排序来扩展进程排序的额外语法来处理跟踪[19，41]（我们处理的是记录中的跟踪）。 其次，我们的语义规则是非常普遍的可扩展性。我们通过扩展到弱转换语义来说明这一点，其中404C. Braga，J.Meseguer/Electronic Notes in Theoretical Computer Science 117（2005）393忽略无声的相比之下，传统的CCS处理需要为弱转换定义一个新的关系（表示为“x”），而[41 ]中的扩展虽然是模块化的，但需要额外的语义规则来显式地处理弱等价本身（我们在记录中以等式的方式识别等价迹）。我们的规则形式中隐含的另一个可扩展性方面是，可以很容易地将全新的特性（如命令式构造）添加到CCS中，而不需要对我们的语义规则进行任何更改。这对于标准SOS规则（见[29]中的第2.5节）和[41]中的规则指定CCS语义的主要模块是CCS-SEMANTICS。由于我们对小步长语义感兴趣，因此第节中的模块RCONF3.1是进口的在语义实体的记录中有两个字段：一个是动作的跟踪，索引为tr，另一个是环境，索引为env，保存进程名定义的上下文（可能是递归的）。跟踪组件使用ACTION-LIST模块中的动作列表，而环境组件使用称为上下文的过程定义集，并在CCS-CONTEXT模块中定义。我们的Maude动作、过程和上下文语法遵循[41]。关键模块当然是CCS-SEMANTICS，我们稍后将其扩展为WEAK-CCS-SEMANTICS。fmod ACTION正在保护QID。排序标签法。子分类Qid<标签<法。op tau：-> Act.op ~_：Label -> Label [prec 10].eq ~ ~ l：标签= l：标签。endfmfmod PROCESS正在保护ACTION。排序ProcessId进程。子排序Qid进程。op_._ ：Act Process -> Process [prec 25].op _+_：Process Process -> Process [asshopprec 35]. 操作_|_ ： Process Process -> Process [asktop prec 30].op_[_/_]：进程标签标签->进程[prec 20]。op _\_：Process Label -> Process [prec 20].endfmC. Braga，J.Meseguer/Electronic Notes in Theoretical Computer Science 117（2005）393405fmod CCS-CONTEXT是PROCESS的扩展。sort Context.op _=def_：ProcessId Process -> Context [prec 40].op none：-> Context.op_&_：Context Context -> Context [ascurrentid：none prec 42]. opdupl：[Context] -> [Bool].var x：ProcessId。var p p'：Process. var c：上下文。等式dupl（x =def p&x =def p&' c）=真。endfmfmod ACTION-LIST正在保护ACTION。对ActList进行排序。subsort Act ActList。op：ActList ActList -> ActList [ctoraslogid：mt]。endfmmod CCS-SEMANTICS保护CCS上下文。包括RCONF。保护动作列表。对跟踪环境进行排序。subsort过程<程序。子排序跟踪环境<组件。ops tr env：-> Index.op nil：-> Trace.* 抽象接口op _;_：Trace Act -> Trace。* abstract interface opdef：[ProcessId] [Env] -> [Process]. * 抽象接口op[_]：ActList-> Trace [ctor].* 具体排序强制op{_}：[Context]-> [Env][ctor]。* 具体排序强制varsl m：标签.var a：Act.vars p p ' q q'：过程。varx：ProcessId。var t：Trace.var e：Env.var c：上下文。vars al '：ActList.vars pr pr ' pr''：PreRecord.406C. Braga，J.Meseguer/Electronic Notes in Theoretical Computer Science 117（2005）393mb（tr：t）：字段。mb（env：e）：字段。cmb {c}：如果dupl（c）=/= true，则为Env。方程式[al]; a =[al a]。ceqdef（x，{x =def p &c}）= p if {x =def p &c}：环境* 前缀rl{a. p，{（tr：t），pr}}=>[p，{（tr：t; a），pr}]。* 求和crl{p +q，{（tr：t）， pr}}=>[如果{p，{（tr：nil），pr}}=>[p '，{（tr：nil ; a），pr'}]。* 组成crl {p| q，{（tr：t），pr}} =>[p'|q，{（tr：t ; a），pr'}]如果{p，{（tr：nil），pr}}=>[p '，{（tr：nil ; a），pr'}]。crl {p| q，{（tr：t），pr}} =>[p'|q'，{（tr：t ; tau），pr'}]如果{p，{（tr：nil），pr}}=>[{q，{（tr：nil），pr'}} => [q '，{（tr：nil ;（~ l）），pr'}].* 限制crl{p\ l，{（tr：t），pr}} => [（p如果{p，{（tr：nil），pr}}=>[p '，{（tr：nil ; a），pr'}] /\ a = / = l / \ a = / = ~ l。* 重新标记crl{p[m/ l]，{（tr：t），pr}} => [（如果{p，{（tr：nil），pr}}=>[p'，{（tr：nil;l），pr'}]。crl{p[m/ l]，{（tr：t），pr}} => [（如果{p，{（tr：nil），pr}}=>[p ' ， { （ t r ： n i l ; （ ~l ） ） ， p r ' } ] 。crl{p[m/ l]，{（tr：t），pr}} => [（如果{p，{（tr：nil），pr}}=>[p '，{（tr：nil ; a），pr'}] /\ a = / = l / \ a = / = ~ l。* 定义crl{x，{（tr：t），（env： e），pr}}=>[{p，{（tr：nil），（env：e），pr}}=>[p '，{（tr：nil ; a），（env：e），pr'}]. 恩德姆注意在最后一个规则的条件中使用了在Maude 2.0中，可以在等式条件中引入新变量（然后用语法：=写作，称为匹配等式），只要等式的左侧是一个模式（变量或构造项），其新变量在简化为规范形式后通过匹配右侧来实例化。这个例子说明了我们的方法的三个关键点。第一点是使用记录继承来使规则具有通用性，C. Braga，J.Meseguer/Electronic Notes in Theoretical Computer Science 117（2005）393407尽可能的可扩展。请注意，在语义规则中，我们保留了这样一种可能性，即在CCS的语言扩展中，通过对那些可能的额外字段使用排序为PreRecord的变量，可以将新字段添加到记录中;同样，在条件规则中，我们保留了这样一种可能性，即在未来的扩展–adding for example imperative features to CCS processes– when computinga subexpression of a process expression some of those extra fields could bemodified,第二点是，具体语义排序相反，它们总是被指定为相应的子类型，响应抽象排序，或者，如本例中所示，由子映射到抽象排序。在本例中，我们使用了op[_]：ActList-> Trace [ctor].* 具体排序强制op{_}：[Context]-> [Env][ctor]。*具体排序强制第二个强制类型的使用表明它是一个部分函数，因为只有当一个进程名没有两个不同的定义时，一个环境才是良好类型的。实际上，这个要求是由一个条件成员资格强加的，在它的条件中使用了辅助谓词dupl（也是一个部分函数）。第三，密切相关的一点是严格遵守信息隐藏原则，根据该原则，任何出现在语义规则中的记录表达式在本例中，抽象接口由函数op nil：-> Trace.* 抽象接口op _;_：Trace Act -> Trace。* abstract interface opdef：[ProcessId] [Env] -> [Process]. * 抽象接口这是语义规则中使用的唯一函数：规则中从未提及ACTION-LIST或CCS-CONTEXT模块（定义语义实体的具体排序）中的函数遵守这些原则是模块化可扩展性的关键假设现在我们想为CCS定义一个弱转换语义，其中τ步变得不可观察。 在CCS理论中，这被标记为转换P=aPJ，所有这些转换都是在之前或之后观察到的行动;行动扩展几乎是微不足道的，完全模块化：我们只需要引入一个新的构造函数，从ActList到Trace，对应于这些新的跟踪，其中τ步被忽略，并定义它们的跟踪等价性408C. Braga，J.Meseguer/Electronic Notes in Theoretical Computer Science 117（2005）393并通过两个简单的方程给出了抽象的“右对称”函数的意义。mod WEAK-CCS-SEMANTICS是扩展CCS-SEMANTICS。op<_>：ActList -> Trace [ctor]. * concept sort coercion varsal ' ： A c t L i s t .var a：Act.等式 = al al' >。等式; a = 。恩德姆请注意，语义规则中不需要任何更改事实上，在WEAK-CCS-SEMANTICS模块中，原始转换语义和弱转换语义都是可用的：它们只依赖于为记录选择的初始状态。如果我们想根据原始的转换语义用进程P进行计算，初始配置将具有以下形式：，对于e，过程定义的所选环境。相反，如果我们想用弱转移语义进行计算，我们将使用初始配置），（env：e）}>。请注意，这两个初始配置在语法上都不同于<实际上这个例子的所有规范http://formal.cs.uiuc.edu/meseguer/modular。4.2模块化重写bc的语义在本节中，我们将讨论我们的技术在GNU bc语言的三种不同语义规范中的应用：标准重写语义，带有物理单元注释的语言扩展，以及等式语义。我们用样本规范片段来说明这些想法bc的三种语义的完整模块化规范可以在文件bc-rules.maude、units.maude和equational-bc.maude中找到在http://formal.cs.uiuc.edu/meseguer/modular网站。C. Braga，J.Meseguer/Electronic Notes in Theoretical Computer Science 117（2005）393409GNU bc语言是一种任意精度的计算器语言，其语法基本上可以被视为C语言的子集。递归阶乘函数的以下定义说明了函数定义的bc语法。public int findDuplicate（）{if（x<=1）return（1）; return（f（x-1）*x）;}在bc-rules.maude中我们对bc的模块化重写语义规范中，记录有两个主要组件：环境和存储。因此，bc中的变量只是变量标识符到存储位置的环境绑定。1应用信息隐藏原则，使得在语义规则中仅提及抽象函数，确保了以下的实际细节(i)如何创建新的内存位置;（ii）位置例如，指定赋值和变量求值的含义的语义规则利用基于环境和存储的可扩展存储器模型（这稍后用单元扩展来说明）的抽象数据类型的接口中的抽象函数本体论承诺（一）商店和环境的抽象分类。下面的Maude规则指定了SV：SimpleVar = E：Expr的求值，它是对表达式（E：Expr）求值产生的值的非数组变量（SimpleVarcrl

下载后可阅读完整内容，剩余1页未读，立即下载