理论计算机科学电子笔记130（2005）281-300www.elsevier.com/locate/entcs面向分层架构的M'arcioCorn'elio1Departamento de SistemasComputacionaisEscolaPolit′ecnica-UniversidadedePernambuco天气-累西腓，巴西安娜·卡瓦尔康蒂2约克大学计算机科学系英国约克Augusto Sampaio3CentrodeInform'aticaUniversidade Federal de Pernambuco天气-累西腓，巴西摘要在本文中，我们提出了如何重构的面向对象的程序可以通过使用正式的细化。我们的方法是基于使用的重构规则设计的顺序面向对象语言的细化（ROOL）类似于Java。 我们定义了一种策略，旨在根据分层架构来构建程序，该架构涉及重构规则，面向对象编程法则以及数据和算法改进的应用。由于这些规则是在ROOL的最弱前提语义中证明的，因此重构的正确性是通过构造来保证的。保留字：重构，形式细化，细化演算1电子邮件：mlc@upe.poli.br2电子邮件：Ana. cs.york.ac.uk3电子邮件：acas@cin.ufpe.br1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.03.015282M. Cornélio等人/理论计算机科学电子笔记130（2005）2811介绍面向对象编程被认为是获得比传统软件更容易修改的软件的一种手段[20]。然而，改变一个面向对象的程序通常需要结构上的改变，比如在类之间移动属性和方法，以及将一个复杂的类划分成几个类。这样的修改应该只改变软件的内部结构，而不会影响用户所感知的软件行为这种行为被称为重构[16]。关于重构的工作通常以一种相当非正式的方式描述用于程序修改的步骤[16，23，25]。在我们的方法中，形式重构是通过应用程序设计法则来实现的，这些法则既处理命令，也处理面向对象的特性，如方法和类[3，4]。这些定律是为ROOL[8，7]提出的，rool是面向对象语言的缩写，它是顺序Java的一个子集，具有类、继承、属性的可见性控制、动态绑定和递归。编程法则是重构规则推导的基础，以及导致类的数据细化的法则[12]。这些法律精确地指出了可以对程序进行的修改，并规定了相应的证明义务。使用法律，程序开发是公正的和记录的。通过使用重构规则和编程法则完成的程序转换保持了程序的行为[12]。我们的语言有一个最弱的前提语义，它支持我们所使用的法则的形式正义，从而支持我们的策略。 在[12]中给出了对于ROOL[3，12，4]提出的关于最弱前提语义[8，7根据由独立软件层组成的体系结构构建的系统，以正交方式处理数据库访问，GUI，分布和功能需求，具有目的明确分离的类[6]。结构良好的程序对于提高重用性和可扩展性是必不可少的。例如，使用分层架构，我们可以集成面向对象编程语言和关系数据库，而不会影响软件质量因素，如可重用性和可扩展性[26]。在本文中，我们展示了如何使用重构规则[12]和编程定律[3，4]来完成面向对象程序的重构。我们提出了一种重构策略，并以模板类的使用为例说明了它的应用使用这种策略，我们重构一个程序，这是一个真正的应用程序的代表。我们的案例研究首先在[26]中报道，并非正式地开发，涉及面向对象编程语言与重新编程语言的集成M. Cornélio等人/理论计算机科学电子笔记130（2005）281283国家数据库。我们把原来的程序，它最初没有单独的架构问题，到一个架构实现软件质量因素，如可重用性和可扩展性。这个案例研究的正式开发有助于为ROOL确定新的重构规则，并改进我们的重构策略。它最初出现在[12]中。本文件的结构如下。在第2节中，我们将介绍ROOL的概述以及命令和类的一些基本规则在第3节中，我们提出了两个重构规则，我们在这里介绍的推导中使用。之后，在第4节中，我们提出了一个在ROOL中进行程序重构的策略，其目的是根据分层体系结构来构建程序，并简要介绍了我们的案例研究。在第五节中，我们讨论了一些相关的工作。最后，在第6节中，我们总结了所取得的成果，并指出未来的研究方向。2规则与法律ROOL[8，7]是一种基于顺序Java的面向对象语言。它允许对面向对象的程序和规范进行推理，因为这两种结构都以摩根精化演算的风格混合在一起ROOL的语义，像通常的精化演算一样，是基于最弱的前提条件。ROOL的命令结构基于Morgan的精化演算语言在精化演算中，指定被视为命令。事实上，我们使用术语命令来指代通常意义上的命令，以及规范和命令混合的编程结构ROOL中的程序cds·c是一个cds类序列，后跟一个主命令c。在下面的例子中，我们定义了一个类Account。Account类扩展对象pribalance：int...methgetBalancemethsetBalance=^（resr：i nt·r：=self. balance）=^（vals：i nt·self. balance：=s）新的端=^self. balance：=0类通过单一继承相关，这由子句extends指示。类对象是所有类的超类。因此，在帐户声明中可以省略extends子句。Account类284M. Cornélio等人/理论计算机科学电子笔记130（2005）281包括一个名为balance的私有属性;这通过使用PRI限定符来指示。属性也可以是protected（prot）或public（pub）。ROOL只允许重新定义那些公开的并且可以递归的方法;它们是使用Back的参数化命令形式的过程抽象来定义的参数化命令的格式可以是valx：T·c或resx：T·c，它们分别对应于按值调用和按结果调用的参数传递机制。例如，方法getBalance有一个结果参数r，而setBalance有一个值参数s。初始化器由新条款声明。ROOL中的命令类似于Morgan特别地，在一个指定语句x：[101，102]中，我们称x为框架，而谓词101和102分别是前置条件和后置条件。当在满足条件1的状态下执行时，这个程序在满足条件2的状态下终止，只修改x中的变量。 在初始状态不满足条件1的情况下，命令x：[x1，x2]中止：所有可能的行为和非终止都是可以预期的。在[3，4]中已经定义了ROOL命令的法则处理小粒度构造，而类的法则考虑中等粒度构造。许多命令的法则类似于命令式编程的法则，例如，在[18]中，但是ROOL有支持面向对象特性的法则，例如方法调用，类，类型转换和测试。对于ROOL的最弱前提语义，这些定律被证明是合理的[12ROOL法则，主要是那些与面向对象特性相关的法则，解决了上下文问题。我们使用cds1=cds，ccds2，其中cds是cds1和cds2的类声明的上下文，c是表示类声明cds1和cds2的集合的等价性的主命令。这个符号只是对程序等价性cds1cds·c=cds2cds·c的一种聚焦，它在[8，7]中得到了下面我们举几个例子。当从左到右应用定律必须满足某些条件时，我们写我们也用我们使用条件在法律规定的条款中说明使用法则2.1“方法消除”，我们可以从类中删除一个方法，如果它没有被cds中的任何类调用，在主命令c中，也没有在类C中。为了从右向左应用这个定律，方法m不能已经在C中声明，也不能在它的任何超类或子类中声明，这样我们就可以在类中引入一个新方法。符号B。m通过静态类型为B的表达式调用方法m。子类关系用≤表示。我们写B≤A来表示类B是一个M. Cornélio等人/理论计算机科学电子笔记130（2005）281285A类的子类。第2.1条排除法=cds，c提供（→）B. m不出现在cds，c中，也不出现在ops中，对于任何B使得B≤C。（←）m没有在ops中声明，也没有在cds中的C的任何超类或子类中声明。Q法则2.2类删除当从左到右应用时，允许删除整个程序中没有引用的类。相反方向的应用程序在程序中引入了一个新类第2.2条规定的第二类消除规则（→）cd1中声明的类在cds或c中没有引用;（←）（1）在cd1中声明的类的名称与在cds中声明的所有类的名称不同;（2）出现在cd1中的超类要么是对象，要么是在cds中声明的;（3）cd1声明的属性和方法名称不是在cds中由它的超类声明的，除非在方法重新定义的情况下Q要从左到右应用这条定律，在cd1中声明的类的名称在整个程序中不能被引用。为了从右向左应用这条定律，在cd1中声明的类的名称必须与所有现有类的名称不同;出现在声明cd1中的超类是object或在cds中声明。最后，对于cd1中声明的类，只允许重新定义方法。定律2.3私有属性耦合不变式允许我们改变类中的私有属性，并将它们与新的属性关联起来。这个定律的应用改变了类中声明的方法的主体。这些变化遵循传统的数据精炼法[21]。按照惯例，由x表示的属性是抽象的，而由y表示的属性是具体的。耦合不变量CI将抽象属性和具体属性联系起来。符号CI（mts）表示CI应用于mts中的每种方法：C类扩展D广告ops端C类扩展D广告methm=^pcend;ops端286M. Cornélio等人/理论计算机科学电子笔记130（2005）281应用CI根据数据精化定律[21]改变了方法，也就是说，为了假设耦合不变量，增加了保护，并且每个命令都通过修改扩展到具体变量，我们写pria：T;ads来表示属性声明pria：T和ads中的所有声明，而mts代表方法和初始化器的声明。定律2.3私有属性耦合不变量≤CIQ符号≤表示该定律涉及通过耦合不变量CI相关的属性之间的模拟。类的数据细化的模拟及其可靠性证明在[9]中给出还有一些法则可以处理将属性和方法移动到超类，例如改变属性和参数的类型，以及其他特性。他们可以在[3，4]中找到。目前，ROOL具有复制语义而不是引用语义。当然，指针在实践中无处不在。然而，我们决定首先集中讨论面向对象和Java的其他方面，如继承、动态绑定、可见性和类型测试和强制转换。一般来说，我们得到的结果在指针存在的情况下也是有效的，但是在共享存在的情况下，它们需要修改。3重构规则在[12]中，我们提出了一套全面的重构规则，这些规则捕获并形式化了[16]中非正式引入的大多数重构。在这里，我们介绍了在分层架构模式的推导过程中使用的两条规则。重构规则是通过两个并列的框以及where和provided子句来描述的必要时，我们用where从句来写缩写。应用重构规则的附带条件在规则的provided子句中列出规则的左边classAextendsCpriy：TJ;ads CI（mts）端CDS· CclassAextendsCprix：T;ads mts端CDS· CM. Cornélio等人/理论计算机科学电子笔记130（2005）281287第3.1条取消授权=cds，c提供（Participate）（1）super不出现在n中;（2）bnull错误b/=错误是一个A的不变量;（3）自性。y不出现在n中，对于adb;（→）（1）自我。对于任何public或protected属性，a不出现在n中由D或其任何超类声明的a;（2）self。p不出现在n中，对于在mts b中或在B的任何超类中声明的任何方法p;（3）self。b不出现在mtsa中;（4）x不在adsa中声明，也不在A的任何超类或子类中声明;（←）（1）b不在广告a中声明，也不在A的任何超类或子类中声明;（2）自我。x不出现在mtsa中;在规则应用之前显示类;在规则应用之后显示类：转换后的类。然而，我们必须注意到，许多重构规则是等价的，可以在两个方向上应用。classAextendsCprib：B;adsamethm=^（pds·self. B. n（α（pds）阿山新w=^self. b：=新w. B端类B扩展Dprix：T;adsbmethn=^（pds·c）mtsb端classAextendsCprix：T;adsamethm=^（pds·c）mtsa端类B扩展Dprix：T;adsbmethn=^（pds·c）mtsb端288M. Cornélio等人/理论计算机科学电子笔记130（2005）2813.1代表团消除规则3.1允许在两个类之间消除委托，从左到右应用。从右到左的应用程序允许在类之间引入委托。在这条规则的左边，对类A的方法m的任何调用都被转发到类B。类A声明了类型B的属性b，并使用对象B初始化它。类B声明了类型T的属性x和属性adsb。在B的方法n中，可能会出现self表达式。X.在右边，类A没有声明类型B的属性，而是声明了同样在B中声明的属性x。A的方法m由定义B的方法n的相同参数化命令定义。证明我们可以用下面的方法来证明这个重构规则的可靠性。从左到右，使用Law_change_visibility：从private到public_change_visibility [12]，从左到右，我们将类B的属性x的可见性更改为public。我们消除了出现在类A的方法m内部的对类B的方法n的任何调用。然后，我们继续进行A类的数据细化。 我们使用定律2.3-私有属性耦合不变量和其他定律来进行数据细化。最后，我们利用law去掉了类A的属性b，属性消除[12]，从左到右。从右到左的证明是相似的。3.2接口客户端规则3.2接口客户关系（Interface Clientship）在类B和类D之间引入了客户关系，它通过使用abort定义方法m的主体来建模接口。类D被充分扩展（表示接口实现），以引入最初在类B中描述的概念。通过应用这个规则，我们可以在以后提供这个概念的不同实现。在这个规则的左边，类B声明了一个属性x，a方法m（mtsb中的其他方法）。在右边，我们引入类D，其方法m由带有bodyabort的参数化命令定义，对Java接口的效果进行建模。Java接口包含一组抽象方法的签名;通过定义要中止的方法体，我们给它们最抽象的定义。在这条规则的右边，类E扩展了D，声明了一个属性x并重新定义了m。B类是D的客户端，并初始化其at-M. Cornélio等人/理论计算机科学电子笔记130（2005）281289B类扩展A初级：T;广告bmethm=^（pdsm·cm[c J]）MB山端=cds，c端Mmethm=^（pdsm·c J）B类扩展Aprid：D;广告b我thm=^（pds m·c m [self. D.m]）new=fself. d：=新的E（）mtsb端类Dmethm=^（pdsm·abort）endE类扩展Dprix：T;第3.2条接口客户关系提供（→）（1）D和E不在cds中声明;（2）self。x未出现在mtsb中;（←）（1）在cds或c中不提述D类和E类。用E类的对象来表示d，以这种方式避免程序流产。命令c m是根据调用self来定义的。D. M.为了应用规则“接口客户身份”，从左到右，我们要求类D和E不在cds中声明。此外，属性x不应该在B的方法中访问，而不是m。为了从右向左应用这个规则，除了B类之外，不能有对D类和E类的引用。证明我们可以用下面的方法来证明这个重构规则的可靠性。我们使用法则2.2从右到左的类消去法引入类D和类E。但是，类E的属性x必须在初始时是公共的。下一步是290M. Cornélio等人/理论计算机科学电子笔记130（2005）281接口通信业务数据Fig. 1. 四层架构B类数据细化。我们不使用B类的属性x，而是使用E类的x，通过应用定律2.3私有属性耦合不变量。由于这个原因，我们引入带有公共属性x的类E。最后，通过使用Law将可见性从private更改为public，从右到左，我们将x的可见性更改为private。对x的访问现在通过调用E的方法m来实现。Q4分层架构根据分层架构构建的程序支持增强和重用[24]。因此，只要有必要，就应该进行面向对象程序的重构，以获得具有分层架构的最终程序[2]。在这里，我们的目标是一个分层的体系结构，最初是为面向对象的编程语言与关系数据库的集成而设计的[26]。架构的主要目的是尽可能避免数据存储和检索与实现系统功能需求的代码混合。为了实现这一目的，类被分成两组：描述系统（功能）需求建模所需的对象的类;以及用于数据存储和操作的类。这些组的类之间的连接由接口定义第一组类独立于数据存储和操作的有效实现，因为这些类不依赖于用于存储的数据结构的知识，而只依赖于接口定义的方法。第一组类包含我们所说的业务代码，它实现了系统的功能需求然而，第二组类知道如何实现持久性操作，并依赖于用于存储的数据结构。它们包含用于操作数据结构的数据代码更一般地说，这个架构被看作是由四个独立的层组成的（图1）.对功能需求进行建模的类构成业务层，而类用于数据存储和操作M. Cornélio等人/理论计算机科学电子笔记130（2005）281291构成数据层。包含子系统间通信代码的类组成通信层;实现用户界面的类组成界面层。在这里，我们将重点放在将应用程序结构化为业务层和数据层上。业务层的类分为三组：基本类，表示基本实体;集合类，表示基本对象组;控制类，定义功能需求的控制流程。集合类包括用于添加、搜索和移除集合项的方法，以及用于调用业务对象的典型操作的方法。如果采用外观模式[17]，则单个（控制）类合成应用程序的功能。从一个结构不良的系统，我们打算通过数据细化和重构规则的应用，达到一个结构良好的系统，遵守这里描述的分层体系结构。4.1建筑模式的衍生我们的重构策略包括三个阶段。每个阶段都涉及新类的引入，以及对现有类的数据和算法改进。数据细化通常涉及引入新的属性来重构类，以提高重用性。从第一阶段（阶段1）到最后一阶段（阶段3），程序根据前面描述的分层架构从结构不良的程序变为结构良好的程序。在实践中，可能没有必要遵循这里提出的所有步骤：开发人员应该确定其程序处于开发的哪个阶段，并从这个阶段到最后一个阶段应用重构。将开发划分为阶段的主要原因是简化了数据细化。阶段1在第一阶段，我们处理一个整体类数据和业务代码是混合的。这个阶段的目的是在这样一个单一的描述中识别基本的实体，并将每个实体建模为一个单独的类，以及它的相关属性和方法。图2给出了一个整体类的一般形式。 属性一个表是用来建立数据库模型的。aTable的类型由一个partial从类型T1到类型T2的单射函数（→）。使用方法更新来更新表的记录。它以记录标识符n及其新值m作为参数;它还有一个结果参数rp：一个报告更新是否成功的字符串。 首先，方法更新检查是否292M. Cornélio等人/理论计算机科学电子笔记130（2005）281类别应用程序priaTable：T1›→T2;.. .m=b（valn，m：T1，T2;resrp：string·if（n∈d o maTable）→sel f. aTable：=sel f. aTable{n<$→m};rp：=[]（n/∈domaTable）→rp：=（五）.. .端图二. 第一阶段开始时的应用程序类n属于aTable的域，aTable是一个业务规则。如果是，则aTable在位置n处用表达式exp更新，其中可能出现表达式m，即数据操作。方法update的主体中的符号''代表函数重写。Application类还提供了在表中插入新元素、删除现有元素的方法，以及检查与表域中给定元素相关联的值的方法。 在这一阶段结束时，我们希望将描述存储在表中的元素的概念（类）分开。类Application的转换如图3所示。我们通过使用法则2.2“类消去法”从右到左引入类BasicEntity。这个类捕获属性aTable的域和范围引入的概念。这个类为位于2的属性提供了get 和 set 方法 ， 因 为它随 着类 BasicEntity 的对 象的 生存 期而 改变 。attribute的值为1通常在对象创建时建立，并且不会在BasicEntity对象的生命周期中修改。这反映了一个事实，即属性1的行为就像一个键，用于识别在类Application中与它相关联的属性2。类BasicEntity表示实现系统的功能需求所必需的基本对象。类BasicEntitypriat1，at2：T1，T2;methse tAt 2 =^（valm：T2·self. at2：=m）methge tAt 2 =^（resm：T2·m：=self. at2）new=^（valn，m：T1，T2·self. a t1：=n;self. at2：=m）端下一步是准备类Application以进行数据细化。这种准备包括应用简单规范法[21，12]来定义属性aTable。本法的适用改变了转让-M. Cornélio等人/理论计算机科学电子笔记130（2005）281293类别应用程序pridata：seqBasicEntity;m=b（valn，m：T1，T2;resrp：string·varp，i：BasicEntity，int·self. return（n，i）;如果（p是基本实体）→p。setAt2（m）; self. data（i）：=p;rp：=“已更新“[]（p=null）→rp：=（fiend）methsearch=b（valj：int;resobj，pos：Pair，int.）. ）的方式...端图3.第三章。第一阶段结束时的应用程序类在相应的具体说明中。类别应用程序priaTable：T1→ T2;methupdate=^（valn，m：T1，T2;resrp：stringg·如果（n∈domaTable）→self. a表：[自我。aTable=self。a Table{n<$→m}];rp：=[]（n/∈domaTable）→rp：=“未更新“（五）...端之后，在原始类Application中引入了一个新的（私有）属性。我们使用 定 律 2.3-private 属 性 耦 合 不 变 式 来 向 Application 添 加 一 个 类 型 为seqBasicEntity（BasicEntity的序列）的属性数据。耦合不变量将新属性与旧属性联系起来。从数据细化的角度来看，新的变量是具体的变量。耦合不变量CI阶段1用于关联属性aTable和数据，它是类BasicEntity的对象序列。CI表1={i：0. . #da ta−1·da ta（i）. a t1›→da ta（i）. at2}（i，j：0.. #data − 1·i/= j data（i）. at1/= data（j）. 1）这个耦合不变量保证了aTable是由数据中存在的每个对象中的值相关的映射形成的。此外，数据中对象1处的属性值必须是不同的。294M. Cornélio等人/理论计算机科学电子笔记130（2005）281法则2.3将私有属性耦合不变式应用于类Application，根据数据细化法则改变了该类的方法[21]。正如预期的那样，规范语句和保护必须假设耦合不变量。现在的类Application如下。类别应用程序pridata：seqBasicEntity;主表：T1→T2;.methupdate=^（valn，m：T1，T2;resrp：stringg·如果（n∈doma Table<$CI）→self. a表：[CI，self. aTable= self。a表[n{ n<$→m} nCI];rp：=[]（n/∈doma表CI）→rp：=“未更新“（五）...端现在我们对类Application进行细化，以移除对抽象变量aTable的引用。首先，通过应用法则2.1，从右到左，我们介绍了类Application中的方法搜索。方法search返回一个BasicEntity类型的对象，其属性1与n具有相同的值。我们继续对规范语句和守卫进行算法改进。 所有应用方法均需进行此类细化。修订后的方法更新如下。methupdate=^（valn，m：T1，T2;resrp：stringg·varp，i：BasicEntity，int·self. return（n，i）;如果（p是基本实体）→p。setAt 2（m）; self. public void run（i）;rp：=“已更新“[]（p = null）→ rp：=“未更新“文件结束）方法update使用两个局部变量：p和i（参见图3）。首先，它调用新的方法search，在p中获取由n标识的对象，在i中获取其在数据中的索引。如果p为空，则不存在由n标识的元素，这通过rp报告。如果p不为null，则调用BasicEntity的方法将其值设置为包含参数m的表达式的值更新时，更新序列数据，并报告成功。在开发过程中，引入了变量p和i以及一个指定语句，该语句被细化以引入对方法search的调用，M. Cornélio等人/理论计算机科学电子笔记130（2005）281295类BusinessCollectionpridata：seqBasicEntity;m=b（valn，m：T1，T2;resrp：string·var p，i：BasicEntity，int·self. return（n，i）;如果（p是基本实体）→p。setAt2（m）; self. data（i）：=p;rp：=（fiend）methsearch=b（valj：T1;resbj，pos：BasicEntity，T1·.. . ）的方式...端类别应用程序pricollct：BusinessCollection;m=b（valn，m：T1，T2;resrp：string·收集update（n，m，rp））endnew=bcollct：=newBusinessCollection（）.. .端见图4。 第二阶段结束时的应用程序类图五、第2阶段结束时的类BusinessCollection也被类Application的其他方法调用，这些方法用于在数据中插入和删除对象。对BasicEntity方法的调用必须取代对（抽象）属性aTable的直接访问，之后，可以从类Application中删除该属性。这是通过使用类似于摩根[21]提出并在[12]中使用的定律来细化应用通过使用属性消除法则，我们从Application中删除了属性aTable。这个定律也在[12]中提出。阶段2在这个阶段，我们有一个程序，其中不同的概念被描述在不同的类中。最后，我们的目的是将类Application作为系统的外观，其中其方法的主体基本上通过方法调用将责任委托给业务集合。我们通过两个步骤获得类Application（图4）和BusinessCollection（图5）第一步是引入类BusinessCollection。然后，通过使用规则“委托消除”（规则3.1），从右到左，我们使类Application只是一个委托类。296M. Cornélio等人/理论计算机科学电子笔记130（2005）281类BusinessCollectionprirep：RepositoryClass;m=b（valn，m：T1，T2;resrp：string·var p，i：BasicEntity，int·rep. return（n，i）;如果（p是基本实体）→ p。setAt2（m）; rep. update（p，i）;rp：=（fiend）new=b sel f. rep：=新的Repsitory类Ref（）...端见图6。 第3阶段结束时的类BusinessCollection阶段3此时，集合类和持久性机制仍然是交织在一起的。这阻碍了重用和可扩展性，因为如果持久性机制被更改，则必须重新设计系统的一部分。在采用持久化机制时，应将可重用的业务代码与数据代码分离这就是这个阶段的目的我们继续应用规则“接口客户关系”（规则3.2），产生了新版本的类BusinessCollection （ 图 6 ） 和 新 类 RepositoryClass 和 RepositoryClassRef（图7）。注意，类BusinessCollection现在是RepositoryClass的客户端，并使用RepositoryClassRef对象初始化attributerep。此属性为目标调用 RepositoryClassRef 的 方 法 。 ClassRepositoryClass 定 义 了BusinessCollection 和 处 理 持 久 化 机 制 的 类 之 间 的 接 口 。 像RepositoryClass这样的类类似于Java接口.类RepositoryClassRef实现了对最初在类BusinessCollection中定义的数据结构的访问。接口的使用提供了集合和存储库类之间的独立性。例如，我们可以将存储库类从使用列表的类更改为使用树的类，而对集合类的影响最小。只有这个类的初始化器需要更改，以创建存储库的新实现的对象。我们现在有了一个按照第4节描述的体系结构构建的程序。这里描述的策略也可以用于获得根据三层架构构建的系统[6]。我们的体系结构和三层体系结构的主要区别是通信层的存在。M. Cornélio等人/理论计算机科学电子笔记130（2005）281297类RepositoryClassmethupdate=b（valobj，ind：BasicEntity，T1·abort）methsearch=b（valj：T1;resobj，pos：BasicEntity，T1·abort）...端类RepositoryClassRef扩展RepositoryClasspridata：seqBasicEntity;在此，我们使用了一种新的方法，该方法包括：将数据转换成数据，并将数据转换成数据，然后将数据转换成数据。data（ind）：=obj）methsearch=b（valj：T1;resbj，pos：BasicEntity，T1·.. . ）的方式...端见图7。 类RepositoryClass和RepositoryClassRef5相关工作与面向对象程序重构相关的文献包括Opdyke [23]的工作，它提出了一组必须满足的七个属性然而，没有证据表明，在这项工作中，满足这些属性保持程序的语义。我们的重构方法是基于法律的。每项法律都规定了必须满足的限制，以允许法律的适用。应用一个定律修改了一个程序，使其行为保持不变，因为每个定律的可靠性都是针对ROOL的最弱前提语义和[8，7]中定义的精化关系证明的[12]Fowler [16]建议，在开始重构之前，应该有一套可靠的测试，这些测试必须是自检的。每一次修改都必须经过程序编译和测试。然而，没有任何条件可以保证行为保持。使用代数定律进行重构，如这里所提出的，消除了编译程序的需要，因为定律应用的结果通过构造是正确的，无论是从句法还是从语义的角度来看。测试套件的使用是可选的。Cinn′eide和Ni xon[11]提出了一种方法，用于以半形式化的方法开发设计模式转换，以证明可维护性。他们识别出了微型图案，即在图案目录中重复出现的某些图案。对于每一个minipattern，一个minitrans-mation开发。一个小型转换包括一组先决条件，一系列的转换步骤，一组后置条件，和一个参数证明行为的保留。每一个小变换都是根据重构来定义的。他们的论点缺乏一个完全正式的AP的严谨性298M. Cornélio等人/理论计算机科学电子笔记130（2005）281接近没有基于语义的证据证明转换不会改变程序的行为，但它应该依赖于回归测试。Flores，Reynoso和Moore [15]使用RAISE规范语言来正式指定模式参与者的责任和协作他们使用他们的模型来指定任何面向对象的设计，这样他们就能够验证设计对应于给定的图案。没有关于将一种设计转换为另一种设计的讨论。Eden [14]提出了一种名为LePUS的声明性语言，用于指定设计模式的结构和行为方面。他认识到LePUS规范中的关系可以映射到不同编程语言的不同编程构造，尽管他认为设计模式描述中使用的关系集直接映射到静态类型编程语言中定义良好的语法构造。他没有提出任何系统的方法来进行这种翻译。他还认为，LePUS的原型工具可以在Prolog中开发，允许在程序中操纵表示修改的公式。然而，在这一领域的实际成果并不明显，但在他发表的工作。在我们的方法中，我们转换一个特定的设计，目的是根据设计或建筑模式获得一个新的设计。转换是通过使用元语言元素编写的规则来完成的，比如表示属性的元变量，但是使用的语言非常类似于ROOL，我们用来编写程序的语言Lano等人 [19]通过将两组类（“之后”系统由根据模式组织的类的集合组成。证明“后”系统是“前”系统的扩展是通过一个合适的解释，证明了选定的公理。不同的是，我们采用了一种基于规则的建设性的转型方法，而不是基于系统扩展原始系统的验证6结论本文阐述了如何重构的面向对象程序可以在一个正式的方式，通过使用基于规则的方法来完成。这是基于重构规则的应用[12]。所提出的获得具有分层架构的系统的策略还涉及经典的数据细化[21]和算法细化。程序转换的可靠性，使其遵循架构模式或设计模式，依赖于重构规则的使用，M. Cornélio等人/理论计算机科学电子笔记130（2005）281299最后，关于编程法则和数据精炼的使用。重构规则的推导是基于使用处理命令式命令和面向对象特性的编程法则，其针对ROOL的形式语义的可靠性证明[8，7]被提出[12]。尽管我们使用的是一种具有复制语义的语言，但迄今为止的经验表明，这并不是重构的障碍我们的研究的一个显着特点是使用一个简单的，统一的，模块化的推理机制的设计实践的正式justification：一组基本的代数规律ROOL。我们的总体目标是正式面向对象的设计实践。我们目前正在研究成熟的设计模式[17]。这对于面向对象程序的形式化重构的实践，以及对旨在根据设计模式构建系统的设计更改的有效性进行形式化证明，都是非常重要的。在[12]中，我们已经提出了转换，通过使用重构规则，将系统重构为符合Facade Pattern [17]的系统。 这里介绍的外观模式和架构模式都是通过应用重构规则获得的。作为未来的工作，我们计划建立一个工具来机械化的规则应用程序的转换。我们打算通过使用像Elan [5]这样的系统来机械化编程定律的应用。这将作为重构规则以及架构和设计模式的机械化派生的基础。一旦编程法则和重构规则被机械化，就有可能构建一个环境来推理程序转换，并保证语义的完全形式化。引用[1] 回来，河。J.R.，程序抽象在精化微积分，技术报告，计算机科学系，阿波-芬兰（1987年），ser.A. 号55个。[2] 回来，河。J.R.，软件构造的逐步特征介绍，在：D。B. et. al. ZB2002：Formal Specificationand Development in Z and B，Lecture Notes in Computer Science2272，2002，pp. 162-183。[3] B 或 b a ， P. 、 杨 A.S am p aio ， A.我 不 能 和 M 一 起 去 。 Corn'elio ，AlgebraicReasoningfororObject-OrientedProgramming ， Science of Computer Programming（2004），pp.53-100.[4] Borba ， P. 、 杨 A.是 一 个 MP AIO 和 M 。 Corn'elio ， Areefinementalgebraforrobject-orienteddprogramming ， in ： L.Cardelli ， editor ， European Conference on Object-OrientedProgramming，ECOOP257-282.[5] Borova n sky'，P. 等。，http://www.loria.fr/equipes/protheo/SOFTWARES/ELAN/manual/index-。
