软件系统层次结构的类型证明与重构

理论计算机科学电子札记109（2004）97-109www.elsevier.com/locate/entcs形层次建筑设计2丹·赫希·乌戈·蒙塔纳里Dipartim medInformatica，Uiversita`diPisa，ViaF.Buonarroti 2，I-56127，Pisa，Italia1摘要软件系统的体系结构设计处理高层次的配置结构。检查一个系统是否属于软件架构风格（或形状）意味着该架构是一个结构定义类的实例。另一方面，层次结构允许在不同的细节层次上建模：子系统可以表示为单个组件来抽象结构和行为。本文提出了一种基于类型的方法表示层次SA形状使用类型。类型证明定义了一个基于推理规则的一般框架，其中形状规则和表示系统的图形是类型判断。层次构造函数在类型系统中定义，用于构造捕获层次结构的证明项。我们认为，证明项提供了更多的信息，而不仅仅是关于构造系统的过程的图形，并且允许将重构指定为证明项重写。重构的一致性是通过主题约简获得的：只要剪切和粘贴类型证明仍然产生类型证明，主题约简就得到保证。作为一个可能的实例化的方法，我们提出的形状（和层次结构）的类型系统与全局引用。关键词：软件体系结构风格，层次结构，可重构，类型系统，系统重构1引言软件系统的架构设计是处理用于构建软件产品的配置和规则定义的高层结构的活动[7]。为了满足基于架构的开发对形式化符号和工具的需求，提出了架构描述语言（ADL）[12]。描述的两个相关方面1 电子邮件：dhirsch@di.unipi.it，ugo@di.unipi.it2 研究部分由欧盟FET-1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.05998D. 赫希大学Montanari/Electronic Notes in Theoretical Computer Science 109（2004）97软件体系结构是风格检查和层次组合[12]。本文中提出的正式方法围绕这些方面展开，并且正在欧盟项目AGILE [1]的背景下开发风格（或形状）检查意味着一个架构是某种软件架构（SA）风格的实例，它表征了一类展示公共模式的一个风格可以被看作是一个给定架构的类型。将样式的概念概括为一种类型，从现在开始，我们使用形状这个名称来表示用于类型系统的规则。这个术语来自于基于类型化编程语言指针的数据结构的图语法，其中类型的声明不足以描述（和验证）更复杂的结构，如双向链表或叶连接树。提出了一种用类型表示层次化软件体系结构形状的方法。类型证明定义了一个基于推理规则的一般框架，其中形状规则和表示系统配置的图形表示为类型判断。因此，如果有一个判断的类型证明，那么系统是正确的形状（即类型），其中类型系统的公理是样式的成形规则与形状密切相关的一个方面，我们可以做出贡献，是SA重新配置。重建必须尊重形状，即类型. 但是对于设计来说，仅仅观察实际配置可能是不够的。相反，观察获得最终系统所采取的步骤可能会提供有关施工过程的重要信息。在这一行中，我们主张证明项（即，编码类型证明的规则名称的术语）提供了更多的信息，而不仅仅是关于构建系统的过程的图形，并允许将重构指定为证明术语重写。然后，重构一致性作为主题约简获得：只要剪切和粘贴类型证明仍然产生类型证明，主题约简就得到保证。此外，我们的方法允许形状和层次结构的集成层次组合允许在不同的细节层次上描述系统从总体上看，在与系统配置相关的许多方面都存在层次结构。大规模系统开发、全球计算、广域网等，引入了用分层结构表示系统可能有用的要求。层次结构可以表示嵌套的位置：站点，代理，位于不同位置的管理域等层次结构存在于几个领域，如过程演算（环境演算[4]），并发系统建模（双图[13]），UML（例如分解和细化的状态图）。在我们的例子中，层次结构是通过类似于基本常量的层次构造函数来捕获的然后，对于每个分层构造函数，标准的D. 赫希大学Montanari/Electronic Notes in Theoretical Computer Science 109（2004）9799判断 层次图可以在结果类型系统中派生。总之，我们的目标是应付SA的建模问题。类型系统和结构的线性表示的使用允许利用现有的编程语言和静态类型检查的工作的希望。此外，该方法中的所有元素都有相应的图形视图作为一个可能的实例的方法，我们提出了一个类型推理系统的形状层次结构和全局引用。从[8，9]的一些初始思想，判断描述图和形状规则（图重写规则），层次构造器被类型化为规则，体系结构通过类型化证明导出。相关工作：我们已经提到了指针结构的形状。纸[2]提出了图归约（GR）规范来指定指针数据结构（形状）的类别。GR规则是反向图文法的产物。在[6]中，提出了上下文无关图文法来建模形状类型。两者都提出了算法测试成员和分析其复杂性问题。这些文件处理的形状在编程语言的背景下，一些结果可能是相关的，我们的方法以及。与[6]相关，我们提到[11]的工作，这是第一个为SA风格提出上下文无关的图文法。在[15]中报告了SA重构的图转换工作。 他们提出了一个两级的方法，使用程序设计语言来表示状态和计算，并使用基于类别的代数框架来表示体系结构和重新配置。这些工作与我们的方法的总体目标有关。与层次有关，我们提到了[5]关于层次图变换的工作。在[5]中，引入了特殊的超边，称为框架，包含层次图或变量，允许定义可以在单个步骤中复制和删除子图的规则。每一层次都被独立地处理，层次之间的关系被定义为新的态射。 为此，通过递归地构造推出和态射，将图变换的双推出[14]方法扩展到历史图。此外，它们还提供了一个重命名操作，其中每个级别中的帧都被其内容替换。 等级制度是严格的，不允许跨界。 在这一行中，[10]的工作集成了层次结构和形状，其中边和节点是层次结构的，形状（上下文无关规则）用于输入层次结构。类型是为必须对应于形状的变量定义的。在这些作品中，双重推出理论被重新定义为处理层次结构。这些论文将层次结构作为新的边和节点类型的形状。在我们的例子中，我们使用层次结构构造器来证明，而不是在底层图中需要额外的结构。这种方法更抽象，因为层次和形状可以直接从100D. 赫希大学Montanari/Electronic Notes in Theoretical Computer Science 109（2004）97类型证明和间接从图。保持样式的图变换（即，重构）在我们的方法中通过良好类型的证明项重写规则来实现，而在其他方法（特别是[11]）中，重构必须明确证明是正确的。此外，我们试图通过依赖于为普通图重写和编程语言的类型理论开发的大量概念，尽可能少地重新发明分层图变换及其类型化技术。此外，我们的目标是提出一个框架，可以根据SA感兴趣的问题进行实例化，而上述论文的重点是编程语言。2运行实例作为运行示例，我们使用机场案例研究[1]。基本情况如下。在机场有乘客和飞机。飞机在机场之间运送乘客和他们的行李。在这里，我们采取了一个简单的视图的例子，一个清晰的介绍。我们集中在关于位置的类上，这些类定义了层次结构。国家可能有机场，机场可以容纳飞机和乘客。3成形分层系统本节介绍使用类型表示样式的方法。将样式的想法一般化为类型，我们使用名称shape（[2，6]）作为一类图（表示样式的实例）的特征化，这类图是从称为shape规则的图上的一组重写规则（即，指定系统类型的规则）。然后，类型证明定义了一个基于推理规则的通用框架，可以实例化产生不同的类型系统，从而为某些特定的设计问题选择最方便的解决方案。类型系统是通过对表示形状和图形的类型判断的推理规则来定义的。因此，如果存在代表系统实例的判断的类型证明，则系统是正确成形的（即，类型），其中类型系统的公理对应于风格的形成规则。此外，我们得到了一个统一的线性表示- tation类型判断（包括层次结构），我们认为适合分析，连同适合建模的图形表示。3.1超图与句法判断系统配置表示为超图[14]。超边对应于组件或模块，它们的连接节点是它们与其他组件或模块的通信端口或连接一个超边缘，D. 赫希大学Montanari/Electronic Notes in Theoretical Computer Science 109（2004）97101。。。►|∈|| |或者简单地说是边，是具有标签的原子项（来自排序字母表LE ={LEn}n=0，1，... ）和许多（有序）的触角作为其标签的排名。一组节点和一组这样的边构成一个超图（或简单的图），如果每条边通过它的触角连接到它的附着节点。一个图配备了一系列由不同名称标识的外部节点外部节点可以看作是图与其环境（即上下文）。图在本文中被认为是同构的。 例如，在我们的案例研究中，图2a。 示出一个国家，两个机场，每个机场内有一架飞机，第二个机场有一名乘客，他的行李和机票。它有一个边界，包括行李、护照、飞机票、护照、行李和机票。 所有位置都有一个到节点的索引来标识它们（向上）和其他用于识别这些红外线的通道。c^untry有一个TENTACLTOANODTOCONNECTITISAIRPORTSANDA^IRPORTHASONEFORPLANEANDON EE ORARASSENGERS. 飞机具有与其位置和机上乘客连接的连接点（在图2的飞机没有乘客的情况下）。乘客有一个识别他身份的标签，并与他的位置相关联，一个标签指向他的出发国，两个标签指向行李和机票。请注意，带行李和车票的乘客形成一个图，并且不是分层的（图是分层结构中的叶子）。正如您所看到的，对于位置层次结构，对国家的引用是全局的。此外，在图2B中。您可以看到导出图的位置的等效我们代表超图以及从一组公理和推理规则生成的句法判断。对应证明可以在[8]中找到。然后，一个图被描述为一个判断ΓG，其中节点对应于名称，外部节点表示Γ中的名称（自由名称）。项G包含形式L（x1，. ，xn），其中xi是名称，LLE和运算符将两个共享节点的图放在一起。关于我们添加了运算符以允许对名称进行限制。 正式定义：定义3.1[作为句法判断的图]设N是一个固定的有限名称集合，LE是一个排序的标签字母表。一个句法判断（或简单地说一个判断）的形式是：（图的接口），G是由文法生成的项G：：=L（x）G|G是的。Gnil，其中x是名称的向量，L是一个具有rank（L） =x，y是名称的广义子。 设fn（G）不等于G的所有自由名的集合，即G中所有不受运算符约束的名字对于范围限制，v.我们要求fn（G）<$r。定义了零上运算的结合性、交换性和恒等式的结构公理，以及关于限制名的α转换公理，并给出了nv、nil和 nil 之 间 的 相 互关系。|：vx. 是的。你好vx. Gνx G<$Gifx∈/fn（G），102D. 赫希大学Montanari/Electronic Notes in Theoretical Computer Science 109（2004）97►►vx. 你好G[y/x]若y∈/fn（G），νx. （G1）|G2）n（νx. G1）|G2，如果x∈/fn（G2）.Fig. 1. 图形和句法判断。例如，图1示出了具有两个dg es和lab elsairport和pass的图和对应的判断。N_d_x是可见的，并且t（w_i）是受ν限制的。我们写νX，其中X=xi，来表示νx1.νx2. vx n.利用α转换公理和ν公理，对于任何判断，我们总是有一个等价的标准形式ΓνX.G，其中G是只包含边的平行合成的子项。 r和X是不相交的。 Γnil对应于没有边的图。我们使用符号Γ，x来表示将x连接到Γ，假设x/∈ Γ，并且Γ 1，Γ 2是Γ 1和Γ 2的连接。(a) 衍生图。（b）层次图（c）构造器(d)形状规则。图二. 机场案例研究。D. 赫希大学Montanari/Electronic Notes in Theoretical Computer Science 109（2004）971033.2全局参考类型系统我们的目的是提出一个一般结构的推理规则，但空间的限制，在本文中，我们直接提出了一个可能的实例，允许处理全局引用。 这个例子也显示了该方法比超边替换更通用，并且特别与形状和层次的集成相关。层次结构可以被视为一个严格的结构，其中嵌套意味着元素不能知道同一级别之外的其他元素，即。没有全局引用。尽管如此，许多编程语言允许全局引用，并且像UML这样的架构或设计语言使用全局引用。首先，我们将形状规则和图形定义为判断。为此，我们将判断的概念扩展到类型判断（第3.2.1节），方法是添加二阶变量并定义类型变量和判断 推理规则的形式为JR，其中J、R和RJRJ是类型判断，其中RJ是在R中替换J的结果。然后，给定一组判断作为形状的公理，导出的判断及其类型证明定义了形状的实例。框架中的每个类型系统实例化都包含一个推理规则和一组公理（第3.2.2节）。一般来说，我们定义一个类型系统如下：定义3.2[类型系统]类型系统TS=被定义为公理A的一组类型判断和判断上的推理规则I一个证明项是判断名称的组合如果存在生成证明项的类型化证明，则证明项是良好类型化的因此，当我们说证明项时，我们指的是标准证明项3。3.2.1类型判断图项包含边（如定义3.1）和变量，这些变量作为占位符（对于其他图）连接一些节点（如边）。图形和形状规则是类型判断。基本类型标识非终结符，变量表示规则和使用它们的派生图中出现的非终结符实例。类型和变量根据非终端触手的数量进行排名。定义3.3[基本类型和变量]我们定义了一个固定的排序类型集合NT，其中对于T∈NTn，rank（T）=n;以及一个排序变量集合V ar，其中X：T∈V ar表示X具有类型T∈NT，rank（X）=3每个带括号的证明项对应于一个唯一的类型证明。104D. 赫希大学Montanari/Electronic Notes in Theoretical Computer Science 109（2004）97N∅| | ≥。。。。rank（T）. 变量以小写字母书写为了简单起见，我们重载函数rank。我们定义了一个特殊的类型ε用于分型图。变量不能是ε类型。在我们的例子中，我们需要定义图2d中的形状规则（如下所述）。下面的基本类型集合：NT ={C，A，PI，Pa，Ma，Mpl，Mpa}。定义3.4[类型判断]让是一组固定的名称，NT是一组固定的排序类型，V是一组排序变量。类型判断的形式为S=Γ，T∈G：Ts，其中，(i) S是判断的一个名称，而Γ∈ N是一个不同名称的序列(ii) n是一个变量序列，其形式为X1：T1，.，Xn：Tn，对于G项中出现的所有变量.变量都是不同的。(iii) G是由定义3.1中定义的语法生成的项加上v ariabl es：G：：=X（y）L（z）G|Gvx. Gnil，其中hrank（X） =rank（TX）=|y|。(iv) Ts∈NT<$ε是完全判断的结果型。对于形式为Γ，G：Ts的判断，非终结图对应于/=和Ts=ε，终结图对应于=和Ts=ε。 对于形状规则（s=L→R）（即，（图重写规则）的解释如下：类型Ts∈NT对应于L中的非终结符，而Γ，G是图R的句法判断。 这里，R1是由规则生成的新非终结符的变量序列（规则和判断的对应取决于变量的重命名和排序）。序列Γ包含具有Γ秩（Ts）的外部节点，其中对于具有全局引用的形状规则需要大于（参见3.5节和下面的规则乘客）。在R中只有终端的规则对应于=。在这个表示中，变量在G中的出现都是不同的。两条边可以有相同的（非终结符）标签（即相同的类型），但它们被认为是不同的实例（即不同的变量）。我们对节点名和变量使用序列，因为我们需要匹配节点并识别变量的顺序以构建证明项。X，X：TX表示X是序列的最后一个变量。1，例如，图2d.显示了形状规则和初始图形，形状中的图形是从 这些规则生成位置的树结构。例如，对某些规则和初始图的判断是：defdef^Init = x，X：CX（x）：εCountry = x，X：Ma v w.country（x，w）|X（w）：Cdef^Airport= x，X：Mpl，Y：Mpa v w 1，w 2.airport（x，w 1，w 2）|X（w 2）|Y（w 1）：AdefPassenger= y，x <$v w 1，w 2.pass（x，y，w 1，w 2）|行李（w 1）|ticket（w 2）：Pa位置之间的包含关系定义了一个嵌套结构。规则D. 赫希大学Montanari/Electronic Notes in Theoretical Computer Science 109（2004）97105| |||国家，机场和飞机创建层次结构。乘客创建一个乘客实例及其行李（为简单起见，我们只放一个）和机票。其余的规则创建了一些机场，飞机和乘客4。图2a.显示了从这些规则导出的图表。我们不显示空间限制的推导为了简单起见，按照ap-在文献中对于形状的方法[6，11]，只要有可能，我们就以上下文无关的风格呈现规则（即，左手边的一个非终结符），几乎没有扩展来处理全局引用。3.2.2推理规则下面的推理规则显示了两个判断的合成，通过用J替换R中的变量X，结果得到一个新的判断RJ。定义3.5[全局引用推理规则]设R和J是两个类型判断，那么我们定义一个推理规则，J=y，x，1H：AR=y，r，2， X：Avw. G|X（z） ：CRJ=y，r，n2，n1nvw. G|Hz/x：C|=rank（A）x（Γw）=|=rank(A)x˜∩(Γ∪w˜) =∅判断J表示形状规则，并且它在R中替换最后一个变量X，该变量必须具有与J相同的类型（即，A）。判断J是一个规则，其中A是一个左撇子，它产生了一个规则，其中x是规则的一个子序列（即， rank（A）=rank（X）=|X轴|）的。判断一下R对应于一个图或一个规则（取决于C是否为ε），包含一个带符号A的非终结边。由此产生的判断RJ（以名称连接RJ作为证明项）通过在R中用图H替换变量X而获得。 这是通过连接来自R和J（X除外）的变量X2，X1，并通过在R的图形项中将X的实例替换为H的子项x{\displaystylex}来完成的。你可以把它当作正常的参数和z来处理这是一个事实。 显然，x=z，因为z代表的是在H被嵌入的情况下，对坐标x的不确定性。 没有人能在这座城市里找到他。作为一个例子，我们可以构建一个证明（没有全局引用），对应于一个有机场的国家（国家UniA机场）的规则。UniA=x，X：AX（x）：MaContry=z，Z：Mavw. c^un try（z，w）|Z（w）：CC_u_y_U_iA=z，X：A_u_w. c^un try（z，w）|X（w）：CAirport=r，W：Mpl，Y：Mpavw 1，w2。a^irport（r，w1，w 2）|W（w1）|Y（w 2）：AContryUniA=z，X：Avw3. co^un try（z，w3）|X（w3）：C国家UniA机场=z，W：Mpl，Y：Mpavw1，w 2，w3。 co^un try（z，w3）|a^irport（w 3，w 1，w2）|W（w1）|Y（w2）：C4我们假设至少有一个机场，每个机场有一架飞机106D. 赫希大学Montanari/Electronic Notes in Theoretical Computer Science 109（2004）97⊆一当我们处理表示层次结构的判断时，推理规则通过添加一系列由规则R和J所知道的被命名的名字序列来考虑全局引用。N是不是A的秩的一部分，并在H中使用一个引用，该引用是在R的外部C中定义的，与在H的情况下的x的情况无关W将根据R的内部参考文件进行相应的修改。F或 exampl e ， 如 果 我 们 采 用 term （ Airport MultiPa ） 并 应 用 规 则Passenger，则我们有一个机场乘客规则，该规则引用外部节点（证明中的r）标识机场国家（参见图2）。Passenger= r，x <$v w 3，w 4.pass（x，r，w 3，w 4）|行李（w 3）|ticket（w 4）：PaAi rpo rtMultiP a=r，W：Mpl，X：Mpa，Y：P anvw1，w2. a^irport（r，w1，w2）|W（w1）|X（w2）|Y（w2）：A机场MultiPa P assenger=r，W：Mpl，X：MpaP assenger= w 1，w 2，w 3，w4. a^irport（r，w1，w2）|W（w1）|X（w2）|pass（w2，r，w3，w4）|luggage（w3）|ticket（w4）：A由此得到的RJ的C型与R的C型相同。 如果R是一个图，ε，则RJ对应于规则J在R中的非终结图A上的应用，产生一个新的ε型图。 如果R是一个规则，C作为左手边，那么RJ是一个复合新规则，其应用等价于替换R（需要C），然后在A（由R产生）上替换J的结果。例如，上面的证明是规则，但是如果我们将它们连接起来并将结果应用于初始图（我们只显示证明项），那么我们会对非终结图产生判断：正如我们提到的，我们的意图是提出框架的不同实例我们已经提出了一个全局引用，但值得一提的是，如果我们从上述规则中删除全局引用，我们将获得一个对应于上下文无关超边缘替换（HR）的规则[14]。J=x，1H：AR=r，2， X：Avw. G|X（z） ：C|X轴|=rank（A）RJ=r，r2，r1，rvww. G|Hz/x：Cx（Γw）=定理3.6（HR系统的对应性）给定一个HR系统，它有一组产生式P，和一个类型系统TS= A，I><，TS = A，I>具有上述推理规则，并作为对P的判断，那么TS中的证明项和HR中的句法树是一一对应的。3.2.3分层构造器通常，层次结构由包含关系建模，该包含关系被描述为包含可以再次是框的元素的框。在设计或架构层面上的例子是移动系统的子系统或位置我们建议使用层次结构构造函数，它们的类型与形状规则相同也就是说，D. 赫希大学Montanari/Electronic Notes in Theoretical Computer Science 109（2004）97107►Tff图被指定为一个证明项，其中包含一些仅给出类型的构造函数我们可以将判断的类型定义如下。定义3.7[判断类型]给定一个形式为J=x的类型判断，H：我们可以说J的类型是由两个J=x∈，x∈，A，由连接到外点的点的序列x∈组成，它的参数，和它的最终类型A。例如，图2C。 显示位置构造函数Country，类型为5TCountry=rank（x），X：Ma，C其中rank（Ma）=rank（C）= 1。注意我们不要为Country的右边给出一个项，因为对于hierarchy构造器，我们只对包含关系感兴趣。构造器类型表示Country的content6是Ma类型的X，并且其上下文的结果类型是具有一个外部连接的C类型无论如何，如果我们希望能够使用Country来检查一个术语的正确键入，那么我们需要一个判断来构建键入证明。一个标准的选择是从证明项中获得一个层次图的简化版本，其中给出了构造函数的符号定义例如，我们可以用一个等价的扩展规则Countryf来定义构造函数，它与Country具有相同的类型。在这种情况下，注意规则对应于图2d. Edgelabelco^untryisaterminalsymbolthatti niti es语法树中构造函数的每个子树出现的根。再次，图2c.显示了案例研究和图2c的位置构造函数的图形表示。注意规则。然后，图2b.对应于图2a的分层图。使用构造函数。定义3.8[层次类型系统]给定类型系统TS，其公理为A = R <$C，其中R是一组判断，C是一组构造函数，那么我们定义层次类型系统TS，其中TS与TS相同，但公理为A = R <$Cf，其中Cf是C中构造函数的注意规则集。然后，证明项表示TS中的层次图，如果它使用来自C的构造器，并且TSf中的证明可以使用来自Cf的简化版本来获得。以这种方式，任何具有分层构造器的证明项都可以简化为TSf中的判断。 对层次结构的最小化版本的判断与图的5我们使用上下文无关的例子进行简单的解释6一个构造函数类型可以包含多个变量。这意味着一个盒子可以有几个内容，必须完全订购。108D. 赫希大学Montanari/Electronic Notes in Theoretical Computer Science 109（2004）973.3重组在系统重新配置后，有必要检查形状的一致性。为获得最终系统而作出的决定可提供有关施工过程的重要信息。在我们的框架中，这对应于检查证明项。为了以一致的方式重新构造系统，我们提出了证明项重写。一个重构被定义为一个变换规则R=（I<$O）：T，它接受一个证明项I并返回O（两者都是相同类型的T），其中O可以用不同于I的规则构造。给定获得类型证明的模块化方式，我们可以对证明项（包含输入模式）应用转换并获得新的证明。 请注意，转换可以顺序或并行地应用于任何上下文和实例化。重构的一致性是通过检查I和O是否具有相同的类型来实现的：只要剪切和粘贴良好类型的证明仍然会产生良好类型的证明，就可以保证主题归约。示例的 一个简单转换 可以是MinDistance ， 它使用分层 构造器MultiA50（稍后重新定义）更改生产MultiA，指定机场之间的最小距离应该是50公里的约束。MinDistance=MultiAMultiA50：X：Ma，Y：A，Ma4结论和今后的工作我们提出了一个框架，表示层次SA形状使用类型。我们的目标是提供一个正式的基础，以建模和分析系统的层次结构是一个相关的方面，其架构的演变是一个共同的事件。我们有一个适合分析的图形和层次的线性表示该方法可以被实例化以获得更多的表达能力，从而允许选择哪一个是针对某些特定设计问题的最方便的解决方案。对于层次结构，作为未来的工作，我们必须更详细地研究我们已经提到的相关领域，如进程演算[4]和并发系统[13]。同时，在AGILE的背景下，我们将继续我们的工作，支持UML的移动性扩展[3]。我们已经详细地看到了具有全局引用的形状的类型系统，但是还需要继续研究其他可能的实例化。关于形状分析，我们认为指针数据结构的相关工作中的一些结果也可以与我们的方法相关，特别是与定理3.6中所述的超边缘替换的对应关系。最后，值得一提的是，我们相信可以将我们的类型系统翻译成λ-演算：类型判断映射到λ-演算中具有非常相似的术语结构的类型判断。应用D. 赫希大学Montanari/Electronic Notes in Theoretical Computer Science 109（2004）97109推理规则的抽象对应于规则与应用和β-归约一起应用的变量的抽象。因此，它应该是可能的，以获得一个方便的实现在一个功能语言的合适的工具，以支持我们的方法。引用[1] 安德拉德，L.和etal.敏捷：软件架构为迁移率在最近代数发展技术的趋势-第16届国际研讨会，WADT 2002，Frauenchiemsee，LNCS第2755卷。Springer-Verlag，2003.[2] 贝克韦尔，A.，Plump，D.，和Runciman，C.图归约的指针结构。Tech. 众议员YCS-2003-367，Dep.CS，Univ.约克，2003年。[3] Baumeister，H.，Koch，N.，Kosiuczenko，P.，和Wirsing，M. 扩展活动图来建模移动系统。在Intl. Conf. NetObjectDays，2002.修订论文，LNCS第2591卷，第278-293页。SV，2003年。[4] 卡尔代利湖和Gordon，A.移动环境。Maurice Nivat，编辑，FoSSaCSSpringer-Verlag，1998.[5] Drewes，F.，Ho Bertmann，B.，和Plump，D.层次图变换。Journal of Computer andSystem Sciences，64（2）：249[6] Fradet，P. 和LeM′etayer，D.她是我的朋友。InPrinciplesofProgramingLanguages（POPL'97），第27-39页。ACM Press，1997.[7] Garlan，D.和Shaw，M. 软件架构：新兴学科的观点。Prentice Hall，1996年。[8] Hirsch，D.软件架构风格的图形转换模型。PhD Thesis，Dept.计算机科学，布宜诺斯艾利斯大学，2003年5月。[9] Hirsch，D.和Montanari，U.高阶超边替换系统及其变换：可重构软件架构重构。在GRATRA 2000中，Tech.代表：柏林工业大学，2000-02，第215-223页[10] Ho Mushmann，B.形状嵌套图变换的抽象与控制。Fundamenta Informaticae，No. toappear，2003.[11] 我也是，D。描述了使用grapgrama的两种战争历史类型。软件工程学报，24（7），1998年7月。[12] Medvidovic，N.和Taylor，R.软件体系结构描述语言的分类和比较框架。IEEE TSE，26（1）：70[13] 米尔纳河反应系统。在ConsurSpringer-Verlag，2001.[14] G.罗森伯格编辑图文法和计算的图形转换手册：基础，第1卷。世界科学，1997年。[15] Wermelinger ， M. 和 Fiadeiro ， J. A graph transformation approach to software architecturereconfiguration. 计算机程序设计科学，44：133