理论计算机科学电子笔记127（2005）71-86www.elsevier.com/locate/entcs高级替换单元的终止与模型转换*保罗·博托尼a，1曼努埃尔·科赫b，2弗朗切斯科·巴黎-普雷西切a，d，3加布里埃尔·坦策c，4一Universit`adiRomaBFreieUiversitéatBerlin-GermanyCTechnischeUniversitéatBerlin-GermanyD乔治梅森大学-美国摘要可视化重写技术，特别是图形转换，越来越多地用于通过图形语句来建模系统的转换。已经提出了几种重写模型，在规则类型的表达性和重写机制的复杂性方面存在差异，但其中许多模型的形式属性的基本结果仍然缺失。在本文中，我们提出了一个贡献解决终止问题的重写系统与外部控制机制。 特别是，我们得到的结果更普遍的有效性，通过扩展的概念，转换单元的高层次的替换系统，一个推广的图转换系统。对于高级替换单元，我们陈述并证明了基于终止准则的几个抽象性质。然后，我们用属性图转换系统实例化高级替换系统，并给出具体的终止准则。这些被用来显示一些替换单元的终止，这些替换单元需要表达作为软件重构的结果的模型转换。保留字： 变换单元，图变换，终止，重构。*欧洲共同体在RTN Segravis1 电子邮件地址：bottoni@di.uniroma1.it2电子邮件：mkoch@inf.fu-berlin.de3电子邮件：fparisi@ise.gmu.edu4电子邮件地址：gabi@cs.tu-berlin.de1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2004.08.04872P. Bottoni等人理论计算机科学电子笔记127（2005）711介绍视觉重写技术越来越多地用于通过图解语句来建模特定系统的转换。研究人员正在从语言的静态方面（通过解析过程定义）的具体化转向其动态建模。特别是，图变换是一种广泛的形式主义，应用于解析，模型动画或变换。此外，一系列新的问题，如软件或模型演化[17，15，3，14]，都是由于UML作为软件和通用系统的规范化工具的不同而产生的当指定这样的变换时，很难使用单一的、非结构化的图重写系统来定义复杂的变换。一个典型的问题是将转换的进程引导到图的一些定义良好的配置，即系统的状态。这可能涉及规则应用的某些序列的定义，以及防止将同一规则重复应用于同一比赛，或防止相同应用序列的循环重复。一般来说，保证重写过程的这些性质等同于证明其终止性，这是一个统一版本的不可判定问题[16]，但可以对单个重写系统进行研究，遵循经典的方法，即通过在某些多重集上构造单调测度函数来证明终止性，并表明这种函数的值在每次应用时都会减少，如Dershowitz和Manna在[6]中介绍的那样。由于需要规则表达性，这个问题变得更加复杂。实际上，在单个步骤的重写关系的固有表达性（和复杂性）与引导重写过程的外部控制机制的可用性之间总是存在权衡。虽然已经提出了一些重写模型，不同的规则类型的表达性和重写机制的复杂性，这些模型的形式属性的基本结果仍然是失踪的。属性规则和转换单元的组合使用- ING规则表达式似乎提供了一种转换方法，它已经可以实际使用，但它是足够简单的形式推理。在本文中，我们首先研究属性规则的一个更抽象的版本，即高级替换系统[9]，我们将转换单元的概念扩展到其中[13]。因此，我们得到了一个抽象的属性，一个功能必须满足，以便被用作终止标准，这样的单位。特别是，第2节介绍了相关工作，而第3节采用了转换单元的概念来定义高级替换单元。在第4节中，一个来自软件转换的激励性例子，即重构，P. Bottoni等人理论计算机科学电子笔记127（2005）7173提出了第5节讨论了高级替换系统的终止准则，并给出了一些具体的终止结果。这些都说明了提出一些示例转换，其中替换单元用于指定转换的UML模型随之而来的软件重构。最后，在第6节中给出了结论。2相关工作Kreowski和Kuske在[ 13 ]中引入了变换单元，并且从那时起，变换单元被广泛地用于所有类型的visul变换形式。Küster等人已经考虑了转换单元在定义UML模型转换中的作用[14]。特别是，他们研究了终止和连续的问题。认识到，如Plump在[16]中所证明的，图重写的终止一般是不可判定的，他们提供了一些直观的考虑，尽可能长时间地迭代使用某些给定规则的转换单元的终止或非终止的原因然而，他们没有提出的结果迭代的序列的规则，我们提供了一些终止标准在这里。图变换的终止准则已经被Aßmann [1]考虑过了，他坚持一组具体的准则，并没有像我们在本文中所做的那样，发展出一种基于准则的通用终止已经在几个场合中提出了用于视觉变换过程的管理的负应用条件、设置节点和控制表达式的组合使用。在[5]中，应用分层条件来确保解析过程的终止。我们可以观察到，证明给定变换单元的终止性的一般问题如何等价于引入某种形式的局部分层，使得在图中消除或插入元素的条件根据所采用的单调函数的减少或增加而进行。然而，需要考虑的是，我们在这里感兴趣的不是解析过程，而是一般类型的转换。在[2]中也考虑了这种情况，其中使用转换单元来定义OCL的语义3高级替换单元高级替换系统[9，7]是一般图变换方法的实例，基于变换单元的定义[13]。由此产生的概念被称为高级替换单元。它的语义由所有可能的派生序列的集合给出。此后，通过属性图转换实例化高级替换单元。74P. Bottoni等人理论计算机科学电子笔记127（2005）713.1高级替换单元设CAT是一个范畴，它有一个可区别的态射类M定义3.1[规则]A规则ep：L←lI→rR由两个态射l和r的M.设L（p）是规则p的左手边，R（p）是规则p的右手边。变换单元通过由规则名称上的表达式指定的一组控制条件来控制规则应用。定义3.2[控制表达式]控制表达式的类CN ames（表示一组规则名称）递归定义为：• 我是詹姆斯·詹姆斯，•C1;C2∈ C，如果C1，C2∈C，且• asLongAsPossibleCend∈ C，如果C∈ C.操作符asLongAsPossibleC的预期含义是表达式C的（顺序）应用，只要其应用是可能的。定义3.3[高级替换单元]高级替换单元范畴CAT中的RU=（P，name，C），或者仅仅是替换单元，由规则的有限集合P、双射函数名P→N ames和N ames上的控制表达式C∈C组成。高级替换单元是[13]意义上的单元：我们有一个图转换方法，包括CAT中的对象类，该类别中的规则类，定义3.4中定义的应用运算符，定义3.2中定义的一类控制表达式和一类图类表达式，它们是CAT本身中的对象类。 替换单元是以CAT的对象作为初始图和终止图的变换单元。此外，高级替换单元的导入单元集始终为空。与转换单元相反，高级替换单元的语义由派生集定义。定义3.4[匹配和直接推导]给定一个对象G和一个规则p：L←lI→rR，p到G的一个匹配是一个态射m：L→G。 直接通过p和匹配m从G到H的导数d，d：G<$p，mH，由下式给出：双推出（见图1）。 start和end是从direct对象的派生，使得start（d）=G，end（d）=H。一个派生id：Gpid，mG，称为恒等式。 给定一组规则P，Der（P）={G ∈p，mH|G，H ∈Obj（CAT）<$p ∈ P}是所有具有规则集P的直导子的集合.P. Bottoni等人理论计算机科学电子笔记127（2005）71752我，我我 R（1）（2）JJG，gDH HFig. 1. 双重推出方法定义3.5[推导序列]给定一组规则P，P上的推导序列由函数s：N →Der（P）定义，其中start（s（i+ 1））=end（s（i）），其中i≥0。如果s（i）是恒等式推导<$i > n，则推导序列s的长度为n，end（s（n））称为推导结果。两个长度为m -和t -的导出序列s-的级联st<备注。 如果t的长度为n，则连接是有限的，并且u（m+i）=t（i−1），其中0 F（R（p）），则p的终止准则。从和中删除C中F的值的原因是它包含A和B的公共元素，否则将被考虑两次。即使在定义5.1中，我们认为p是双重推出方法中的一个规则，我们也只涉及它的左手边和右手边。因此，在M类的适当定义下，同样的定义也可以用于单推出方法。我们在这里只为DPO方法发展理论，但将勾画出关于SPO具体标准定义的推论。命题5.2（直接推导）如果F是规则p的终止准则，那么它也是所有d的导出规则pd的终止准则：G<$pH。我的律师。由于F是规则p的最终标准：L←lI→rR我们F（L）> F（R）。对于每个直接导子G∈rH，如图1所示，我们需要F（G）> F（H）。从F（L）> F（R），我们有F（L）+F（C）−F（I）> F（R）+F（C）−F（I），即F（L+IC）> F（R+IC），即F（G）> F（H）。因此，F是导出规则的终止准则Ghpd：G←C→H。Q派生规则的特定实例的终止准则可以用作规则的终止准则，如以下定理所示82P. Bottoni等人理论计算机科学电子笔记127（2005）71命题5.3（导出规则的终止）如果F是d：G <$p H的一个导出规则p d的终止准则，则它是规则p的终止准则。L r证据 设p为规则p：L ← I → R。如果F是一个终止标准，Gh导出规则pd：G←C→H则它必须保持F（L）+F（C）−F（I）=F（L+IC）=F（G）> F（H）=F（R+IC）=F（R）+F（C）−F（I）。因此F（L）> F（R）且F是p的终止准则。Q定义5.4[终止表达式]给定CAT中的替换单元RU=（P，name，C）和N ames上的表达式E，如果F是CAT的终止准则，则F是E的终止准则，并且(i) 若E=name（p）∈Names，则F（L（p））> F（R（p））;(ii) 若E=E1;E2，则对d∈der（E）的每个导出规则pd，F（L（pd））> F（R（pd））;(iii) 如果E=asLongAsPossibleEJend，则对于d∈der（EJ），F（L（pd））> F（R（pd））.命题5.5（序贯合成）如果F是E1和E2的终止准则，那么它也是E = E1; E2的终止准则。证据 若F是导子 d1：G <$H ∈ der（ E1） G的导出规则pd 1和导子d2：H<$K∈der（E2）H的导出规则pd 2的终止准则，则F（G）> F（H）且F（H）> F（K）.因此F也是所有导子d∈der（E）G的导子规则pd的终止准则注意，相反的情况是不正确的，因为可能存在不是组件之一的终止标准的组合的命 题 5.6 （ 尽 可 能 长 的 循 环 ） 如 果 F 是 E j 的 终 止 准 则 ， 它 也 是 E =asLongAsPossibleEJend的终止准则。证据 若F是导子 DJ：G <$H ∈ der（ EJ） G 的 每 个 导 子 规 则 pdj 的 终 止 准 则，则F（L（pdj））> F（R（pdj））. 尽可能长地应用EJ，我们得到一个导子序列s：N→der（EJ），其中F（start（s（i）>F（start（s（i+1），i≥0。由于N没有无限降序序列，因此必须存在一个m∈N，使得对于j >m，F（start（s（j）））=F（start（s（j+1）））=F（end（s（j），使得s（j）是恒等式推导，即，der（E）终止。Q定理5.7（导子终止）P ∈ P中规则上的导子序列是终止的，如果存在一个对所有p ∈ P成立的终止准则F。P. Bottoni等人理论计算机科学电子笔记127（2005）7183证据给定任何导子序列s：N →Der（P），由于命题5.2，我们知道对于i≥0，F（start（s（i）> F（start（s（i+1）。因此，必须有一个m∈N使得对于j> m，s（j）是单位导数，也就是说，der（E）中的所有推导都是终止的。Q定理5.7的结果在下面的推论中适用于使用控制条件的替换单元。推论5.8（置换单元的终止I）给定置换单元RU =（P，name，C），der（C）中的所有导子终止，如果存在对所有p ∈ P成立的终止准则F。证据 定理5.7的直接推论。Q下面的定理表明，终止准则在整个控制表达式上不需要是唯一的。定理5.9（替换单元的终止II）如果C的每个asLongAsPossible子表达式CJ具有终止准则F，则替换单元RU =（P，name，C）终止.证据 证明是通过归纳表达式C的结构：(i) 基本步骤：C是一个规则名：在这种情况下，由于每个规则应用程序都终止，因此RU也终止。(ii) 诱导步骤：• C=C1;C2通过归纳假设，C1和C2都定义了有限导子序列der（C1）和der（C2）的集合;因此der（C1;C2）也只包含有限导子。• C=asLongAsPossibleCJend根据归纳假设，CJ有一个终止准则F，根据命题5.6，它也是C的终止准则。因此，RUtermi-nates。Q因此，定理5.9指出，如果对于C的每个asLongAsPossible-子表达式，存在合适的终止准则，则替换单元是终止的。重要的一点是，这些标准可能因子表达式而异。84P. Bottoni等人理论计算机科学电子笔记127（2005）71S5.2属性图变换现在我们说明如何自然地从图中计数元素中产生的一些函数可以用来建立终止的标准定义5.10 [具体的终止准则]设n：G → N是返回G中节点数的函数，即n（G）= |GN|，并且e：G → N是计算G中的边的数目的函数，即e（G）= |GE|，对于类别ASSIG-Alg中的每个图G。 如果s是SG中的排序，则函数ts：对于ASSIG-Alg中的每个图A，G → N产生ASG中的元素数。我们表明，N，E，和TS可以被用来作为终止条件内的类别ASSIG-Alg。命题5.11函数n、e和ts，对于每个s∈SG，满足定义5.1中的终止准则。证据本文证明了函数n（G），e（G）和ts满足两个态射a：C→A和b：C→B上的推出构造的条件，其中a∈M，b是任意的，所以当b∈M时，它更是成立的。这是定义5.1所要求的。由于a的图部分是单射的，推出构造仅在图C的元素处粘合图A和B，通过分别对节点和边取B和不在a下的C的像中的A的部分的不交并，即D=B（A−a（C））。 因此n（D）=n（A+CB）=n（A）+n（B）−n（C），e（D）=e（A+CB）=e（A）+e（B）−e（C），并且对于每个s∈SGS，ts（D）=ts（A+CB）=ts（A）+ts（B）−ts（C）.Q对于SPO方法中的任何规则p，除了简单的节点和边的计数外，还可以通过考虑函数Fp（G）来获得具体的准则，该函数Fp（G）计算G中p的左侧L的匹配和部分匹配的数目。类M在这里被认为是部分态射m的类使得如果i=j，则m（i）m（j）。因此，我们考虑部分态射L→R，由规则p给出，匹配L→G。推出结构产生图H作为应用p的结果。现在，如果Fp（L）> Fp（R），我们有Fp（H）=Fp（G）+Fp（R）−Fp（L），因此H对于p的完全匹配或部分匹配比G少。这意味着在每次应用p它的未来可能应用的数量减少了，因此它只能在有限的时间内应用，因为原始图G是有限的。5.3示例UML重构第4节的替换单元即将终止。实际上，我们只需要检查completeRefactoring的终止性，以获得任何可能的类选择P. Bottoni等人理论计算机科学电子笔记127（2005）7185和attr，因为这是唯一要循环的规则每次应用此规则时，都会删除一个变量类型的节点（以及将其连接到Class和Type类型的节点的边）。因此，节的函数n和e5.2可作为终止标准，证明该子单元终止6结论终止性是模型转换的一个重要问题在双推出方法中通过图变换对它们进行建模的优点是它们被精确地定义并且可以被形式化地分析。本文研究了图变换系统的终止性问题，提出了一个高级替换系统的一般终止准则，它是图变换系统的推广。由于模型变换可能变得复杂，我们不仅考虑单个规则的应用，而且考虑替换单元，其中规则应用根据附加控制流程受到限制。对于控制流程的描述，我们允许应用单个规则，规则表达式的顺序组合本文包含了一些结果，有关终止更换单位。我们计划以几种方式扩展所提出的结果，例如研究控制表达式的额外运算符，例如。可选的规则应用、if-then-else表达式、优先级等。通过这样做，我们可以表明，用于图解析的分层图变换的终止将是我们框架的结果的特殊情况。分层图变换系统可以被认为是高级替换单元的特殊情况，其中控制表达式是每个应用一组规则的尽可能长的循环的顺序组合此外，我们计划研究更广泛的标准，以建立终止的顺序组成的规则。此外，我们希望考虑负面应用条件（NAC）。在[12]中已经介绍了用于图变换的NAC，并且已经证明在将图变换应用于实际问题时是有用的最近（[8]），它们已被纳入高级替换框架。我们希望在此基础上制定替代单位的最终结果，同时考虑到NAC鸣谢我们感谢匿名审稿人和Kathrin Ho Muslimmann对本文前一版本的几个有用的意见86P. Bottoni等人理论计算机科学电子笔记127（2005）71引用[1] Aßmann，U.，图重写系统的程序优化，ACM TOPLAS22（2000），页。583-637.[2] Bottoni，P.，M.科赫，F。Parisi Presicce和G. Taentzer，OCL约束的自动一致性检查和可视化，在：UML 2000 -统一建模语言（2000），pp. 294-308.[3] Bottoni，P.，F. Parisi-Presicce和G.Taentzer，《集成重构与分布式图变换》，在：具有工业相关性的图变换应用，LNCS3062（2004），第3062页。220-235[4] Bottoni，P. ，P. Parisi-Presicce 和G. Taentzer，“Coherent Refactoring of Software Artefactswith Distributed Graph Transformations” ， P.v.Bommel ， 编 辑 ， Transformation ofKnowledge，Information，and Data：Theory and Applications（2004）。[5] Bottoni，P. 、白藓G. 塔恩茨和A。[10]张文龙，《基于文本对分析的图形化语言的研究与应用》，载于：北京大学出版社，2000年。59比61[6] Dershowitz，N.和Z. Manna，用多集排序证明终止性，Commun。ACM22（1979），pp.465-476[7] Ehrig，H.，M. Gaublsky和F. Parisi-Presicce，应用于代数规范和Petri网的高级替换系统，在：图形语法手册和图形变换计算。2003：Concurrency，Decelism and Distribution，World Scientific，Singapore，2000 pp. 341-400[8] Ehrig，H.和A. Habel，约束和应用条件：从图到高级结构 ，在：Proc.Int.Conf.on GraphTransformation 2004，2004，即将出版。[9] Ehrig，H.，A. Habel，H. J. Kreowski和F. 高级替换系统中的精确性、并行性和并行性。Struc. 在Comp.Science1（1991），pp.361-404[10] Ehrig，H.，联合Prange和G. Taentzer，类型化属性图变换的基本理论，在：Proc。Int. Conf. 在2004年的图表转换上，2004年，出现了。[11] Fowler，M.，K. Beck，W. Opdyke和D. Roberts，[12] Habel ， A. ， R. Heckel 和 G. Taentzer ， Graph Grammars with Negative ApplicationConditions，Fundamenta Informaticae26（1996），pp. 287-313[13] Kr eowski，H. -J. 、S. KuskeandA. SCHUR RR，NestedgraphtrAN SFONUNITS，INT. JournalonSoftware and Knowledge Engineering7（1997），pp.479-502.[14] Ku？ter，J.M.、R.HecelandG.Engels，DefininganddValidatingTrannsforormationsofUMLModels，in：Proc. HCC 2003（2003），pp.145-152[15] Mens ， T. ， S. Demeyer 和 D. Janssens ， Formalising behaviour preserving programtransformations，in：A. Corradini，H. Ehrig，H.- J. Kreowski和G. Rozenberg，editors，Proc.ICGT 02，2002，pp. 286-301[16] Plump，D.，图重写的终止是不可判定的，Fundamenta Informaticae33（1998），pp. 201-209[17] 是的，G。、白藓D. Pollet，Y. L. 我的天啊。-M. J′ez′equel，Ref actori ngUMLmoddel s，in：M. Gogolla和C. Kobryn，编辑，UML 2001 -统一建模语言。建模语言、概念和工具。第四届国际会议（2001年），pp。134-148。
我的内容管理
展开
