理论计算机科学电子笔记156（2006）135-150www.elsevier.com/locate/entcsMaude的SOS元理论原型1Michel A. 雷尼尔2计算机科学系，埃因霍温理工大学（TU/e），P.O.Box 513，NL-5600 MB埃因霍温，荷兰摘要我们提出了一个原型实现SOS元理论的莫德长期重写语言。原型定义了SOS元理论的基本概念（例如，转换公式，演绎规则和转换系统规范）。除了基本的定义，我们还实现了检查某些SOS元定理前提的方法（例如，GSOS同余Meta定理）.此外，我们定义了一个通用的策略，用于在我们的元语言中为语义规范动画化程序和模型。这条研究路线的总体目标是开发一个通用工具，通过检查定义下的语言的有用属性来帮助语言设计者，并提供一个快速原型环境，以便根据定义的语义来仔细检查程序的实际行为关键词：形式语义学，结构操作语义学，术语重写，语言原型，莫德。1引言定义一种语言的形式语义通常是将其带入形式世界的第一步。定义语义的过程涉及许多选择，其中一些是非常隐含的，设计师的肉眼看不到。此外，在定义语义的过程中，通常没有参考点来检查最终结果是否“正确”，以及是否做出了对于一个复杂的语言，它很快就超出了人类的能力，以保持跟踪的结果，设计决策的语义和人们往往可以忽略可能的反直觉现象介绍。证明定理关于1电子邮件：M.R. tue.nl2 电子邮件：M.A. tue.nl1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.09.030136M.R. Mousavi，M.A.Reniers/Electronic Notes in Theoretical Computer Science 156（2006）135直觉属性和检查系统运行的几个实例（根据给定的语义）与直觉是建立关于语义的洞察力和信心的好方法。在本文中，我们报告了一个初步的尝试，实现一个通用的工具，提供了一个语言设计师与上述可能性。我们的原型类型适合于结构操作语义（SOS）[22]，它现在是定义规范和编程语言语义的事实标准围绕SOS的概念已经开发了一套合理的知识体系，旨在证明SOS规范的有用属性[3]。 同余结果[13，5]、导出方程理论[2]和保守扩张[11]是这个方向上最值得注意的元理论。我们的目标是定义一个框架，使我们能够检查SOS规范的上述元定理的简单实例的前提，并进一步允许根据给定的语义来动画规范和程序。Maude项重写语言[1]作为我们实现的基础语言非常方便本文其余部分的结构如下。在第二节中，我们回顾了SOS语言的原型设计和元定理证明的相关工作。之后，在第3节中，给出了作为SOS形式化的转换系统规范的一般定义，并描述了它在Maude中的实现。然后在第4节中定义并实现了一个同余元定理的实例。第5节定义了一个简单的运算保守性定理，并说明了它的实现。第6节致力于动画SOS规格。最后，第7节总结了本文，并提出了我们的原型的几个可能的扩展。2相关工作尽管在SOS元理论领域有大量的知识，但在实施方面却做得很少在[21]中，我们报告了在Maude重写逻辑[1]它被用作特定目标语言的原型仿真和模型检查环境。这个初始原型帮助我们检查并删除了初始语义中的一些“bug”。除了我们以前的实现，其他作者已经研究了重写逻辑[15]和SOS [22]之间相当清晰的联系，无论是从理论[10，15，16，17]还是从实践的角度[8，9，24，26，27]。在[8]中，给出了从模块SOS（MSOS）[18，19]到Maude重写逻辑的转换的概要，并证明了其正确性。翻译相当M.R. Mousavi，M.A.Reniers/Electronic Notes in Theoretical Computer Science 156（2006）135137简单明了，主要的技术转折是将标签分解为源中的配置和转换的目标，这是由于MSOS中标签的结构该翻译已完全实现，有关此实现的详细信息可参见[7]。这项研究与我们的研究之间的主要本文中实现的元定理）和实际普及性。Verdejo在[24]中以及Verdejo和Marti-Oliet在[26，27]中报告了Maude中SOS语义的一些实例的实现我们的方法在本质上非常接近他们的工作，SOS演绎规则被解释为Maude条件重写规则。这种方法被称为重写转换。我们通过以下方式为他们的工作做出贡献：首先，提高抽象的水平，以便人们可以一般地谈论SOS规则，指定和执行它们，并对其进行推理;其次，我们实现了更多的参与在我们的框架中有负前提的SOS案例早期版本（Maude）不支持以重写为条件的条件重写。因此，在[15]中提出了一种不同的方法来实现SOS，称为作为判断的转换。 在该方法中，每个转换被实现为项，并且SOS演绎规则被实现为重写规则，该重写规则将结论中的转换重写为前提中的转换，反之亦然（即，使用自下而上或自上而下的方法构造证明结构这两种方法都是由[15]而前者已在[25]中实施作为重写和判断的过渡在[26]中，据报道，重写方法的转换更容易实现，并且引起的并发症较少。此外，将转换建模为重写允许利用Maude中实现的可用搜索和模型检查库来研究模型的行为LETOS [14]是一个工具，可以从广泛的语义（包括某些形式的SOS）中生成LaTex文档以及Miranda [ 23 ]中的可执行第一次尝试实现SOS元定理，涉及[13]的运算保守性，也在[14]中报道。然而，该实现并没有完全检查该定理，而只是检查源依赖性要求，这是[13]的保守性定理的假设之一。138M.R. Mousavi，M.A.Reniers/Electronic Notes in Theoretical Computer Science 156（2006）135C3过渡系统规格动机转换系统规范（TSS）是在[13]中提出的SOS的形式化在本节中，我们定义了具有常数标签和负前提的TSS概念[12，5]，并在Maude中将其形式化。我们框架的一个自然扩展是支持术语作为标签。基本定义我们假设一个可数无限的变量集V ={X0，Y0，. . }。一个签名函数包含许多函数符号（复合运算符：f，g，. . ），具有固定点（ar（f），ar（g），. . ）.元数为0的函数符号称为常量。过程项的集合，由T（V，V）表示，典型成员s，t，sJ，tJ，在一个签名上归纳定义，变量V. 替换σ用其他项替换项中的变量。如果存在一个替换σ使得σ（t）=s，则项s可以匹配项t（与项t是唯一的）。出现在项t中的变量的集合由vars（t）表示。如果vars（t）=0，则项t是闭合的。一个转换系统规范（TSS）是一个元组（A，V，L，D），是签名，V是一组变量，L是一组标签，D是一组演绎规则。对于所有lll∈L，且s，SJ∈ T（V，V），我们定义s→lsj，且s~l分别是正公式和负我们把s称为源的两个公式和SJ作为目标的积极的。一个演绎规则dr∈D，被定义为一个元组（H，c），其中H是一组公式，c是一个正公式。公式c称为结论和公式从H开始称为前提。具有空前提集的规则称为公理。演绎规则（H，c）由H表示。替换和匹配的概念被提升到公式中。Maude的形式化标签和变量分别被定义为标签和变量。标签由用户定义，但我们将标签视为常数（可能具有某种代数结构）。基本参数X- n和Y- n是为自然数索引的变量Xn和Yn签名将根据规范进行定义签名中的函数符号例如，二元运算符+可以定义为OP+：T T -> T [ctor]，其中T是这类术语的给定名称，ctor代表构造函数。替换和匹配已经为变量定义，并且必须由用户提升到术语级别。我们预见到了M.R. Mousavi，M.A.Reniers/Electronic Notes in Theoretical Computer Science 156（2006）135139通过在元级检查签名，自动地实现替换和匹配公理Formulaes→lsJ和s~l由表达式s ==l==> sp和s ==1=/=>。TSS是一种函数理论，其参数为：签名、变量和标签。然而，由于Maude当前实现中的一个技术问题（在upModule方法中缺乏对参数化模块的支持），我们将它们实现为纯功能模块。将我们的实现转换为参数化设置的问题是H重命名接口和排序名称。一个演绎规则表示为CH = c和一个集合中的演绎规则用逗号分隔。使用TSS和相关概念的一般实现请注意，这些示例仅用于解释目的，并不一定代表SOS的实际和有意义的实例示例表1显示了我们框架中最小进程代数（MPA）的SOS规范Maude代码是不言自明的，几乎与任何SOS规范中出现的文本相同。 签名由死锁过程的常量delta、一类一元运算符a;对于动作，前缀a是排序BAct的成员（对于基本动作），二元运算符+用于非确定性选择。项的替换、匹配和变量的概念由项的简单结构归纳来定义（这些定义的基本情况一般在模块Term-Match中定义）。演绎规则定义了动作前缀和非确定性选择的操作语义我们的下一个例子是MPA的一个简单扩展，其时序方面如表2所示。在这个扩展中，我们有一个新的标签tick用于时间转换和一个新的一元操作符延迟;这会导致时间转换发生。除了前面规定的演绎规则外，我们还必须增加一些演绎规则来定义延迟算子的行为和选择的时间确定性（参见图10）。[4]），即，如果两个组件中的一个阻塞时间转换，则时间将仅决定非确定性选择为了简化剩下的部分，我们假设TSS140M.R. Mousavi，M.A.Reniers/Electronic Notes in Theoretical Computer Science 156（2006）135fmodMPA-TSS是等式vars（delta）= emptyVars。inc术语匹配。等式vars（act;s）= vars（s）。incTSS-定义。eq vars（s +t）=排序BAct。vars（s）cup vars（t）.对BAct标签进行子排序<。eq match（delta，delta）= emptySbst.*MPA签名eq匹配（（s +t），（sp+tp））=opdelta：-> T [ctor]。（match（s，sp），match（t，tp））.op _;_：BAct T-> T [ctor]。等式match（（act;s），（act;t））= op_+_：T T-> T [ctor]。match（s，t）.* 替换和匹配* MPA op a：-> BAct [ctor]的操 作 语 义 。操作MPA：-> TSS。varact：BAct.当量MPA =varsigma：Sbst.（=vars s t sp tp：T.a;X-0 == a ==> X-0），等式sigma（delta）= delta。（X-0 == a ==> Y-0eq sigma（act;s） =act;sigma（s）.X-0+ X-1== a==> Y-0），等式sigma（s+ t）=（X-1==a==> Y-1sigma（s）+ sigma（t）。===X-0+X-1==a==>Y- ①的人。endfm表1Maude中MPA的结构操作语义fmod MPAT-TSS是（（ X- 0 ==tick=/=>，包括MPA-TSS。X- 1 == tick ==> Y-1）选项tick：-> Labels [ctor]。===opdelay;_：T-> T [ctor]。X- 0 + X- 1 == tick ==> Y- 1），等式sigma（延迟; s）=（（X- 0 == tick ==> Y- 0，延迟; sigma（s）。X-1 ==tick =/=>）eq match（（delay; s），=（delay;t））= match（s，t）.X-0+X-1== tick==> Y-0），等式vars（delay;s）=vars（s）。（（X-0==tick==> Y-0，*MPAT的操作语义X- 1 ==tick==>Y- 1）op MPAT ：-> TSS。===eqMPAT=（MPA，X-0+X-1==tick==>（=Y-0 + Y-（1））。delay; X- 0 ==tick==> X-0），endfm表2Maude中MPA随时间的简单扩张4一个同余元定理动机操作语义学通常会为闭项引入一个标记转换系统，当两个项显示相同的行为时，观察它是有趣的。这种行为等价的概念可以用来确定一个实现在其规范方面是正确的人们非常希望行为等效的概念是成分或技术上M.R. Mousavi，M.A.Reniers/Electronic Notes in Theoretical Computer Science 156（2006）135141L这是一个很好的例子。在文献[3]中已经提出了几个同余元定理。这些元定理保证了如果语义的演绎规则符合某种句法标准，则特定语义上的行为等价概念是一个同余在这里，作为一个例子，我们选择了一个实际有用的例子，这样的元定理，从[5]并在我们的框架中实现它我们实现的元定理保证了特定TSS的（强）双相似性基本定义如果TS_S_spJ，wedenteitbyytssp→lpJ(see第6节“证明过渡”的确切含义给定TSStss，闭项上的对称关系R是互模拟关系，当lJlJ J Jq（p，q）∈Rl，pJtssp→pqJtssq→q（p， q）∈R. TWO闭项p和q是双相似的，记为pParticipateq，当存在一个互模拟关系R使得（p，q）∈R。项上的等价关系R是一个同余关系，当对所有函数符号f∈R，对所有项pi，qi∈T（R，V）（0≤iar（f）），如果（pi，qi）∈R，对于所有的0≤i
TSS。incTSS-定义。eq测试=* 签名（=业务处a b：-> T [ctor]。ft（a）== l ==> ft（a））。op ft_：T-> T [ctor]。endfmop l：-> Labels [ctor].表3一个简单的违反GSOS格式的前提在它们的源和目标中只包含正确类型的变量使用元级函数，我们的实现变得独立于签名的选择以及定义和使用的变量集。所实现的GSOS检查方法将TSS的名称（类型Qid）作为参数，从相应的功能模块读取TSS的签名，检查规则的一致性，并输出一个声明肯定结果的字符串，或者输出一个不符合GSOS格式的示例考虑表2中给出的MPAT的TSS以下语句显示了如何检查MPAT与GSOS格式的一致性以及此检查的结果（对MPA应用类似的命令会产生类似的结果）。GSOS-Check中的Maude>红色：GSOS-Chk（'MPAT-TSS，MPAT）。在GSOS-Check中减少：GSOS-Chk（'MPAT-TSS，MPAT）。rewrites：211 in 30 ms cpu（80 ms real）（7033rewrites/second）结果消息：successmsg（“全球安全观测系统检查：TSS符合全球安全观测系统。“）现在，考虑表3所示的TSS。在此TSS上应用GSOS检查会导致以下错误消息。GSOS-Check中的Maude>红色：GSOS-Chk（“Test-TSS，Test）。在GSOS-Check中减少：GSOS-Chk（'Test-TSS，Test）。rewrites：49in0 ms cpu（0 msreal）（~rewrites/second）结果消息：errormsg（“GSOS-Check：Error，the followingrule：“，emFr =ft（a）==l==>ft（a），“在其结论来源“）GSOS元定理仅为双相似性的全等提供了充分（而非必要）条件，但在上述情况下，双相似性确实不是全等：一个Particib，因为它们都没有运算行为，但它并不认为f（a）参与f（b），因为前者可以使一个转换使用上述规则，而后者不能使任何过渡M.R. Mousavi，M.A.Reniers/Electronic Notes in Theoretical Computer Science 156（2006）135143015操作保守性动机使用功能模块的概念，我们可以在新模块中包含SOS规范，并使用新的功能符号，新的标签和新的演绎规则对其进行扩展确保这种扩展是保守的，即，它们不改变旧术语的操作行为在这一节中，我们制定了一个简单的操作保守性元定理的例子（通过限制它的GSOS框架），并解释其在Maude中的实现。基本定义为了扩展由TSS定义的语言，可能必须将前签名与新签名组合。然而，并不是所有的签名都可以组合成一个，因为功能符号的特性可能会冲突。为了防止这种情况，我们定义两个签名是一致的，当他们同意共享函数符号的arity考虑一致的TSStss0与tss1的扩张，记为tss0<$tss1，定义为（ 0<$1 ，V0<$V1 ， L0<$L1 ， D0<$D1 ） 。 如 果 <$p∈C （ <$0 ） <$pJ∈C （ <$0<$$>1 ）<$l∈L0<$L1tss0<$tssp→lpJ惠tssp→lpJ，则tss0<$tss1是操作保守的TSS0的扩展。下面的定理是[11]中提出的一般定理的简化定理5.1（GSOS的运算保守性）考虑在GSOS中一致的TSSGSOS格式。 tss0 <$tss1是tss 0的操作保守扩展，如果对于所有演绎规则d ∈ D1，以下条件之一成立：(i) d在结论的来源中有一个从101\ 100开始的勒伊杰(ii) d有一个正的前提xi→ yi，其中lij∈ L1\L0.Maude的形式化这个元定理的形式化与同余元定理的形式化是相同的。首先，我们编译一个列表中的功能符号和标签的扩展和扩展TSS的，然后检查扩展TSS的演绎规则，要么包括一个新的功能符号的来源的结论或一个新的标签在至少一个积极的144M.R. Mousavi，M.A.Reniers/Electronic Notes in Theoretical Computer Science 156（2006）135例如检查MPA（表1）随时间（表2）延长的保守性如下。CONSV检查中的Maude>红色：Cons-Chk（'MPA-TSS，MPA，'MPAT-TSS，MPAT）。在CONSV检查中减少：Cons-Chk（'MPA-TSS，MPA，' MPAT-TSS，MPAT）。rewrites：14in0ms cpu（0ms real）（~rewrites/second）result消息：successmsg（“CONS-Check：操作守恒定理检查成功。“）在非保守性扩展上尝试相同的例程会导致错误消息，该错误消息指出已经违反的演绎规则和保守性定理的假设6动画SOS动机尽管SOS规范具有可操作性，但通常无法执行。如[5]所示，对GSOS的轻微扩展很容易破坏证明转换的可判定性。为了增加复杂性，在[12]中表明，并非所有SOS规范都是有意义的，因为它们可能根本不定义过渡关系，或者它们可能模糊地允许多个过渡关系。如果把全球安全观测系统作为一个框架，就可以免除这些麻烦。我们的动画方法不需要TSS在GSOS中。然而，倘TSS被严格及有限度地分层（GSOS规格包括在内），则其保证终止并产生良好结果接下来，我们精确地定义了从TSS可证明的转换意味着什么，以及这个概念如何在Maude中形式化基本定义一个正闭公式φ可从一组正公式T和一个转移系统规范tss（记为（T，tss）φ）中证明，当且仅当存在一个良基向上分支树，其节点被标号通过封闭公式，• 根节点由φ标记，并且• 如果一个节点q的标号，记为q，是一个正公式，并且{q i|i ∈ I}是直接在q上的节点的标签的集合，那么有一个推论{χ i|i ∈ I}规则χ以吨计（N.B.χi可以是正公式或负公式）和一个代换σ使得σ（χ）=π，且对所有i∈I，σ（χi）=πi;• 如果一个nodeq的label，detdbys~l，是一个负公式，M.R. Mousavi，M.A.Reniers/Electronic Notes in Theoretical Computer Science 156（2006）135145我existsnosJsuchthats→l sj∈T。一个稳定的模型，也称为过渡关系，由一个过渡系统规范tss定义，是一组公式T，使得对于所有封闭的正公式，φ，φ∈T当且仅当（T，tss）<$φ. A跃迁s→lSJ可证明自tss，denotedbyytsss→l jnts会导致一个唯一的表格模型，s→lSJ∈ T。确保TSS定义唯一的转换关系的一种方法是通过下面的分层概念转移系统规范tss的分层是从闭合正公式到序数的函数S，使得对于以下形式的tss的所有演绎规则{t→li TJ|i∈I}{t ~lj | j ∈ J}iijt→ltJ使得对于所有闭置换σ，我们有（1）对于所有i∈I，S（σ（ti→litJ））≤S（σ（t→LTJ））和（2）对所有llj∈J和TJJ，S（σ（tlj tJ）） ) )=>（（sigma，rho）（target（conc（rule）如果（rule， tssp）：=tss/\sigma：=match（conc（rule），（s==l==>））/\（tss||-（sigma（prem（rule）=> rho/\（（sigma，rho）：：Sbst）/\（closed（（sigma，rho）（target（conc（rule）。在上面的代码中，crl代表条件重写，它将箭头=>之前的项重写为之后的项，前提是if子句指定的条件成立在这种情况下，重写箭头之前的项由所考虑的TSS（tss）、源（s）和转换的标签（l）重写箭头之后的项是匹配演绎规则（rule）的结论的目标，其中替换（sigma，rho）将通过应用于它的上述过程来构造。在重写规则的条件部分中，首先，使用模式匹配从TSS中挑选任意规则然后，检查是否存在与规则的源和s匹配的替换sigma。接下来，检查是否可以构造替换rho，以便满足规则的前提（将在剩余部分中进一步解释如果可以找到这样的替换，它将评估规则结论目标中的所有变量。在这里，我们省略了（非纯的，因此，非GSOS规则）的情况下，得到的替代不评估所有变量的目标的结论规则。我们区分以下两种情况，以检查[ 13 ]《易经》中的“道”和“道”，都是有道理的对于不具有这种性质的TSSM.R. Mousavi，M.A.Reniers/Electronic Notes in Theoretical Computer Science 156（2006）135147演绎规则如果前提是一个肯定的前提，那么检查就是从源中寻找一个与前提的目标相匹配的转换。匹配替代sigma然后用于评估其余的前提。CRL（TSS||-（s ==l==>t））=>sigma，如果（TSS|-（s ==l==>））=>sp/\sigma：= match（t，sp）。如果前提是否定的，我们使用元级方法metaRewrite来检查是否可以使用相同的重写理论找到矛盾的重写（转换）注意，对负前提的检查并没有添加 任 何 关 于 正 在 构 造 的 替 换 的 信 息 。 因 此 ， 重 写 的 结 果 是 空 替 换（emSbst）。同样，在这两种情况下，我们省略了专门用于前提链断裂的情况的重写规则（即，规则不是纯的），并且在所评估的前提中不能找到具有闭源的转换CRL（TSS||-（s ==l=/=>））=>（emSbst），如果可能吗：= metaRewrite（upTerm（（tss|-（s == l ==>），1） /\（可能吗？：：ResultPair）。上述过程，在终止时，为我们提供了一个完整的转换证明然而，一般来说，该过程不需要终止。考虑以下两个SOS规范。a==l==> a a==l=/=>- -a==l==> a a==l==> aMaude工具在尝试对上述两个TSS中的任何一个进行动画处理时崩溃，因为该过程导致无限重写链，每个重写都是下一个重写的条件。然而，这个问题不会发生在GSOS规范中，并且通常不会发生在严格和有限分层的TSS中因此，条件重写检查转换的深度而且，这种搜索的广度总是有限的，因为我们只能指定有限个规则，每个规则都有有限个前提。如果证明搜索在所有前提下都成功，它为我们提供了一个替换，该替换对演绎规则的目标中的变量进行赋值，因此，我们能够使用演绎规则的结论的标签和赋值目标来找到术语s的值得一提的是，该过程是非确定性的，148M.R. Mousavi，M.A.Reniers/Electronic Notes in Theoretical Computer Science 156（2006）135可以是闭项s的几个可证明的转换。Maude语义具有对非确定性重写理论的固有支持，因此在这样的转换中的选择仍然是非确定性的，并且最终由Maude重写引擎做出。使用Maude工具可以浏览可证明的转换，检查特定转换的可证明性，甚至使用逻辑公式（线性时态逻辑（LTL）公式）来模型检查转换和运行的属性。例如考虑表1的TSS MPA。我们可以动画化a;（（a;delta）+ delta）项的转换，如下所示。Maude> rewin TSS-Animation：（MPA）|-（a;（a; delta + delta）== a ==>））。在TSS-Animation中重写：MPA|-a;（a; delta + delta）== a ==>。重写：13 in0 ms cpu（0 msreal）（~重写/秒）结果T：a; delta+ delta7结论和未来扩展在本文中，我们提出了一个初步的尝试，实现SOS元理论在莫德。我们的实现定义了一个带有常量标签的基本SOS框架此外，它允许动画SOS规格。对于我们的实现来说，Maude是一个非常方便的选择特别是，重写和转换之间的对应关系简化了从SOS到Maude的翻译。Maude的相对语义在我们的实现中至关重要。随着Maude提供的元级工具的逐步改进，我们期望更容易和更有效的实现为了把这个原型变成一个全方位的SOS工具，我们预见了以下可能的扩展：(i) 实现更通用的SOS框架及其相应的元定理：有更通用的SOS框架，允许术语作为标签，多排序和绑定签名。实施这样的框架增加了我们的工具的适用性。此外，我们在本文中实现的元定理是最简单的版本中的可用元定理的同余和操作保守性。通过将SOS框架扩展到更一般的设置，实现更一般的元定理，如[20，11]的元定理将是有益的。M.R. Mousavi，M.A.Reniers/Electronic Notes in Theoretical Computer Science 156（2006）135149(ii) 生成合理的和完备的方程理论：我们在本文中没有讨论的一类Meta定理涉及从SOS规范生成方程理论（例如，参见[2]）。这些Meta定理也有算法的性质，可以在我们的框架中实现。(iii) 生成自然语言文档（可能还有研究论文！）从特定的语义。(iv) 自动生成项匹配和替换定义：为了检查同余和运算保守性元定理，我们使用了从理论中提取函数符号定义的例程使用类似的例程，我们可以自动化替换和匹配过程，并使SOS规范的Maude代码更加紧凑。(v) 构建图形用户界面并从通用输入格式（例如，XML）。致谢StevenEkerandPacoDuran提供了有关Maude的几个问题的提示和信息AnaSokolova对这份文件的初稿作了有益的评论感谢SOS研讨会匿名评论者的深刻评论引用[1] Maude系统 可从http://maude.cs.uiuc.edu/。[2] L.阿塞托湾Bloom和F. W.凡德拉格把SOS规则变成等式。I C，111（1）：1[3] L. Aceto，W. J. Fokkink和C.维尔霍夫结构操作语义学。在Handbook of Process Algebra，第3章，第197-292页中。Elsevier，2001年。[4] J. C. M. Baeten和C. A.米德尔堡带定时的进程代数。EATCS各论。施普林格，2002年。[5] B.布鲁姆，S。Istrail和A. R.迈耶互模拟是无法追踪的。JACM，42（1）：232-268，Jan. 一九九五年[6] R. Bol和J.F. 格鲁特过渡系统规范中负前提的含义JACM，43（5）：863[7] C. D. O. Braga.重 写 逻 辑 作 为 模 块 化 结 构 操 作 语 义 框 架 。 PhDthesis ，DepartamentoodeInform'tica ， Pontif'ıciaUniversidadeCat'olic a deRio de Janeiro ， Brasil ，2001.[8] C. D. O. Braga，E. H. Haeusler，J. Meseguer，and P. D.苔藓将模块化SOS映射到重写逻辑。在LOPSTR'02的会议记录施普林格，2002年。150M.R. Mousavi，M.A.Reniers/Electronic Notes in Theoretical Computer Science 156（2006）135[9] C. D. O. Braga，E. H. Haeusler，J. Meseguer，and P. D.苔藓Maude action tool：使用反射将动作语义映射到重写逻辑。在AMAST'00会议记录斯普林格，2000年。[10] P. Degano，F. Gadducci和C.普拉米通过重写逻辑实现CCS的因果语义。TCS，275（1-2）：259[11] W. J.Fokkink和C.维尔霍夫保守地看待变量绑定的操作语义。I C，146（1）：24[12] J. F.格鲁特具有负前提的过渡系统规范。TCS，118（2）：263-299，1993.[13] J. F. Groote和F. W.凡德拉格结构化操作语义与互模拟一致性。I C，100（2）：202[14] P. H.哈特尔LETOS -一个轻量级的操作语义执行工具。 软件，实践与经验，29（15）：1379[15] N. 我的天啊-我的天啊。Meseguer. 重新写入日志icalogi In哲学逻辑手册，第9卷，第1Kluwer，2002年。[16] J. Meseguer。作为并发统一模型的条件重写逻辑。TCS，96（1）：73-155，1992.[17] J. Meseguer和C.Braga. 程序设计语言的模块化重写语义 在AMAST'04会议录Springer，2004.[18] P. D.苔藓在结构化操作语义学中利用标签。Fundamenta Informaticae，60（1-4）：17[19] P. D.苔藓 模块化结构操作语义。 J.J.，60-61：195[20] M.R. Mousavi，M.J. Gabbay，and M.A.雷尼尔高阶过程的SOS。在Proceedings of the 16thInternational Conference on Concurrency Theory （ CONCUR308-322. Springer-Verlag ，2005.[21] M.穆萨维，M。Sirjani和F.阿巴布组件连接器的规范和验证。技术报告CSR-04-15，埃因霍温理工大学计算机科学系，2004年。[22] G. D.普洛特金操作语义学的结构化方法。2004年，June，60-61：17[23] D. A.特纳Miranda：一种多态类型的非严格函数语言。在Proceeding of the ACM Conferenceon Functional Programming Languages and Computer Architecture中，LNCS第201卷，第1-16页。Springer，1985年。[24] A. Verdejo。Maude中LOTOS符号语义的构建工具。在FORTE'02的Peoceanology施普林格，2002年。[25] A. Ver d ejondN. 妈的-撒谎。我在找CCSINMAUDE。参见FORTE/PSTV'00的出版物Kluwer，2000年。[26] A. Ver d ejondN. 妈的-撒谎。在马来西亚，有两种电磁兼容性标准：CCS和LOTOS。系统设计中的形式化方法，27（1）：113[27] A. Ver d ejondN. 妈的-撒谎。在Maude中执行可执行的任务。TechnicalReport134-03，
我的内容管理
展开
