没有合适的资源?快使用搜索试试~ 我知道了~
OCL消息的形式语义与对象模型相关的研究
理论计算机科学电子笔记102(2004)77-97www.elsevier.com/locate/entcsOCL消息的形式语义Stephan Flake和Wolfgang Mueller1C-LAB,帕德博恩大学Fuerstenallee 1133102帕德博恩,德国摘要最新的OCL 2.0提案提供了两种语义描述,即,一种基于元模型的语义,它使用UML本身来将语义域与语言概念相关联,另一种基于称为对象模型的集合论方法的形式语义。不幸的是,这两种语义目前既不一致也不完整,因为(a)形式语义没有考虑新引入的OCL消息的概念,以及(b)这两种语义都缺乏Statecharts的集成和状态相关操作的语义定义本文重点讨论OCL消息的形式化语义,作为两种OCL语义之间一致性的基础。我们扩展了对象模型,并提出了一个系统状态的扩展定义,包括所有相关信息,以便能够评估OCL表达式也w.r.t. OCL消息。保留字:OCL 2.0,扩展对象模型1介绍所采用的OCL 2.0提案遵循两种方法来定义OCL的语义首先,通过基于元模型的方法使用UML本身描述语义[6,第5章]。不同的包被定义为表示元模型层M2上的抽象语法和UML建模层M1上的语义域。然后,一个单独的包通过语义域的元素和抽象语法的元素之间的关联来关联这些包例如,语义域的每个值与抽象语法的类型相关联。类似地,OCL表达式的求值与抽象语法中的相应表达式相特定1电子邮件:{flake,jinggang}@ c-lab.de1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi:10.1016/j.entcs.2004.09.00978S.弗莱克,W. Mueller / Electronic Notes in Theoretical Computer Science 102(2004)=≺∈def在给定的系统快照上执行OCL表达式的评估,使得作为结果产生唯一值此外,形式语义是由一种称为对象模型的集合论数学方法定义的,该方法基于M.里希特[10]。对象模型是一个元组Mdef。CLASS,ATT,OP,ASSOC,ASSOC,ASSOC,associates,roles,multiplicities具有类的集合CLASS、属性的集合ATT、操作的集合OP、关联的集合ASSOC、类上的泛化层次结构以及函数关联、角色和多重性,这些函数关联、角色和多重性分别为每个关联作为ASSOC给出其专用类、其角色名称和多重性。在本文的剩余部分中,对象模型的特定实例化称为系统。一个系统随着时间的推移而处于不同的状态对象(的数量)、它们的属性值和其它特性在系统执行在OCL 2.0提案中,系统状态σ(M)=CLASS,ATT,ASSOC在形式上被定义为一个三元组,由当前存在的对象的集合CLASS、对象的属性值的集合ATT和连接对象的当前建立的链接的集合ASSOC组成然而,OCL 2.0提案中提供的形式语义并不完整,因为不可能使用系统状态给出的信息来推理当前激活的Statechart状态或已发送的消息因此,不可能为状态相关操作和OCL消息上的操作提供正式的语义。在我们的工作中,我们专注于完成基于对象模型的形式化语义。在上一篇文章中,我们已经通过状态配置的概念将Statecharts集成到OCL中,并为状态相关操作oclInState(状态名:OclState)提供了形式化的语义[5]。本文现在进一步扩展了这项工作,并将重点放在OCL消息的形式化上。本文其余部分的结构如下。在第2节中,我们简要地解释了OCL消息的概念。第3节通过提供额外的组件来捕获OCL消息,扩展了对象模型的形式定义。第4节然后通过引入OCL消息相关操作符的解释函数提供了相应的语义,运营 第5节结束本文。S.弗莱克,W. Mueller / Electronic Notes in Theoretical Computer Science 102(2004)792OCL消息OCL消息的概念是在OCL 2.0提案中新引入的,用于指定对对象发送的消息的行为约束。它是基于[7,8]中提出的工作。基本上,OCL消息指的是发送的信号或调用的(同步或异步)操作虽然发送的信号本质上是异步的,调用对象只是继续执行,但同步操作调用使调用操作等待返回值。相反,异步操作调用就像发送一个信号,这样潜在的返回值就被简单地丢弃了。关于消息传递动作的更多细节,参见UML 1.5的动作语义[9,第2.24节]。注意,UML动作语义也定义了广播信号动作,而相应的OCL消息还没有定义。OCL消息的概念使建模者能够指定后置条件,这些后置条件要求特定的信号必须已经发送,操作必须已经调用,或者操作必须已经完全执行并返回。2.1语法预定义的参数化类型OclMessage(T)现在是OCL标准库中OCL类型系统 的 一 部 分 , 其 中 模 板 参 数 T 表 示 操 作 或 信 号 。 因 此 , 具 体 的OclMessage类型分别由(a)所引用的操作或信号和(b)所引用的操作的所有形式参数或所引用的信号的所有属性来描述。OclMessage(T)类型定义的操作如图1所示。注意,只允许在操作后置条件中获取和使用OCL消息。OCL消息由附加到目标对象的消息操作符^^获得。例如,OCL表达式targetObj^^setValue(17)产生已发送到在执行所考虑的操作期间由targetObj确定的对象-回想一下,所考虑的表达式必须在操作后置条件。结果序列的每个元素都是OclMessage(T)类型的实例。例如,OCL表达式targetObj^^setValue(17)的类型是Sequence(OclMessage(setValue(i:String)。人们可以利用所谓的未指定值来表示实际参数不需要具有指定值。未指定的值用问号表示,例如,targetObj^^setValue(?:)。参数类型可以在OCL消息表达式中省略,但请注意,80S.弗莱克,W. Mueller / Electronic Notes in Theoretical Computer Science 102(2004)1:hasReturned():Boolean2:--如果模板参数表示操作3:--并且调用的操作已经返回,则第四章:5:result():被调用操作的返回类型>>6:--返回调用的操作的结果,如果模板7:--参数表示操作,调用的操作8、已经回来了。否则返回OclUndefined。九:10:isSignalSent():Boolean11:--如果模板参数表示信号,则返回true。十二:13:isOperationCall():Boolean14:--如果模板参数表示15:--操作调用,则返回true。Fig. 1. OCL消息当使用不同的参数类型多次指定操作时,它们可能是必要的,要检查消息是否已发送,可以使用hasSent运算符^,例如,如果在所考虑的操作的执行期间消息setValue(17)已经被发送到targetObj,则表达式targetObj_setValue(17)导致真。更多示例见[6,第2.7.3节]。2.2语义OCL消息的语义目前仅在基于元模型的语义中定义[6,5.2节在此上下文中,表示语义域的所谓Values包具有用于本地快照的类。本地快照是语义域的一个元素,它存储以后引用所需的值。本地快照被保持为允许访问对象的值的历史的有序列表,例如,在操作执行开始时设置属性值。特别地,本地快照跟踪对象在操作执行期间发送的消息序列和对象接收的消息序列OCL消息的正式语义尚未定义,即,OCL的两种语义目前是不一致的。为了克服这一缺陷,我们在下一节中扩展了对象模型的形式化方法2.3例如作为一个应用示例,我们回顾了OCL 2.0提案中的一个后置条件[6,第2.7.2节]:context Person::giveSalary(amount: 1)S.弗莱克,W. Mueller / Electronic Notes in Theoretical Computer Science 102(2004)81post:letmessage: OclMessage = company^getMoney(amount)inmessage.hasReturned()--getMoney被发送并返回,message.result()=true--getMoney调用返回true不幸的是,这个后置条件没有完全正确地指定;表达式公司^getMoney(amount)没有返回OCL消息,而是返回一个布尔值,因为应用了hasSent运算符。 相反,必须使用消息运算符^^来提取发送的相应消息context Person::giveSalary(amount: 1)post:letmessages: Sequence(OclMessage)= company^^getMoney(amount)in消息->forAll(msg:OclMessage| msg.hasReturned())和消息->forAll(msg:OclMessage|msg.result()= true)请注意,我们现在必须推理一系列OCL消息。 上面的后置条件要求所有发送给对象company的消息getMoney(amount)都已经返回了结果值true。如果我们想限制消息getMoney(amount)只发送一次,我们必须添加一个附加条件,如下所示:context Person::giveSalary(amount: 1)post:letmessages: Sequence(OclMessage)= company^^getMoney(amount)inmessages->size()= 1-- getMoney被发送一次,messages->first().hasReturned()--getMoney返回,messages->first().result()=true--调用返回true3扩展对象模型在OCL 2.0提案中,对象模型的正式定义目前缺乏Statechart状态和OCL消息的组件,因此我们定义了对象模型的扩展,称为扩展对象模型。特别是,必须新引入以下概念:• 具有相应格式良好性规则的类的信号接收• 状态图及其与活跃类的关联,• 对国家配置的正式定义,以及• 类的形式描述符的扩展此外,必须将以下信息添加到系统状态中,以便能够评估使用状态相关和OCL消息相关操作的OCL表达式:82S.弗莱克,W. Mueller / Electronic Notes in Theoretical Computer Science 102(2004)def。∈∈=• 所有当前存在的活动对象的状态配置,• 当前执行的操作,以及• 对于每个当前执行的操作,到目前为止发送的所有消息。3.1小节解释了扩展对象模型的语法元素在3.2小节中,我们提出了系统状态的扩展版本。这个扩展使我们能够给消息相关的操作一个语义,到目前为止还没有正式定义。3.1语法在本文的其余部分,设A是一个字母表,N是A+上的一组名称,T是一组类型。特别地,T=TBTETCTS包括• 一组基本标准库类型TB,即,布尔、实数、布尔和弦,• 一组用户定义的枚举类型,• 用户定义类的集合TC,c∈CLASS,以及def• 一组特殊类型TS={OclV oid,OclState,OclAny}。我们将类型t表示的值集ITYPE(t)(或在上下文清楚时简称为I(t))称为类型域。为方便起见,我们假设OclUndefined(在下文中由符号“”表示)包含在每个类型域,例如,I(OclV oid)={0},I(OclAny)=t∈TB<$TE<$TCI(t){}。此外,设c CLASS为类,tc TC为类C.2每个类c与描述其对象的特性的属性的集合ATTc 一个属性有一个名称a∈ N和一个类型t∈T,指定属性值的域。类c也与操作的集合OPc和信号的集合SIGc相关联(在UML中,由类处理的信号由所谓的接收指定[9,第3.26.6节])。我们通过元组定义扩展对象模型Mdef。CLASS,ATT,OP,paramKind,isQuery,SIG,SC,ASSOC,工作人员,员工,角色,多重性2每个类c∈CLASS都导出一个对象类型tc∈T,它与类同名。c和tc之间的区别在于,对于所有的c∈CLASS,我们有特殊的值f ∈I(tc)。S.弗莱克,W. Mueller / Electronic Notes in Theoretical Computer Science 102(2004)83c∈CLASS×→× × → {}C =CCCC=ATTc• 一组状态图SC,SC=c∈ACT IVESCc,cJ∈parents(c)与• 主动和被动类别的集合CLASS=ACTIVE ASSIV E• 属性的集合ATT,ATT=ATTc,• 一组运算OP,OP=c∈CLASSOPc,• a函数paramKind:CLASSOPNin、inout、out为每个操作参数给 出 其参数种类(参见[9,第2.5.2.31节]),• - 函数isQuery:CLASS OP Boolean,其确定操作是否是没有副作用的查询操作(参见[9,第2.5.2.7节]),• 信号的集合SIG,SIG_c∈CLASSSIG_c,• 类之间的关联的集合ASSOC• 类的泛化层次结构和信号的泛化层次结构,以及• 函数关联、角色和多重性,分别定义ASSOC中每个元素到参与类、其相应角色名称和多重性注意,我们在这里不进一步描述扩展对象模型的元组组件。有关集合CLASS、ATT、OP和ASSOC的更多详细信息,请参考相应的来源[6,10]。我们还省略了信号和状态图的正式语法定义,并参考[5]了解更多细节。在类中定义的特征集及其继承的特征被称为类的完整描述符。更正式地说,类c∈CLASS的完整描述符是一个元组FD定义ATT,OP,SIG,SC,navEnds(c)包含属性、操作、信号、可导航角色名称的完整集合,以及(在活动类的情况下)关联的状态图。例如,类c的完整属性集定义为:Escherdef其中,parents(c)表示c的(传递的)超类的集合。相应地定义了操作、信号和n个角色名称的完整集合OPc、SIGc和navEnds(c)ATTcATTcJ,84S.弗莱克,W. Mueller / Electronic Notes in Theoretical Computer Science 102(2004)∈∈=Σ∈3.2系统状态类c CLASS的定义域是该类及其所有子类的对象的集合。对象由在整个系统上下文中唯一的对象标识符引用。类C的对象标识符的集合类是由一个无限def集合oid(c)定义为={ob jId1,objId2, . 。 。}。一个类c∈CLASS的整环是我CLASSdef(c)=cJ∈CLASSwithcJ <$c<$cJ=coid(cJ).出于技术目的,我们还定义了I类def=c∈CLASS oid(c).当扩展对象模型的特定实例化(即,系统,tem)执行时,实例化对象的数量、它们的属性值、状态图配置和其他特征将随时间而变化。如前所述,当前只有三个组件的系统状态的概念不足以评估使用状态相关操作和OCL消息的OCL表达式。此外,我们需要有关当前激活状态、已调用和发送信号的操作、当前执行的操作等的信息。在这种情况下,我们采用[11]的思想来形式化当前执行的操作,并定义函数来捕获所需的附加信息。形式上,扩展对象模型M的系统状态是元组σ(M)def.Σ类,ZeroATT,中国 ,CONF,当前操作,当前操作参数,发送消息,发送消息参数。在本小节的其余部分,我们将更详细地解释系统状态的组成部分,但请注意,在[6,10]中已经定义了类,类ATT和类ASSOC(1) 联系我们def=c∈CLASS 初级班,c。有限集合类别c包含所有存在于系统状态中的类c∈CLASS的对象,即,CLASS,c此外,我们相应地为主动类定义了集合EACTIVE ,c,为被动类定义了集合EPASSIVE,c请注意,我们使用附加的下划线来强调我们引用当前存在的对象的事实。S.弗莱克,W. Mueller / Electronic Notes in Theoretical Computer Science 102(2004)85∈ ID--⟩⟨这种区分有助于第4节中OCL消息语义的定义。(2) 当前属性值保存在set_attribute_attribute 中。 它是函 数σA T T , a :<$CLASS,c→I(t)的并集,其中a∈A T Tc<$且t是对a指定的typ。每个函数σ ATT,a为给定类c ∈ CLASS的每个对象的某个属性赋值。(3) ΣAssocdef=作为∈ASSOCASSOC,作为包括有限集合,如的包含连接对象的链接我们将以[10]为例,详细说明。关于链接的信息,即,IASSOC(as)的元素,以及多重性规范的形式化。(4) 当前的状态图配置由σCONFdef=c∈ACTIVE。σCONF,c第四章E,c→ISC (c)- 是的每个函数σCONF,c为给定类c∈ACTIV E的每个对象分配一个包含所有激活(子)状态的完整状态配置。集合ISC(c)表示与活动类c相关联的状态图SCc的可能状态配置。在[5]中可以找到状态配置的正式定义。必须考虑其他运行时信息,来计算访问OCL消息的表达式。这主要涉及当前执行的操作以及发送的信号和消息的历史。这与OCL 2.0的基于元模型的语义中定义的本地快照有关[6,Section 5.2]。3.2.1目前执行的操作设ID为无限可积集,例如,ID=N,并让OpStatusdef=执行,返回。 在操作执行的起始点,唯一标识符opId与当前操作执行相关联。因此,一个操作的执行可以通过一个给定的对象objId∈OPCLASS , c ,一个操作签名op∈OPc,以及一个操作标识符opId∈ ID来唯一地标识。当前执行的操作集定义为:电流Opdef=。 σ电流Op,c:高级,c ×OPc→c∈CLASSP(I CLASS×OP× ID × ID ×OpStatus)每个函数σcurrentOp,c给出一组形式为sourceId、sourceOp、sourceOpId、opId、status的元组,其唯一地标识给定对象和操作名称的所有当前执行的元素sourceId、sourceOp、86S.弗莱克,W. Mueller / Electronic Notes in Theoretical Computer Science 102(2004)∈def--∈第1页,...,val n,returnV aln,if返回srcId,srcOp,srcOpId,opId,执行∈和sourceOpId是指最初调用具有标识符opId的所考虑的操作op的操作执行。这些元素对于在操作执行终止后返回潜在结果值的引用是必需的。我们要求关联的操作标识符opId在该操作的执行终止之前不能更改标记状态OpStatus指示操作扩展的当前状态。与UML 1.5中指定的消息传 递 动 作 相 比 , 我 们 在 这 里 省 略 了 状 态 ready 和 complete[9 , Section2.19.2.3],因为它们在OCL的上下文中是不必要的。已执行操作的实际参数值保存在currentOpParam中。当前OpP aramdef=。σcurrentOpParam,c:高级,c ×OPc× IDc∈CLASS对于所有的t∈T,我们定义I?(t→我?(t1)×. ×I?(t n)× I?(t )I(t){?}。 象征?表示未分配)=的值的状态此符号不得与未定义值混淆表示,也不同于字符串文字'?' 。函数σcurrentOpParam,c给出给定对象、操作签名和操作执行标识符的当前 执 行 操 作 的 实 际 参 数 值 。 对 于 每 个 c∈CLASS , 我 们 定 义 σcurrentOpParam,c如下,其中op=(ω:t c×t1×. ×tn→t)∈OPc:σcurrentOpParam,c(objId,op,opId)›→∈σcurrentOp,c(objId,op)返回srcId,srcOp,srcOpId,opId,返回currentOp,c(objId,op)否则,我会的。在上面的定义中,val i∈I?(t i)表示定义为类型t i∈T,1≤i≤n。 对于paramKind(c,op,i)∈in,inout的位置i处的参数,对应的值vali由操作调用预先确定。paramKind(c,op,i)=out的参数携带未赋值的值?直到操作执行结束。 返回值returnV al我?(t)也保持未分配状态,直到操作终止。我们要求所有的参数值在操作终止之前都不改变当操作执行状态从执行变为返回时,类型inout和out参数以及返回值returnV al⎧⎨⎪S.弗莱克,W. Mueller / Electronic Notes in Theoretical Computer Science 102(2004)87⊥/⟨ ⟩ ∈ID P × X ID更新并获得值=?。3如果操作没有返回结果,则操作op的结果类型t为OclV oid。在这种情况下,当操作终止时,我们设置returnV al=。请注意,这些更新只对同步操作调用有影响,因为根据UML规范,异步操作调用的结果值将被丢弃。3.2.2发送的消息为了能够计算使用消息操作符^^的OCL表达式,我们必须存储为每个执行的操作发送的消息的历史 为对于每个对象objId∈OSCLASS,c和它当前执行的每个操作op,我们定义一个函数σsentMsg,c(objId,op,opId),它给出了与它们对应的目标对象一起发送的消息集当一个消息从一个具有标识符opId的操作op的执行发送到一个具有标识符targetId的目标对象时,该目标对象必须实际存在(否则我们无法引用它),但是当操作op的执行终止时,它可能已经被销毁了。这就是为什么我们不能使用集合RISKCLASS作为目标对象的基本集合,因为该集合只保留当前存在的对象。相反,函数σsentMsg,c的签名必须使用目标对象标识符的一般集合ICLASS。我们将传递的信息定义为联系我们def=。 σsentMsg,c:高级,c ×OPc× ID →c∈CLASSP(I类×(SIG类OP)× ID)集合在值集中,(I级)(SIGOP)) 用 于 在为同步操作调用返回值时引用正确的消息标识符。在源对象的上下文中具有唯一的标识符就足够了,例如,命名为IDsourceId,但为了简洁起见,我们在这里简单地重用setID。元素targetId,msg,callId σsentMsg,c(objId,op,opId)表示具有签名msg和调用标识符callId的消息已经从对象objId发送到具有标识符targetId的对象,作为具有签名op和标识符opId的操作执行的一部分。我们只需要保留在相应的调用操作执行期间发送的消息的信息。在手术执行前后,3请注意,此类更新的规则是动态语义的一部分。 我们在这里必须假设更新正确执行,并具有所需的效果。88S.弗莱克,W. Mueller / Electronic Notes in Theoretical Computer Science 102(2004)- 是的ΣΣ≤≤⎧⎪⎨∈删除targetId,msg,callId,如果删除srcId,srcOp,srcOpId,opId,执行/∈我们简单地设置σ sentMsg,c(objId,op,opId)= σ。 更正式地说,我们有σsentMsg,c(objId,op,opId)›→∈σcurrentOp,c(objId,op)返回srcId,srcOp,srcOpId,opId,返回currentOp,c(objId,op)否则,我会的。此外,我们必须存储每条消息的实际参数值def发送.因此,我们定义:c∈CLASSσsentMsgParam,c:C类,c×OPcC类× ID ×I类×(SIGC类)× ID→我?(t1)×. ×I?(t n)× I?(t)。数量n和类型ti,1i n由相应消息签名的形式参数确定,即,信号sig=(ω:tc×t1×. . 。 xtn)∈SIG_c或一个运算算子=(ω:tc×t1×. 。 ×tn→t)∈OPc.每个函数σsentMsgParam,c定义为:σsentMsgParam,c(objId,op,opId,targetId,msg,callId)›→第1,...,val n,returnV aln,if返回targetId,msg,callId返回σsentMsg,c(objId,op,opId)否则,我会的。价值观 是什么?(ti)记录所发送消息的参数值。我们设置所有的kindout参数,返回变量returnV al为?默认情况下,即,这些参数值保持不被分配直到它们被计算。基本上,它们只与同步操作调用相关,其中值=?在被调用操作终止后分配同样,请注意,对于异步操作调用,潜在的结果无论如何都会被丢弃对于发送的信号,返回类型t的域被设置为I?(OclV oid),返回值保持未赋值。。⎨⎪S.弗莱克,W. Mueller / Electronic Notes in Theoretical Computer Science 102(2004)89帮助集和函数。在本文的剩余部分,我们需要一些帮助集和函数。这些基本上分别是ΣsentMsg 和ΣsentMsgParam 的子集以及σsentMsg , c和σsentMsgParam , c的子函数。由于它们的正式定义是直接的,为了简洁起见,我们在这里省略了它们在操作执行期间发送的信号被保存在set_configessentSig中。在这个集合中,函数σsentSig,c返回发送信号的历史。实际的参数值保存在具有函数σsentSigParam,c的集合ΣsentSigParam中。被调用的操作保存在set_called_Op中。我们使用函数σcalledOp,c返回调用的操作历史。Set_calledOpP_aram 保存被调用操作的实际参数值,函数σcalledOpP_aram,c用于访问被调用操作的实际参数值为了进一步区分同步和异步操作调用,使用了集合“synchronedSynchOp”和“synchronedAsynchOp” 。 在 每 个 集 合 中 , 我 们 有 函 数 σcalledSynchOp , c 和σcalledAsynchOp,c,它们返回给定操作执行的调用同步和异步操作的历史。实际参数值保存在集合中,称为SynchOpP aram和AsynchOpP aram, 并由函数σ访问,称为SynchOpP aram,c和σ称为AsynchOpP aram,c。我们现在有了所有必要的组件,可以计算一般的OCL表达式,即,还有那些访问OCL消息的4OCL消息首先,我们正式定义OclMessage类型的域,I(OclMessagedef)=的c∈CLASS,op∈OPcI(OclMessage(op))c∈CLASS,sig∈SIG其中,对于给定操作op=(ω:tc×t1 ×t 1),集合I(OclMessage(op))... xtn→t)∈OPc定义如下:I(OclMessage(op))= ID × I CLASS× I(t1)×.x I(t n).SetID是指发送消息的唯一调用标识符(callId)。SetICLASS用于保存消息发送到的目标对象的对象标识符。对于信号sig=(ω:tc×t1×. . 。 ×tn)∈SI Gc非常相似,即,I(OclMessage(sig))= ID × I CLASS× I(t1)×.90S.弗莱克,W. Mueller / Electronic Notes in Theoretical Computer Science 102(2004)x I(t n).S.弗莱克,W. Mueller / Electronic Notes in Theoretical Computer Science 102(2004)91∈ ∪ ∪∪我们现在可以给出后置条件表达式的语法了。OCL消息操作符和下一小节中的相应语义。OCL消息上的操作语义在4.2小节中给出。4.1OCL消息运算符我们在这里关注更通用的消息操作符^^的形式化,因为hasSent操作符^可以很容易地导出如下。给定一个目标对象表达式targetExpr和一个OCL消息声明msg(msgArgs),我们可以用以下表达式替换OCL表达式targetExpr^msg(msgArgs):targetExpr^^msg(msgArgs)->size()> 0。请 注 意 , 这 个 标 识 在 OCL 2.0 中 没 有 得 到 正 确 的 处 理 , 因 为OclMessageExpCS的定义是发送到目标对象的消息数正好是= 1(而不是>0)[6,4.3节语法. OCL表达式的基本语法元素由所谓的数据签名定义,其中• TM是类型t的类型表达式TExpr(t[6,第A.2.5节],• ≤是TM上的类型层次[6,Section A.2.7],并且•M是操作签名的集合,然后归纳定义一般有效的OCL表达式的形式语法,以便从简单的表达式递归构建更复杂的表达式OCL表达式的语法由以下集合defExpr =t∈TM快递和一个额外的函数来捕获自由变量。有效OCL后置条件表达式的集合Post-Expr的定义方式与Expr相同,但有额外的规则允许操作oclIsN ew(),operator @pre和一个名为result的预定义结果变量[6,SectionA.3.2.2]。此外,以下规则VIII。介绍了一种新的后置条件表达式w.r.t.OCL消息。注意这里我们还必须考虑消息表达式的信号。因此,我们使用集合M来指代在对象模型M的实例化中定义的信号集合。92S.弗莱克,W. Mueller / Electronic Notes in Theoretical Computer Science 102(2004)∈→∈、。∨∃msg=(ω:tcJ×t1×. . 。×tn)∈SIG<$cJ、八. 如果(a)e目标∈Post-Exprt,并且(b) 或者(ω:t c×t1×. ×tn→t)∈ <$M或(ω:tc×t1×. ×tn)∈M,以及(c) e i∈ Post-Exprtifor alli ∈ {1,.,n},则e目标(e1,.,e n)∈Post-Exprt以及目标εω(ε1,., e n)表达后。这在OCL 2.0提案的抽象语法中映射到OclMessageExp语义一般来说,表达式的语义是在给定环境τ=σ(M),β的上下文中定义的,环境具有系统状态σ(M)和变量赋值β:V ar t I(t)。变量赋值β将变量名映射到值[6,第A.3.1.1节]。在下文中,设Env是环境τ=βσ(M),βσ的集合。虽然OCL表达式e的语义通常由函数I[[e]]:Env→I(t)定义,但在操作后置条件的情况下,我们必须考虑两种环境环境τpre(在操作执行开始时)和τpost(在终止时)。因此,在后置条件中指定的表达式e的解释函数变成I[[e]]:Env×Env→I(t)。现在,我们在给定对象objId∈NCLASS,c和已执行对象的上下文中定义环境(τpre,τpost使用签名op OPc和标识符opId的操作(隐式地,我们假设操作执行刚刚终止)。首先,我们定义一个帮助集MSG etargetω(e1,.,en)保持发送的所有相关消息。MSGe目标值ω(e1,.,en)def=VcallId,eV al目标,v1,.,v n|cJ∈CLASS:eV altarget=I[[etarget]](τpre,τpost)∈ICLASS(cJ)\{n}{1,., n}:eV al i= I [[e i]](τ pre,τ post)∈ I?(ti)\{laugh}{1,.,n}:(eV al i=? ⇒ eV ali=vi)∧∃msg=(ω:tcJ×t1×. . 。×tn→t)∈OPc目标,msg,callId<$∈σsentMsg,c(objId,op,opId)你知道吗?(OclAny):1,...,v n,anyV aln ∈σ sentMsgParam,c(objId,op,opId,eV al target,msg,callId).,使得S.弗莱克,W. Mueller / Electronic Notes in Theoretical Computer Science 102(2004)93∈def≤ ≤⊥∈⊥1n非正式地说,这些元素被称为Id,eV al target,v1,.,该集合的V n确定如下。目标对象标识eV al目标是从e目标中评估的,并且必须在它与eV不同的意义上进行良好定义。类似地,参数表达式e i的所有求值eV al i必须被良好地定义。出于一致性原因,那些eV都被评估为实际值(即,的值/=?)必须等于vi。此外,必须有一个消息签名msg,这样三元组可选的target,msg,callId表示在所考虑的操作执行内从对象objId最后,值vi必须等于为所发送的调查消息存储(并可能更新)的实际参数值。变量anyV al只是出于技术原因引入的,以允许返回值的任意值在下文中,令m为MSG e target中的元素的数目, en)。对于每个i∈{1,.,m},令xi=VcallId i,eV al target,v1,i,.,v n,i是集合MSGet rgt∈ω(e1,...,en),其中对于
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 4
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 收起
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
会员权益专享
最新资源
- zigbee-cluster-library-specification
- JSBSim Reference Manual
- c++校园超市商品信息管理系统课程设计说明书(含源代码) (2).pdf
- 建筑供配电系统相关课件.pptx
- 企业管理规章制度及管理模式.doc
- vb打开摄像头.doc
- 云计算-可信计算中认证协议改进方案.pdf
- [详细完整版]单片机编程4.ppt
- c语言常用算法.pdf
- c++经典程序代码大全.pdf
- 单片机数字时钟资料.doc
- 11项目管理前沿1.0.pptx
- 基于ssm的“魅力”繁峙宣传网站的设计与实现论文.doc
- 智慧交通综合解决方案.pptx
- 建筑防潮设计-PowerPointPresentati.pptx
- SPC统计过程控制程序.pptx
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功