Alloy建模语言的重构规范

理论计算机科学电子笔记95（2004）227-243www.elsevier.com/locate/entcs重构Alloy规格Rohit Gheyi1，2Paulo Borba3伯南布哥联邦大学巴西累西腓摘要本文提出了一种面向对象的形式化建模语言Alloy的建模规则。这些定律不仅对定义Alloy的公理语义很重要，而且对指导和形式化流行的软件开发实践也很重要。特别是，这些定律可以用来正式重构规范。作为一个例子，我们正式重构了Java类型的规范。关键词：形式化方法，模型转换，重构，模型检测。1介绍编程法则不仅对定义编程语言的公理语义很重要，而且对软件开发过程也很重要。事实上，除了被用作非正式开发实践的基础，如重构[6]，由于像极限编程[1]这样的现代方法学，这些定律非常有助于激励正式开发方法的实际使用。虽然它们还没有被充分研究，建模定律或设计模型定律可能会带来类似的好处，但影响1我们要感谢匿名推荐人提出的几个建议。特别感谢Tiago Massoni和软件生产力小组的其他成员，感谢他们的重要评论。这项工作得到了巴西研究机构CNPq的支持。2 电子邮件地址：rg@cin.ufpe.br3 电子邮件地址：phmb@cin.ufpe.br1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.04.014228R. Gheyi，P. Borba /《理论计算机科学电子笔记》95（2004）227-243可靠性和生产力，因为它们用于软件开发过程的早期阶段。为了探索这一点，本文引入并形式化建模规律。我们还展示了如何使用这些定律来重构Alloy规范。特别是，我们专注于Alloy [13]中项目模型的转换，Alloy是一种正式的面向对象建模语言。我们选择了Alloy而不是统一建模语言（UML）[2]和对象约束语言（OCL）[15]，因为Alloy具有更简单的语义，并且没有二义性，允许一致的形式化。Alloy的另一个优点是支持自动规范分析，这是在实践中使用形式化方法的一个重要方面。此外，尽管它的语义简单，但Alloy的表达能力足以对各种各样的应用程序建模。也许，我们的法律也可以是有用的UML模型的推理，如果我们给UML类图使用合金的语义。除了阐明Alloy的语义之外，这些基本定律还为模型转换的实际应用（如将设计模式引入模型）提供了更详细的定律。 由于空间有限，我们不会在这里展示。由于我们证明了基本定律保持语义，我们保证这些更详细的法律派生，使用基本定律，也保持语义。这些基本定律的重点是使用它们来推导出更精细的定律，这些定律重构了我们希望确保语义得到保留的模型然而，我们也可能希望在不保留语义的规范中进行更改。在这些情况下，接下来提出的基本定律是不合适的，但这是由用户完成的。此外，这是一种良好的做法，表明在某种意义上来说是完整的。标准的方法是证明基本定律集足以将任意模型转换为用语言运算符的一个小子集表示的范式[9]。然而，这超出了本文的范围。类似的工作已经为Refinement Object Oriented Language（ROOL）做了[3]。但是，ROOL在指定类型之间的结构属性方面功能较弱。而ROOL只支持属性声明，如Java [8]，Alloy支持具有任意性和多重性的双向关系声明，如UML中的OCL。另一个区别是，在ROOL中，我们不能定义全局约束，例如那些涉及整个系统中类的基数（实例数）的约束。在Alloy和带有OCL的UML中，这是可能的。相关的方法[16，7，20，5]已经提出了一些UML模型的转换。然而，有些转换并不完全保留语义.此外，它们与我们的不同，因为它们不R. Gheyi，P. Borba /《理论计算机科学电子笔记》95（2004）227-243229提出了一个小的小粒度转换集。它们与设计重构非常相似，后者是大粒度的转换，保留了语义，并可能提高规范的可读性、设计结构和可重用性。模型转换很有用，因为转换模型比转换代码更容易。通常，我们只重构代码。 然而，如果我们构建一个工具来自动关联代码和模型转换，我们只需要在更简单的模型中进行更改，它就会自动将更改映射到代码。本文的其余部分组织如下。 第2节概述了Alloy语言。在第3节中，我们介绍了合金的一些基本定律。下一节将说明如何使用上一节中介绍的定律来形式化地重构Java类型的设计模型。最后，第5节讨论了一些相关的工作，并提出了我们的结论。2合金Alloy是一种强类型语言，它假设一个由划分为子集的元素组成的世界，每个子集都与一个基本类型相关联。Alloy模型或规范是两种类型的段落序列：用于定义新类型的签名，以及用于记录约束的公式段落，如事实和函数。每个签名都有一组对象（元素）。这些对象可以通过签名中声明的关系来关联。签名段落引入了一个基本类型如果一个签名扩展了另一个签名，那么它的类型就是父签名类型。除了签名扩展，Alloy还有其他重要的结构和操作符，如模块，多态性，用于分析规范的命令，可以在其他地方找到[13]。假设我们想在银行系统的Alloy部分中建模，其中每个银行都有一组账户，每个账户都有一个唯一的标识符。图1描述了系统的对象模型[17]。对象模型中的每个框表示一组对象。箭头是关系，有时称为关联，它们指示一个集合中的对象如何与其他集合中的对象相关。例如，标记为id的箭头从Account到String显示，Account中的每个对象都有一个字段，其值对象是String对象。多重性符号是：！（1）？（零或一），*（零或230R. Gheyi，P. Borba /《理论计算机科学电子笔记》95（2004）227-243Fig. 1. 银行系统对象模型+（一个或多个）。多重性注释可以出现在箭头的两端。如果省略多重性符号，则假定为 *。下面的代码介绍了对银行系统进行建模的三个签名和两个关系。签署银行{帐户：设置帐户}sig帐户{id：String}String {}在Bank的field声明中，关键字set指定accounts将Bank中的每个元素映射到Account中的一组元素。当我们省略关键字时，比如在id的声明中，我们指定所有帐户都有一个标识符（total函数）。其中一个公式段落被称为事实。它用于打包始终保持的公式，例如关于某些类型和集合的元素的不变量。下面的示例引入了一个名为Restrictions的事实，建立了有关前面引入的签名和关系的常规属性事实限制{账户 =银行账户all disj acc 1，acc 2：帐户|（acc1.id）！= （acc2.id）}第一个公式指出，没有一个账户不是银行账户另一种说法是，不同的账户有不同的标识符。关键字all是通用量化器，我们在acc1和acc2之前使用disj来表示它们是不相交的。在Alloy中，事实公式被隐式声明为它们的结合。函数是参数化公式，可以通过将其参数绑定到类型与声明的参数类型匹配的表达式来应用。R. Gheyi，P. Borba /《理论计算机科学电子笔记》95（2004）227-243231它们对于指定系统操作的行为特别有用下面的例子声明了一个函数，它将一个帐户添加到一个特定的银行，并返回一个添加了新帐户的银行fun Bank：：addAccount（acc：Account）：Bank{ result.accounts = this.accounts + acc}运算符+对应于联合运算符。 关键字this和result是包含接收方和结果参数的匿名变量。receiver和result参数分别表示addAccount函数的前状态和后状态。加入P。关系p和q的q是通过取p中的元素和q中的元素的每个组合，并包括它们的连接（如果存在）而得到的关系。关系p和q可以有任意的元数，只要它们不都是一元的。p的右类型必须匹配q的左类型。这是标准连接运算符的广义定义。比如说，这个的加入。accounts，其中这是一个bank，accounts是一个将bank与accounts关联起来的二元关系，它返回一组元素，这些元素是accounts中this的关系映像。此表达式生成接收方银行的所有帐户。Alloy规范的语义是对签名名和字段名的所有可能赋值，这些赋值满足规范的隐式和显式约束。在上一个示例中，它包含对签名名称Bank、Account和String以及关系名称accounts和id的所有有效赋值。这些赋值必须满足规范的所有隐式和显式约束例如，所有分配给Account的元素都必须是银行账户。Alloy中的模型是简洁的、可分析的、声明性的和结构化的。这些功能本身并不是什么新功能。Alloy是不同的，因为它同时是声明性的和可分析的。 很长一段时间以来，一个高级规范不能同时是可分析的和可声明的。函数式程序既是声明式的，也是可执行的，但它们没有Alloy规范的相同抽象级别在Alloy中，可以自动化不同类型的模拟和分析[12，10，11，14]。3基本规律在本节中，我们将介绍一些针对Alloy提出的基本定律这些定律陈述了关于签名、公式和关系的性质。第一定律确定了我们总是可以引入一个空签名，用一个新的名字声明。这表明我们也可以删除未使用的空签名我们232R. Gheyi，P. Borba /《理论计算机科学电子笔记》95（2004）227-243用ps表示一组段落。由于在Alloy中，我们不能有两个同名的段落，因此我们有一个但书，说明新签名的名称不会出现在ps中。法则1引入空签名=提供（→）ps不声明任何名为S的段落;（←）S不出现在ps中。我们在但书前写上（→），以表明但书仅适用于从左到右的应用。类似地，我们用（←）表示它只适用于从右向左的法律，而我们用（Participate）表示但书在两个方向上都是必要的。 重要的是要注意，当从左到右或从右到左应用时，每个基本定律都定义了一个保持语义的转换。我们认为Alloy中的两个模型是相等的，如果对一个模型的名称的所有可能的类似的定律也适用于事实，但由于合金事实不能从其他段落中引用，因此消除空事实总是可能的。法则2引入空洞的事实=提供（→）ps不声明任何名为F的段落。下一个定律规定，我们可以在一个事实上增加或删除一个公式，只要它可以从规范的其他公式中推导出来定律3引入公式=提供（Participate）公式f可以从ps和forms中的公式推导出来。psfactF{forms f}psfactF{forms}psfactF{}PSpssigS{}PSR. Gheyi，P. Borba /《理论计算机科学电子笔记》95（2004）227-243233由于f是从其他公式推导出来的，我们保证这两个speci- tions具有相同的含义。这个公式所施加的限制已经被其他公式所施加。我们写形式来表示一组公式。从谓词演算出发，我们从JA=>BJ和A公式推导出JA和BJ因此，我们可以应用这个定律。这些规律只适用于铝合金结构.然而，关系运算符属性和谓词演算属性也可以应用于Alloy公式。另一个定律表明，我们总是可以将公式从一个事实转移到另一个事实。法则4移动公式=我们可以将一个公式从一个事实移到另一个事实，因为在Alloy中，一个公式是否在一个事实或另一个事实中声明并不重要，因为Alloy规范的语义将它们视为所有事实公式的结合。我们可以把定律1和定律2看作是中性的元素。类似地，定律3陈述了合取逻辑运算符的等元性，而定律4陈述了合取逻辑运算符的结合性除了处理事实的法律之外，我们还有处理关系的法律下一个定律指出，我们可以引入一个新的关系及其定义，即r=exp形式的公式，为关系建立一个值。我们也可以删除一个不使用的关系第五定律介绍关系及其定义=提供（→）S的族在ps中不声明任何名为r的关系，并且T要么是S，要么是ps中声明的签名名;（←）r关系不出现在ps和forms中。S签名族是所有扩展的签名的集合，并且被S扩展，包括它自己。声明新的关系名称不出现在S签名族中的前提条件保证了我们没有冲突名称。合金不允许两个关系相同pssigS{rs} factF{表格}pssigS{rs，r：集合T}事实F{forms r=exp}psfactF{forms}事实G{formsJ f}psfactF{forms f}事实G{formsJ}234R. Gheyi，P. Borba /《理论计算机科学电子笔记》95（2004）227-243家族签名中的名字。请注意，前面的定律可以用来简单地引入一个关系，而不需要任何定义。我们只要把exp当作r本身，引入一个重言式，这个重言式可以用定律3简单地消除。在S签名中声明的一个关系被限定为T的集合，表明S中的每个元素都可以与任意数量的T元素相关。由于它不施加任何约束的映射，我们保证以前的法律保持隐式和显式的约束。因此，我们不引入不一致性。r关系的类型也可以被限定为标量或T的选项。第一个限定符定义一个全函数，最后一个限定符定义一个全函数。从S到T的部分函数，在这种情况下。默认限定符是标量。由于标量和选项限定符引入的隐式约束，我们不能引入用这些限定符声明的关系，因为隐式约束可能与规范的先前隐式和显式约束相矛盾。在这种情况下，我们只能引入一个与集合限定符的关系。然而，如果我们从隐式和显式约束中推导出这个新关系是一个全函数或部分函数，那么我们可以从左起应用定律3来纠正并引入这个公式。在那之后，我们可以通过应用我们接下来展示的定律来改变关系的类型。下面我们使用r而不是S$r，因为为了简单起见，我们假设在规范中没有其他具有相同名称的关系。符号S$r可替代地表示对S签名的r关系的引用。下面的两个定律允许我们将关系的类型从集合改变为标量或选项。其中第一个建立了我们可以将关系的类型从集合改变为标量，反之亦然，如果r是一个全函数。法则6：改变关系类型：从集合到标量pssig S{rs，r ：集合T}pssigS{rs，r：事实F{形成所有s：=标量T}S | 一个S.RfactF{forms}}一个类似的定律被提出来将关系的类型从集合改变为选项，反之亦然。在这种情况下，我们需要一个公式来证明r是一个部分函数。R. Gheyi，P. Borba /《理论计算机科学电子笔记》95（2004）227-243235法则7：改变关系类型：从set到option=重要的是要注意，如果S签名扩展了其他签名，则定律6和定律7也有效。我们已经证明了这些定律的正确性，并提出了其他定律，如上拉关系，但这些都超出了本文的范围。我们证明了这些法律的合理性的基础上denotational合金的语义，我们建议使用合金。我们倾向于提出小粒度的变换，因为它更容易证明它们保持语义。通过组合它们，我们可以得到大粒度的转换，从而保持语义。下一节列举了使用这些法律的例子4重构Java类型规范维护一个面向对象的程序通常需要结构上的改变，比如改变类之间的关系。这对于软件演化是有用的，当设计人员有兴趣重新构建规范以进行改进，或者以更适当的方式引入新的需求时。在本节中，我们将展示如何通过简单地使用所提出的定律来重构一个简单但不平凡的Alloy这说明了这些定律对于重构模型是有用的我们在这里考虑一个规范，它对Java类型检查器规范的一部分进行建模。这个模型是由Daniel Jackson4编写的，有一些语法差异，是Alloy Analyzer分发包5的一部分。4.1初始规范Java类型的规范描述了Java中类型的基本概念，如图2所示。一个带有封闭头部形式的箭头，如从Object到Class，表示一个子集关系。在这种情况下，Object是Class的子集。如果两个子集共享一个箭头，则它们不相交。例如，类和接口是不相交的。如果箭头被填满，则子集将耗尽4http：//sdg.lcs.mit.edu/http://alloy.mit.edupssigS{rs， r集合T}：factF{formsalls：S | sole s.r}pssigS{rs，r选项T}factF{forms}：236R. Gheyi，P. Borba /《理论计算机科学电子笔记》95（2004）227-243图二. Daniel Jackson的Java类型对象模型超集，所以超集的成员都是子集的成员。在这种情况下，子集形成一个划分：超集的每个成员都属于一个子集。了！对象框中的符号表示该框表示的集合包含一个元素。此模型忽略基元类型和空引用。每个类型可以具有一组子类型。 类型被划分为类接口类型和对象是一个特定的类。下面的Alloy签名类型{ subtypes：set Type }签名类，接口扩展类型{}在Alloy中，我们可以一次声明多个签名，如果它们不声明任何关系，如Class和Interface的声明所示。一个签名可以扩展另一个签名，建立扩展签名是父签名的子集。这不会引入另一个基本类型，如前所述。扩展签名与父签名的类型相同。静态签名对象扩展类{}static关键字表示签名只有一个元素。在这个例子中，Object签名只有一个元素。下面的事实声明指出每个类型都是ObjectR. Gheyi，P. Borba /《理论计算机科学电子笔记》95（2004）227-243237但不是其自身的子类型。此外，它规定每个类型是最多一个类的子类型。它还声明不存在同时是类和接口的类型，并且任何类型都是唯一的类或接口。运算符、和分别对应于关系的自反传递闭包、传递闭包和转置。fact TypeHierarchy { Type in（Object.*亚型）无t：类型|tin（t. subtypes）allt：类型|sole（（t.~subtypes）&Class）no（Class&Interface）Type =（Class+Interface）}运算符对应于交集运算符。关键字no是第二个公式中的量化器。 但是，当应用于表达式时，如在第四个公式中，定义了一个表达式中没有元素的谓词。Alloy中的关键字in可以表示一个子集运算符，就像前面事实的第一个公式一样，也可以表示一个成员运算符，就像前面声明的第二个公式一样。当关键字sole应用于表达式时，它定义了一个谓词。例如，sole（t. subtypes&Class）为真，如果表达式（t. subtypes类）最多有一个元素。到目前为止，我们已经在Java中指定了类型。为了简单起见，现在我们描述一些表达式的简单类型检查器的一部分。下面的签名声明表示每个对象都有一个类型（其创建类型），即类。一个变量可以保存一个实例，并有一个声明的类型。sig实例{ type：Class } sig变量{持有：option实例，类型：类型}最后，TypeSoundness事实声明变量持有的所有实例都factTypeSoundness {all v：Variable|（v.holds.type）in（v.type.* subtypes）}4.2重构规范前面的模型根据子类型关系描述Java类型。但是，我们希望重构这个模型，以便用超类型关系（如extends6和implements）来描述Java类型。为了保证结果模型与原始模型是等价的，我们不应该以一种特别的方式进行，对模型进行任意的修改。 事实上，我们可以使用第2、3、5和7条法则来逐步改变规范，如下面所示，保持其语义。所需的对象模型如图3所示。为了简化下面的重构步骤，我们认为ps包含之前声明的签名和事实，除了Type签名。在6.注意Alloy中没有关系可以命名为extends，因为它是一个关键字。然而，我们在这里使用它只是为了提高可读性。238R. Gheyi，P. Borba /《理论计算机科学电子笔记》95（2004）227-243图三. Java类型的对象模型重构在本节的最后，我们展示了完整的规范。为了引入新的关系，我们可以使用定律5，但是由于这个定律需要一个事实，我们首先从左到右应用定律2来引入一个空的事实。接下来，我们介绍，使用法律5从左到右，关系扩展和实现，在类型，和他们的定义在定义事实。ps sigType { subtypes：set Type，extends：set Class，implements：set Interface }事实定义{ implements=（~subtypes（Type->Interface））extends=（~subtypes（Type->Class））}&&符号−>表示将左操作数中的每个元素与右操作数中的每个元素组合并连接它们的乘积运算符。这些元素也可以是元素的元组当应用于集合时，该运算符表示标准笛卡尔积。请注意，我们可以应用该定律，因为在Type的族中没有定义扩展和实现还要注意，新关系的类型在初始规范中是有效的。我们的目标是推导出亚型定义，以便用其定义来取代它，并最终将其从规范中删除。要推导它的定义，请注意extends和implements具有相同的类型（Type−>Type）。我们使用一些谓词演算和集合论性质[19]以及指定中的一些公式（括号内）来证明推导中的每一步。R. Gheyi，P. Borba /《理论计算机科学电子笔记》95（2004）227-243239由于它们具有相同的类型，我们可以推导出它们的并集是：（extends+implements=（~subtypes（Type->Class））+（~subtypes（Type->Interface）[A B + A C = A（B+C）]=>（extends+implements=~subtypes（（Type->Class）+（类型->接口）[（A->B）+（A->C）=（A->（B+C））]<=>（扩展+实现=~子类型（类型->（类+接口）[类型=（类+接口）]<=>（扩展+实现=~子类型&&（类型->类型））=>（扩展+实现= ~子类型）[（A=B）=>（~A=~B）]=>（~（扩展+实现）= ~~子类型）[~（A+B）=（~A+~B）]=>（~扩展+ ~实现= ~~子类型）[~~A = A]=>（~扩展+ ~实现=子类型）[（A=B）=>（B=A）]=>（子类型=扩展+~实现）由于这个公式是从定义中推导出来的，从左到右使用定律3，我们可以在规范中引入这个公式ps sigType { subtypes：set Type，extends：set Class，implements：set Interface }事实定义{ implements=（~subtypes（Type->Interface））extends=（~subtypes（Type->Class））subtypes=（~extends+ ~implements）}&&从TypeHierarchy事实的第三个公式中，我们可以推导出，正如下面解释的那样，所有的t：Type|Sole（t. 延伸）。所有t：类型|sole（（t.~ subtypes）&类）[subtypes =extends +~implements]<=> allt：Type |sole（（t.~（~extends +implements））&Class）[~（A+B）= ~A + ~B]<=> allt：Type|sole（（t.（~~extends +~~implements））&Class）[r.（A+B）= r.A + r.B]<=>所有t：类型|鞋底（（t.~~扩展+t.~~ implements）&Class）[~~A = A]<=> allt：Type |sole（（t.extends + t.implements）&Class）[（A+B）&C = A& C + B&C]<=> allt：Type |sole（t.extends）&Class）+（（t.implements）&Class））[no（Class&Interface）]<=>allt：Type |sole（t.extends）&Class）+{}）[A +{}=A]<=> allt：类型|sole（（t.extends）&Class）<=> allt：Type |sole（t.extends）然 后 ， 我 们 可 以 从 左 到 右 应 用 定 律 3 ， 在 定 义 中 引 入 所 有 t ：Type|Sole（t. extends）公式，因为我们推导出一个公式，说明extends是一个部分函数。ps sigType { subtypes：set Type，extends：set Class，implements：set Interface }事实定义{ implements=（~subtypes（Type->Interface））extends=（~subtypes&&（Type->Class））subtypes =（~extends +~implements）all t：Type|sole（t.extends）}现在我们可以将extends关系的类型从set改为option第七条从左到右ps sig Type { subtypes：set Type，extends：option类，实现：set接口}事实定义{实现=（~subtypes（Type->Interface））extends =（~subtypes（Type->Class））subtypes =（~extends +~implements）}&&接下来，我们将子类型关系的引用替换为其定义。请注意，从每个包含子类型关系的公式（除了它的定义）中，我们可以导出一个公式，用子类型关系的定义代替子类型关系，并将它从左到右插入到应用定律3的规范中因此，这些新公式也可以导出具有子类型的公式。接下来，240R. Gheyi，P. Borba /《理论计算机科学电子笔记》95（2004）227-243我 们 可 以 从 应 用 定 律 3 的 规 范 中 从 右 到 左 删 除 包 含 子 类 型 ps（subtypes=extends+implements）表示法表示我们将ps中出现的每个子类型替换为extends+ps（subtypes = ~extends + ~implements）sig Type {subtypes：set Type，extends：option Class，implements：set Interface} fact定义{ implements =（~（~extends + ~implements）（Type->Interface））extends =（~（~extends + ~implements）（Type->Class））subtypes =（~extends + ~implements）}&&由此产生的定义的第一和第二个公式是平凡有效的公式。我们可以使 用 规 范 中 的 一 些 集 合 论 性 质 和 公 式 推 导 出 ， 它 们 分 别 等 价 于implements=implements和extends=extends。因此，我们可以从右向左应用定律3来ps（subtypes = ~extends + ~implements）sig Type {subtypes：set Type，extends：option Class，implements：set Interface} fact定义{ subtypes =（~extends + ~implements）}由于子类型没有出现在ps中，因为我们用它的定义代替了它，所以我们可以使用定律5从右到左删除这个关系及其定义。在此之后，定义事实变为空，并且可以从右向左应用定律2这是将子类型关系替换为扩展和实现关系的最后一步。所得规格如下所示：sig Type { extends：option Class，implements：setInterface } part sig Class，Interface extends Type {}静态签名对象扩展类{}fact TypeHierarchy {Type in（Object.*（~extends+~implements））no t：Type |tin（t.（~extends +~implements））allt：Type |sole（（t.~（~extends +~implements））&Class）no（Class&Interface）类型=（类+接口）}sig实例{ type：Class } sig变量{ holds：option实例，type：Type}fact TypeSoundness {all v：Variable|（v.holds.type）in（v.type.*（~extends+~implements））}现在，规范根据超类型关系对Java类型进行建模。然而，结果模型中的一些公式不是那么可读，比如TypeHierarchy事实中的一些公式我们可以用其他公式来代替例如，我们可以用所有的t替换这个事实的第三个公式：|Sole（t. 扩展）使用一些集合论和谓词演算属性和规范的公式。事实上，我们甚至可以去掉这个公式。首先，从右向左应用第7定律，得到相同的公式。接下来，使用从右到左的定律3最后，从左到右应用定律7，得到一个没有R. Gheyi，P. Borba /《理论计算机科学电子笔记》95（2004）227-243241所有t：类型|Sole（t. 扩展）公式。我们已经重构了其他规范，并导出了其他重构，例如引入泛化和移动关系。但由于篇幅有限，这里就不一一介绍了。5结论在本文中，我们提出了合金的基本规律。这些定律不仅对定义建模语言的公理语义很重要，而且对重构规范也很重要，如Java类型的模型所示这里提出的定律已被证明是合理的，Alloy的正式语义。因此，它们应作为进行模型转换的工具。基本定律的一个直接应用是定义一个接口，从中可以导出更复杂的定律，如重构。如第4节所示，它们也可以用于逐步重构设计。我们不需要证明初始和最终的Java类型规范具有相同的语义，因为我们使用的基本定律保证了每一个都保持语义。因此，它们的组合也保留了语义。基本法律的主要焦点是建筑师。架构师将使用它们来派生可供设计人员使用的重构（大粒度转换）设计者将只使用架构师派生的重构。我们推导了一些重构，并将其中三个应用于银行系统在这种情况下，设计者只需要应用三个重构，而不是像我们在Java类型的规范中所做的那样，应用基本定律，用大约20个步骤来重构银行系统形式化进一步的基本定律，比如说在哪些条件下我们可以引入泛化，重构，并将它们应用于其他现实案例研究，是进一步研究的一些主题。大多数基本定律都很容易应用，因为它们的前提条件是简单的句法条件。然而，为了避免错误并帮助架构师，一些定律（如引入公式的定律（定律3））可能需要使用自动定理证明器或证明助手来验证两个在这些情况下也可以使用合金。但是，我们只能在Alloy Analyzer中保证断言对预定义的范围有效。我们扩展了Alloy Analyzer工具，使其包含了这里介绍的大多数基本定律的实现，用户不需要验证先决条件并应用它们。用户只需要通知转换的参数值。另一种方法，我们可以用来自动实现它们，242R. Gheyi，P. Borba /《理论计算机科学电子笔记》95（2004）227-243是使用Maude [18]项重写系统。虽然我们已经有了Alloy的一组基本定律，其中一些我们在这里展示，但我们仍然需要证明一个归约定理，说明我们的定律集在允许将任意Alloy规范归约为语言运算符的一个小子集中表示的范式的意义上是完整的，遵循ROOL [4]，命令式语言[9]等采用的方法。另一个进一步的研究课题是检查建模规律和编程规律之间的关系，例如ROOL规律。特别地，我们需要调查设计重构是否有相应的代码重构。相关的工作[20，5，7，16]已经在UML设计模型的转换上进行。然而，一些转换[20，7，16]不保持语义。例如，有人认为，创建类之间的泛化保持语义。然而，通过引入泛化，规范中的约束可能变得不一致（图4）。例如，我们不能用T类扩展S类，当我们在规范中有一个明确的约束，说明S比T有更多的元素。在这种情况下，引入一个推广将使规范不一致，因为推广引入了一个隐式约束，即T包含S。因此，我们从这个隐式约束中推断出T具有与S相同或更多的元素，这与规范中的显式约束相矛盾。见图4。引入泛化此外，另一项工作[16]指出，逻辑上加强类不变式是一种细化变换，尽管添加公式有时会另一个工作[5]删除类和关系，而不检查规范中是否有关于它们的一些约束，这在正式设置中是不可接受的。这些转换并不保留语义，因为其中一些转换使用的UML语义是不明确的。另一些定义了UML语义的一部分，但没有验证转换的可靠性，或者没有考虑OCL约束。R. Gheyi，P. Borba /《理论计算机科学电子笔记》95（2004）227-243243引用[1] Beck，K.，“Extreme Programming Explained,” Addison-Wesley,[2] Booch，G.，I. Jacobson和J. Rumbaugh，[3] 博 尔 巴 山 口 和 A.Sampaio， Basic laws of ROOL ： an object-oriented language ， RevistaBrasileiradeInform'ticaTéoricaeAplicadaVII （ 2000-AshorterversionappearedinThirdBrazilianWorkshoponFormalMethodds，pages33-44，J o a rksho P e ssoa，Brazil，Octo o b e r 2000. ），pp. 49比68[4] Borba ， P. 、 杨 A.是 一 个 MP AIO 和 M 。 Corn'elio ， Areefinementalgebrafororobject-orientedprgraming ， in ： 17th European Conference on Object-Oriented Programming ，ECOOP457-482[5] Evans，A.，用UML类图进行推理，在：第二届IEEE工业强度形式规范技术研讨会，WIFT102[6] Fowler，M.，“Refactoring: Improving the Design of Existing Code,” Addison-Wesley,[7] Gogolla，M.和M. Richters，UML类图的等价规则，在：统一建模语言，UML '98-超越符号。第一次国际讲习班，米卢斯，法国，1998年6月，1998年，第100页。87比96[8] Gosling，J.，B.乔伊和G。Steele，[9] Hoare，C.，J. 斯皮维岛Hayes，J.他，C.摩根A.W. Roscoe，J.桑德斯岛索伦森和B. Sufrin，Laws of Programming，Communications of the ACM 30（1987），pp.672-686。[10] Jackson ， D. ， Object models as heap invariants ， in ： Essays on ProgrammingMethodology，Springer-Verlag，2000.[11] 杰克逊，D。和A.Fekete，对象交互的轻量级分析，第四届计算机软件理论国际研讨会，仙台，日本，2001年。[12] Jackson，D.， I. 谢克特和我 Shlyakhter，Alcoa：合金约束分析仪，在：软件工程国际会议，利默里克，爱尔兰，2000年，页。七三零七三三[13] Jackson，D.，I. Shlyakhter和M. Sridharan，一种微模块化机制，在：ACMSIGSOFT软件工程基础会议/欧洲软件工程会议（FSE/ESEC62比73[14] 杰克逊，D。和K.Sullivan，COM revisited：软件结构的工具辅助建模和分析，在：ACMSIGSOFT软件工程基础会议，圣地亚哥，美国，2000年，页。149比158[15] Kleppe，A.和J. Wa