统一过程中形式化方法的应用及优势研究

理论计算机科学电子笔记101（2004）95-127www.elsevier.com/locate/entcs统一UML1的视图Zhiming Liu，He Jifeng，Jing Liu中国澳门特别行政区联合国大学国际软件技术研究所萧山里澳门大学软件工程学院，澳门特别行政区，中国摘要我们提出了一种将形式化方法嵌入到Rational统一过程（RUP）中的方法其目的是：（a）统一建模语言的不同观点;（b）以形式化方法加强统一建模语言，以改善软件系统的质素;及（c）提供统一的概念架构，以迭代和渐进的方式，支持有效地使用形式化方法进行系统规格说明和推理。RUP的主要特征之一是它是用例驱动的，并且比其他过程模型（如瀑布模型）更明确地支持迭代开发面向对象还支持比传统的命令式编程更好和更显式的增量编程这些将有助于在软件系统开发中推广使用形式化方法该模型基于Hoare和He关键词：面向对象，RUP，UML，UTP1介绍如今，一个软件系统，如用于医疗保健、社会保障或国防的软件系统，是一个用程序表示的真实世界的模型（部分）。1电子邮件：lzm@iist.unu.ed u，hjf @i ist. u nu。ed u，xsl @u ma c.m o.Z.刘先生于英国莱斯特大学计算机科学系休假;他是从华东师范大学，上海，中国休假。J. Liu正在中国上海大学休假。本研究得到了MoE 02104研究基金和科技部973项目2002CB 312000的部分资助。1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.02.01896Z. Liu等/ Electronic Notes in Theoretical Computer Science 101（2004）95-127明语。随着现实世界的不断变化，代表它的软件系统需要不断地维护和发展。开发和维护这样一个不断发展的软件系统显然是困难的。一个纪律严明的过程和一个良好的建模符号是必不可少的控制活动，在构建和记录不同的模型在不同阶段的软件开发。Rational统一过程（RUP）[32]已经成为一种流行的软件开发过程[33，38，31]。作为建模符号，RUP使用UML [9]，这是在广泛的应用中开发软件的事实上的标准建模语言。RUP促进了几个最佳实践，但是其中一个最重要的是用例驱动和迭代开发的思想。 在RUP的用例驱动和迭代方法中，系统开发被组织为一系列短的、固定长度的小型项目，称为迭代，每个项目用于少量的用例。每个迭代都包括它自己的需求分析、设计、实现和测试/验证活动，在下面的小节中进行了描述。尽管RUP和UML实际上很流行，但它们没有一个良好的形式化方法，使得很难分析UML规范的一致性。这项工作是为了一个正式的方法与RUP和UML的集成。第2节简要讨论了RUP中的活动和UML模型。我们在第3节中总结了我们方法的主要思想。第4节介绍了一个面向对象的符号，将用于所提出的形式化方法。第5节展示了在UML模型的规范中规范符号的使用。我们将使用一个图书馆系统作为例子来说明在RUP的不同周期中创建的模型的处理，而不是深入到UML的形式化的细节中。最后，第6节以讨论结束本文。第7节讨论了与现有工作的关系。2RUP和UML如前所述，每个RUP迭代都包括它自己的需求分析、设计、实现、测试和验证活动。2.1需求分析迭代的需求分析是为需求创建一个UML模型，其中包含一个用例模型和一个概念类模型。Z. Liu等/ Electronic Notes in Theoretical Computer Science 101（2004）95-12797图书馆1 * Pub 1 *复制.........概念模型用例模型用例模型：自由：RMH：会员：自由LS Lib Pub......这是什么？......m1 m2 m3副本......这是什么？执行执行：复：酒吧：LSLS Lib Pub......这是什么？......m1 m2 m3副本......这是什么？：LS：Pub：库：复制.........概念模型图书馆1 * Pub 1 *复制1*构件...构件...M5Fig. 1.迭代软件开发过程用例模型由用例图和每个用例的文本描述组成。用例图只提供关于用例的静态信息。在用例的文本描述中描述的功能和行为属性部分地表示为用例和系统的参与者之间的交互序列。UML系统序列图用于描述用例的参与者与被视为黑盒的系统之间的交互的可能顺序重要的是要注意，系统序列图没有也不应该提供系统内部对象之间的交互信息[14，38，40]，因为这些内部交互是设计所关注的。用例模型的形式化应该处理交互的顺序（即交互视图）和由这些交互引起的状态变化，即功能和行为视图。对象约束语言（OCL）[53]，作为UML的一部分，可以描述一些功能方面，例如操作的前置和后置条件然而，八达通卡没有实施设计要求98Z. Liu等/ Electronic Notes in Theoretical Computer Science 101（2004）95-127它是一种形式化的语义，在描述面向对象的许多有用方面（如递归方法调用、动态绑定）时，它的表达能力不够。在本文中，我们将定义一种面向对象的规范语言（OOL），它可以用来在不同的抽象层次上指定函数行为。概念模型是由类（也称为概念）和类之间的关联组成的类图。一个类代表一组概念对象，而一个关联决定了关联类中的对象在应用程序域中的关系。在这个层次上我们称类图为概念图的原因是它不关心对象做什么，它如何行为，或者属性如何表示。这些问题的决定将在设计阶段作出，的用例被分解并分配给适当的对象。UML社区认为类模型表示静态视图，而用例模型表示需求的动态和交互视图2.2设计设计是将需求模型转换为由设计类图和交互图族组成的设计模型。交互图表示设计的交互视图，显示系统的对象如何相互交互和协作。交互图的创建主要涉及对对象的职责分配，以便它们的交互正确地实现用例。根据对象维护的知识进行用例分解和职责分配。 对象能做什么取决于它知道什么，尽管对象不必做它能做的所有事情。一个对象所知道的是由它的属性和与其他对象的关联决定的。在确定了对象的责任之后，可以确定关联的方向（即从一个对象到另一个对象的导航和可见性）和类的方法。 这将导致建筑设计类图，显示设计的静态视图，即概念类图的概念和关联是如何通过软件类实现的。2.3执行实现是用编程语言对设计进行编码。在面向对象的编程语言中，这是根据设计类图中的类及其方法定义软件类，Z. Liu等/ Electronic Notes in Theoretical Computer Science 101（2004）95-12799交互图一旦获得了交互图和设计类图，就可以很容易地从中生成代码。可以开发一个工具来帮助将设计转换为实现代码。2.4迭代和增量模型构建RUP中的迭代生命周期是基于通过多次迭代对系统的连续扩展和细化，并以循环反馈和适应作为核心驱动来收敛到一个合适的系统。系统会随着时间的推移逐步增长，一次迭代接着一次迭代，因此这种方法也被称为迭代和增量（参见图1）。 早期的迭代过程思想被称为螺旋式开发和进化式开发[7]。然而，RUP中的新特性是用例驱动的本质，以及对面向对象和增量开发的明确支持。每个周期可能会考虑一个或多个要分析的用例，并为它们构建一个概念模型。然后这些用例可以被设计来创建交互图和设计类图。然后对设计进行验证、编码和测试。这一个循环也可以通过轮流使用用例或用例的“部分”以迭代的方式再次完成。在下一个周期中，我们可能会从上一个周期中提取一个用例的细化或扩展版本，并细化或扩展系统，或者我们会提取一些新的用例来分析、设计和实现。因此，在新的迭代中创建的模型是在前一次迭代中获得的模型的细化和扩大。如图1所示。在每次迭代中，用例模型和概念模型之间的关系是概念模型指定了环境，即状态空间，用例将在该环境下执行。状态是一个对象图，它由一组对象和这些对象之间的一组链接如果概念模型足以实现用例模型所需的功能服务，则它与用例模型一致。这种一致性需要在每个周期中进行检查。需要根据相同迭代的需求规范验证设计规范。并且在接下来的周期中需要保持一致性和正确性。将形式化方法集成到RUP中的主要目的是允许这些检查被精确地执行。3方法概述在本文中，我们将关注RUP的增量和迭代特性，并解决以下问题：100Z. Liu等/ Electronic Notes in Theoretical Computer Science 101（2004）95-127(i) 如何在迭代中形式化需求的UML模型，并确保模型的静态和动态视图之间的一致性？(ii) 如何形式化迭代设计的UML模型，并确保其静态和动态/交互视图之间的一致性(iii) 如何将设计的UML模型和迭代的需求形式化地联系起来？(iv) 如何在重复迭代中保持已建立的一致性和正确性？我们通过首先开发面向对象编程的正式框架来解决这些问题该框架包括一个面向对象的规范语言（OOL）和一个面向对象设计的改进演算（COOL）。演算是关系和预测的，它基于Hoare和He然后，我们将研究如何在设计演算中对需求和设计的UML模型进行形式化表示和推理。当形式化需求的UML模型RM=（cm，um）时，我们将静态视图cm描述为声明部分cdeclscm，并通过程序命令指定cum来描述用例模型um。因此，RM被定义为一个面向对象的程序规范cdeclscm·cum。 的语义在OOL的语义中给出了cdeclscm、cum及其组合·。这形式化捕获CM和UM的语法和语义以及它们之间的一致性。命令cum指定了对系统状态执行什么操作以及可能的顺序。一个系统状态实际上是类图cm的一个对象图。由于无法决定用例执行的顺序，OOL将允许非确定性的规范。因此，OOL不仅将形式化一些UML模型，而且还补充UML以提供用例的功能规范的属性，例如类不变量和类之间关联的约束可以在逻辑中推理。类和用例模型中的一致性更改可以通过保留这些属性甚至通过细化来确保类似地，对于由设计类图dc和序列图的家族sd组成的设计DM=（dc，sd）的UML模型，我们用OOL中的声明部分cdeclsdc来形式化设计类图dc这个声明部分中的类现在有了方法，一个类的方法可以调用其他类的方法。因此，这些方法的规范描述了序列图中的对象交互。但是，方法仍然可以通过主程序csd中的命令激活。因此，设计的UML模型（dc，sd）也被指定为声明Z. Liu等/ Electronic Notes in Theoretical Computer Science 101（2004）95-127101部分和一个主程序（同样没有对应的UML）：cdeclsdc·csd。类图dc和对象序列图sd之间的一致性由cdeclsdc的语义和OOL中方法调用的语义来捕获。实际上，设计类图中方法的具体化结合了UML中没有对应的功能视图和UML中对象状态描述的行为视图图和由UML对象交互图捕获的交互视图。设计模型（dc，sd）相对于需求模型（cm，um）的正确性由细化关系定义cdeclscm·c um±cdecls dc·c sd精化也可以用来证明增量设计的步骤（例如，在[33，38]中非正式使用的那些），例如添加属性，将属性从子类提升到超类，封装属性，将对象的功能委托给其关联的对象，等等。精化演算与RUP的这种集成使得设计演算在迭代和增量方式中的使用更加有效，以便在迭代的每个阶段只处理4面向对象规范语言我们开发了一种面向对象的语言，具有类、引用、可见性、动态绑定、嵌套声明和相互递归方法调用。[29]类声明和命令将被定义为设计，这一概念在[29]中定义。4.1语法一个程序的形式是cdecls·P，其中cdecls是声明部分，P是一个命令，可以理解为Java程序的主方法。main方法命令对应于一个活动类。在本文中，我们只处理顺序程序，因此我们不处理一般的活动类。 因此，在这种情况下，对象的状态图将从调用方法时的状态开始，然后状态更改将根据方法定义进行在多线程计算中，我们将有多个4.1.1类声明我们假设一组类名CName。声明节cdecls的格式为cdecls：：= cdecl|cdecls;cdecl，其中cdecl是102Z. Liu等/ Electronic Notes in Theoretical Computer Science 101（2004）95-127以下形式ClassN extendsM{privateU u=a， protectedV v=b， publicW w=d;methodm1（T11x1，T12y1，T13z1）{c1};· ··;m（T1x，T2y，T3z）{c}}哪里• N和M是CName中类的名称，M称为N的直接超类，扩展部分是可选的。• private声明声明了类的私有属性u，它们的类型U和初始值a，同样，protected和public属性的protected和public声明在Java中的含义。我们定义defpri（N）={U a=u| Ua=u∈U u= a}类似的还有pro（N）和pub（N）。我们使用attr（N）表示这三组属性的并集;对于N的属性u，我们使用dcltype（N.u）表示a的类型，Init（N.u）表示在N中声明的u的初始值。• 方法声明声明了方法，它们的值参数Ti1xi，结果参数Ti2yi，值-结果参数Ti3zi和bodiesci，由val（N. mi），res（N. mi），valres（N.mi）和body（N.mi）表示，分别我们也将简单地使用m（k）{c}来表示方法dec-k。我们将使用Java约定来编写一个类规范，并假设一个属性在没有标记为private或public时受到保护。4.1.2命令我们的语言支持典型的面向对象编程结构：c：：=跳过|混乱|c; c终止，中止，序列| varTx=e|端x局部变量声明和取消声明| c <$b <$c|条件选择与非确定性选择| b/c |read（T x）迭代并读入一个值| C.new（x）对象创建| le.m（e，v，u）赋值和方法调用|le.m(e, v, u) assignment and method call其中b是布尔表达式，e是表达式，le是可能出现在赋值左侧的表达式，其形式为le：= x|le.a|其中x是一个简单变量，a是一个对象的属性。Z. Liu等/ Electronic Notes in Theoretical Computer Science 101（2004）95-1271034.1.3表达式表达式可以出现在赋值语句的右侧，它是根据下面的规则构造的。e：：= x|null|自我|e.a|f（e）其中null表示特殊类的特殊对象。 注意，表达式可以作为方法调用的参数出现，但我们不允许方法调用是表达式，因为我们在方法中显式使用结果和我们可以包括更多的表达式，如类型转换（C）e和类型测试（e是C），但它们在本文中不需要4.2语义在UTP [29]中，程序或程序命令被识别为设计，其由对（α，P）表示，其中• α表示程序的变量集。• P是形式为p（x）J定义p（x））R（x，x）=（ok其中x和xJ代表程序变量x∈α的初始值和最终值，谓词p被称为程序的前提条件，它表征了程序的激活将导致其执行的初始状态。终止，而谓词R，称为程序的后置条件，将程序的初始状态与其最终状态联系起来我们描述了一个程序的终止行为的布尔变量ok和okJ，前者是真的，如果程序被正确激活，后者成为真的，如果程序的执行成功终止。程 序命 令 通 常修 改 程 序变 量α 的 子集 。 设 V 是 α 的 子集 ， 记 法 V ：（p<$R）表示（框架）设计p（RwJ=w）其中w包含α中除V外的所有变量。 V被称为设计P的框架。 在例子中，我们经常省略设计的框架假设一个设计只有在变量x的启动版本xJ出现在设计中时才改变变量xA设计D2def=（α，P2）称为D1的精化def=（α，P1），表示为D1±D2，如果P2包含P1，即x，xJ，.，z，zJ·（P 2 （1）这里我们假设α包含x，...，z.104Z. Liu等/ Electronic Notes in Theoretical Computer Science 101（2004）95-1271设ρ是从α2到α1的映射，也可以定义为设计，则def设计D2=（α2，P2）是在映射D1=（α1，P1）在映射ρ下，如果<$x∈α，<$yJ∈αJ·（（ρ;P）<$（P;ρ））211 2其中αJ是α1中这些变量的素数版本的集合;而语义后文正式定义了连续合成的抽搐我们将遵循这种为编程语言定义基于状态的模型的经典方法，并根据变量、状态、表达式、命令、声明和程序来定义我们的OOL。然而，为了简单起见，上面的模型采用了通用数据类型，既不允许引用类型，也不允许嵌套声明。为了形式化面向对象程序的行为，我们必须考虑以下特征：• 程序不仅对原始类型的变量（如整数）进行操作，还对引用类型的对象进行操作。• 为了保护属性免受非法访问，模型必须解决属性对环境的可见性• 一个对象可以与它最初声明的子类相关联。要在动态绑定环境中验证表达式和命令，模型必须跟踪每个对象的当前类型4.2.1价值观和目标值可以是基元类型的成员，也可以是对象标识。我们假设可以引用的对象身份的无限集合REF，并且null∈REF。对象o是由以下结构o：：= null|re f <，type，state>其中ref∈REF，type是类名，state是从attr（type）到对象的映射。对于一个对象o=，我们用identity（o）表示o的identityref，type（o）表示对象的类型名Co，state（o）（a）表示类C的属性a的值σ（a）。 当没有混淆时，我们也用C来表示对象的集合o，使得type（o）=C，在这种情况下，C也表示语义类/类型，我们可以说o∈C。设O是所有对象的集合，包括null，使得对于O中的任何o1和o2，identity（o1）=identity（o2）意味着type（o1）=type（o2）和state（o1）=state（o2）。因此，我们可以使用O中对象的恒等式来引用对象。在本文的其余部分，对象o=表示O中的一个，如果没有混淆，将使用ref. a表示state（o）（a），type（ref）表示type（o）。Z. Liu等/ Electronic Notes in Theoretical Computer Science 101（2004）95-127105JŒ符号：我们引入以下符号：• 一个类N称为M的一个子类，记为N≤M，如果N=N或N = M，或存在有限集合{C i|0 ≤ i ≤ n}的类，使得N=C 0，M=Cn 且super（Ci）=Ci +1，对于0≤i n• 设s=< s1，.，s k>是非空序列。 我们用head（s）来表示defs的第一个元素s1; tail（s）= ，这是序列ob-从s中删除第一个元素（可以是空列表<>）;|s的长度k;和π i（s）第i个元素s i，对于i ∈ { 1，...|the length k of s;and π i (s) the ith element s i, for i ∈ {1,...，k}。• 设S和S1是集合。为了在语义定义的上下文中更好地阅读，我们将S1S定义为从S中删除了S1的元素的集合。• 对映射F：D−→E，d∈D，r∈EdefF{d<$→r}J<$$>b∈{d}<$D·FJ（b）=F（b）=F，其中F（d）=r• 对于一个对象o=，一个C的属性a和一个实体d，它要么是一个原始类型的成员，要么是O中的一个对象，defref{a<$→d}=• 对于对象的集合S O，defS ± {}={o|identity（o）= ref}S{}defRef（S）={ref|ref是S中对象的标识}4.2.2变量和状态我们的模型描述了一个面向对象的程序的行为的设计包含以下逻辑变量作为其自由变量。(i) cn：它的值是到目前为止声明的类名的集合，它被类声明修改。(ii) 每个类N∈cn与(a) attr（N）：类N的（声明的或继承的）属性的集合。我们还使用a∈ attr（N）来表示a是类N的属性名。(b) op（N）：类N的（声明的和继承的）方法的集合。{m1<$→（m 1，D 1），···，mk<$→（mk，Dk）}它指出每个方法mi都有一个形式参数作为它的形式参数，并且mi的行为由Def（N.mi）所指的设计Di这些变量由类声明修改。(iii) 对于每一个N∈cn，n（N）是当前存在于程序执行中的类N的对象的集合，并且它将通过创建一个新对象（并销毁我们在此106Z. Liu等/ Electronic Notes in Theoretical Computer Science 101（2004）95-127（纸）。让def= [N∈cn（N）(iv) super：将类映射到其直接超类的部分函数。这个变量也被一个类声明修改。(v) var：它的值是程序已知的变量的集合。由于我们的语言允许嵌套声明，var将每个变量与一个类型序列相 关联{（x 1，），·· ·，（xn，）}其中，对于i∈ {1，.，n}，是x i的最近声明的类型，并由dcltype（x i）表示。我们还将使用var（x）来表示与x关联的类型序列。(vi) visattr：它的值是从当前类内部可见的属性集，即所有声明的属性加上超类的受保护属性和所有公共属性。这个值将被程序的整个声明和变量的重新声明修改。(vii) x：这个逻辑变量表示变量x的状态。由于变量可以被重新声明，它的状态通常是一个非空的有限值序列，其第一个（头）元素表示变量x的当前值。基元数据类型的变量可以将该类型的任何成员作为其值。但是，对象变量可以存储对象名称或标识作为其值。4.2.3表达式求值表达式e的求值决定了它的类型type（e）和它的值。该评估利用每个类C∈cn的状态。• 一个变量x是定义良好的，如果它是在var中声明的，它的类型是原始的，那么它的当前值是这个类型的成员，或者是cn中的一个类，在这种情况下，它的当前值是一个对象的标识defD（x）= x∈var<$（dcltype（x）是本原的<$dcltype（x）∈cn）∧dcltype（x）是本原的，所以dcltype（x）∈dcltype（x）∧dcltype（x）∈cnhead（x）∈Ref（（dcltype（x））类型（x）def=defdcltype（x）如果dcltype（x）是原始的type（head（x））否则value（x）=head（x）• 空对象表达式，defdefdefD（null）=true，type（null）=NU LL，value（null）=null• self是一个特殊的变量，它的类型必须是cn中的类，它是Z. Liu等/ Electronic Notes in Theoretical Computer Science 101（2004）95-127107以与其他变量相同的方式进行评估，defD（自身）类型（self）值（self）= self∈vardcltype（self）∈cn∧head（self）∈Ref（（dcltype（self）def=type（head（self））def=head（self）• 只有当le是类的类型并且附加到非空对象，并且a是属性名称时，才定义属性le. a因此，属性归纳定义如下：defD（x.a）=D（x）dcltype（x）∈cnhead（x）/=nulln（x）.a∈visattr类型（x.a）值（x.a）def=type（head（x）.a）def=head（x）.aD（le.a）值（le.a）类型（le.a）def=D（le）型（le）.a∈visattrdef= vaule（le）.adef= type（value（le）.a）• 下面举例说明了内置表达式的良好定义和求值D（e/f）def=D（e）<$D（f）<$type（e）=实数类型（f）=实际值（f）= 0值（e/f）def=值（e）/值（f）等式e1=e2的语义是引用等式：D（e1）<$D（e 2）<$（value（e 1）=value（e 2））<$（type（e 1）=type（e 2））4.2.4命令的语义面向对象程序执行的一个典型方面是如何将对象附加到程序变量（或实体[43]）。附加是通过赋值、创建对象或在方法调用中传递参数来实现的。当我们定义语言的元素E的语义[E]时，我们将使用E本身在语义定义方程中表示其语义命令skip终止并且不改变状态defskip=：（truetrue）指挥混乱有最弱的规范defchaos=：（falsetrue）答：有两种情况下的任务。第一个是将一个值（重新）附加到一个变量上。只有当对象的类型与变量的声明类型一致时，才价值观的依附108Z. Liu等/ Electronic Notes in Theoretical Computer Science 101（2004）95-127¢ ¢B@C一其他变量都不会改变。defx：=e={x}：D（x）<$D（e）<$（type（e）≤dcltype（x））<$（xJ=value（e）>·tail（x））第二种情况是修改附加到变量的对象的属性值。 这是通过在系统状态树中查找附加对象并相应地修改其状态来完成的。因此，所有指向此对象标识的变量都将被更改。defle.a：=e= {（type（le））}：（D（le.a）D（e）（type（e）≤dcltype（le.a）（（type（le））J=（type（le））± {value（le）<${a <$→value（e）}）条件选择：以传统方式定义：P<$b<$Q我们使用def=（D（b）类型（b）=布尔）（Pif{（bi−→ci）|1≤i≤n}文件来表示多项选择语句。它的语义被定义为设计^n_n（D（bi）类型（bi）=布尔型） （值（bi）ci）i=1i =1非确定性选择定义为defPHQ=P顺序组合对应于关系组合：JJdefJP（s，s）;Q（s，s）=<$m·P（s，m）<$Q（m，s）循环语句是根据最弱的固定点定义的：孟加拉国def= µX。（P;X）b skip对象创建：C.New（x）（重新）声明变量x，创建一个新对象，将对象附加到x并附加初始值 也就是x的属性。defC0. New（x）={var，x，n（C）}：C∈cnref/∈Ref（n）·1（C）J<=|a∈attr（C）}>}BJCB（x∈var（x=ref>·x））<$CB（varJ={x}<$var<${（x，C>·var（x））}）<$C（x/∈var（xJ=）（varJ=var{（x，C>）}））我们使用C.New（x）[c]来表示命令C.New（x）; x。a：= c，其中a是C的属性列表，c是相同长度的表达式列表。Z. Liu等/ Electronic Notes in Theoretical Computer Science 101（2004）95-127109@x={，x}：（x∈ ）。一变量声明：声明一个变量并将其命名为：defvarT x=e={x，var}：D（e）（type（e）≤T）0 1（（x∈varxJ=value（e）>·xBvarJ={x}<$var<${T>·var（x）}<$Cx/∈var<$（xJ=value（e）>）<$（varJ=var<${（x，T>）}）<变量取消声明：终止允许使用变量的块：def端无功。！（|var（x）|= 1 varJ={x} var）（|var（x）|> 1 xJ= tail（x）varJ={x}{（x，tail（var（x）}）读值：定义为defread（T x）=c0·（varT x=c 0）方法调用：设v、r和vr为表达式列表。命令le.m（v，r，vr）将实际参数v和vr的值赋给le引用的对象o的方法m的形式值和值结果参数，然后执行m的主体。在它终止之后，m的result和value-result参数的值被传递回实际参数r和vr。defle.m（v，r，vr）= D（le）<$type（le）∈ cn <$m ∈ op（type（le））<$ ！varN self=le，T1x=v， T2y=r， T3z=vr;N·（type（le）=N）n（N.m）;r，vr：=y，z;endself，x，y，z其中x，y，z是类别类型（le）方法的值、结果和值-结果参数，而m（N.m）代表与类别N的方法m相关的设计，将在第4.2.6节中定义。4.2.5类声明的语义如果下面的条件成立，那么在4.1.1节中给出的类声明cdecl(i) N之前没有声明过： N/∈cn， N和 M是不同的： N/= M，N的属性名是不同的不同的（u·v·w）可以明确定义的地方。(ii) 属性的初始值与其对应的类型匹配。1.. m·type（ui）= Ui i：1.. n·type（vi）= Vi中文（简体）k：·type（wi）= Wi(iii) 方法名称是不同的distinct（）110Z. Liu等/ Electronic Notes in Theoretical Computer Science 101（2004）95-127BC@一(iv) 每种方法的参数都是不同的。1.. l·。！不同的（xi·yi·zi）|Xi|为|Ti1| ∧ |yi|为|Ti2| ∧ |zi|为|Ti3|令D（cdecl）表示上述条件的合取。类dec-dec_decl将类N的结构信息添加到后续程序的状态中，该角色的特征在于以下设计。defcdecl={cn，super，pri，protattr，pub}：D（cdecl）0cnJ=cn<${N}<$superJ=super<${N<$→M}<$1BJ CBpri=pri{N<$→{U u=a>}}C}}C}}C∈pub（N）}B<$N ∈ cn·attrJ（N）=<${pri（N）<$pro（M）<$pub（M）|N ≤ M} C@AopJ（N）={m <$→（n，n（N.m））|m ∈ op（M）<$N ≤ M}其中设计族由一组递归方程定义。对于每个类N∈cn，每个类M使得N≤M，以及每个方法m∈op（M），它包含一个方程n（N.m）=FN.m（n）其中超级类（N）=M其中F是根据以下情况构造的。情形（1）m不是在N中定义的，而是在N的一个超类中，即 m/∈ op（N）<$m ∈ <${op（M）|N ≤ M}。然后，在N的环境中对方法m的调用将根据声明该方法的N的最低超类中的m的定义执行设M是N的最低超类，即m在M中声明，但M的子类都不声明m。在这种情况下，FN.m（n）的定义方程为：defFN.m（N）=Set（N）;φ N（body（M.m））;ResetCase（2）m是定义在类N中的方法。在这种情况下，方法N.m的行为由其主体和执行defFN.m（N）=Set（N）;φ N（body（N.m））;Reset其中设计Set（N）找出类N可见的所有属性，而Reset为主程序执行此操作：defJ设置（N）={visattr}：true_visattr =！{不适用|a ∈ pri（N）}<${M.a|N≤M，a ∈ pro（M）}{M. a|M ∈ cn，a ∈ pub（M）}defJReset= {visattr}：true_visattr={M.a|M ∈ cn，a ∈ pub（M）}函数φN重命名代码中类N的属性和方法body（N.m）通过添加对象引用self：defφN（skip）=skipdefφN（混沌）=混沌defφN（p1;p 2）=φN（p 1）;Set（N）;φN（p 2）defφN（P1ab dP 2）=φN（P 1）aφN（b）dφN（P 2）defφN（P1HP 2）=φN（P 1）HφN（P 2）defφN（b<$P）=φN（b）<$（φN（P）;Set（N））112Z. Liu等/ Electronic Notes in Theoretical Computer Science 101（2004）95-127defφN（varT x=e）=varx：T=φ N（e）defφN（endx）=endxdefφN（C.New（x））=C.New（φ N（x））defφN（le：=e）=φ N（le）：=φ N（e）defφN（le.m（v，r，vr））=φ N（le）.m（φ N（v），φ N（r），φ N（vr））defφN（m（v，r，（vr））=se lf. m（φN（v），φN（r），φN（vr））defφN（x）=defself.x<$M·N≤M<$x∈attr（M）X否则φN（self）=selfdefφN（le.a）=φ N（le）.adefφN（null）=nulldefφN（f（e））=f（φ N（e））请注意，我们没有引入语法super.m来根据超类中的定义显式地指示对方法的调用。 相反，a方法调用将根据继承层次结构中最低位置的方法定义引入super.m并相应地定义其语义没有困难5UML模型本节以图书馆系统的迭代开发为例，说明如何指定和推理需求分析和设计的UML模型我们建议读者参考我们的论文[40]以获得UML需求模型的形式化规范的细节，并参考[37，36]以获得UML序列图的形式化5.1概念类图类图中的类被指定为类声明。两个类N和M之间的关联是N和M的对象对的类型，并且被建模为具有两个属性的类，其中关联假设一个库系统开发的迭代考虑记录一个副本的用例和图2左图中的概念模型。 一个图书馆拥有许多出版物，每个出版物包含一些副本。我们将此图指定为下面的CM1ClassLib{String name，String address}; ClassCopy{String id};ClassP ub{String id，String title，String author，String isbn};ClassContains{