（计算机应用技术专业论文）uml状态机的形式化语义研究.pdf

状态机的形式化语义研究 学科专业：计算机应用技术 指导教师：张为群教授 内容摘要 研究方向：软件工程 研究生：陈武( 2 0 0 1 3 6 8 ) u m l ( u n i f i e d m o d e l i n g l a n g u a g e ) 作为事实上的面向对象建模标准语言， 它的复杂性和庞大性是不可避免的，但是它也包括了大量的具有模糊、稀疏语义 的标准元素。在u m l 规范中，编制者是用较为形式化的语言o c l ( o b j e c t c o n s t r a i n tl a n g u a g e ) 和自然语言两种手段描述静态语义，而动态语义却基本 上完全是用自然语言来描述的，u m l 缺乏一个严格的动态语义定义。因此，对 u m l 进行形式语义研究，对增进该语言的清晰性、等价性和一致性、可扩展性 是十分有帮助的，为模型的正确性证明、转换以及支持u m l 建模工具的一致性 检查提供了有力的理论工具。 目前。很多机构和个人都在从事u m l 的形式语义研究，他们试图通过对 u m l 的研究来对u m l 的未来产生影响。这些机构和个人所采用的方法主要是 补充法和具有面向对象扩展的形式语言方法。这两种方法各具有优点。但是也存 在不足。在补充法中所使用的形式化语言不具有面向对象的特征，不能很好地和 当前实践相结合，而具有面向对象扩展的形式语言方法又不能直接对u m l 模型 的语义进行形式化，影响了读者对u m l 模型形式化的理解。 针对以上不足，作者将上述两种方法结合起来，提出了一种新的形式化状态 机语义的方法，即首先对u m l 状态机的元模型的语法结构进行：分析，然后通过 具有面向对象特征的r a i s e ( r i g o r o u sa p p r o a c h t oi n d u s t r ys o f t w a r e e n g i n e e r i n g ) 的说明语言r s l ( r a i s es p e c i f i c a t i o nl a n g u a g e ) ：直接对u m l 状 态机的操作语义进行形式化。其中在对语法结构分析这一部分中，作者通过提出 一个状态层次结构对u m l 状态机的各种状态及其间的相互关系进行分析，然后 依次对事什、转换的结构进行分析，最后对u m l 状态机的语法结构进行了总结 性形式化描述。在对u m l 状态机的“运行到完成”这一基本操作的语义进行形 u m l 状态机的形式化语义研究 式化中作者运用r s l 语言，依次对转换的成立、转换的冲突、冲突的解决、 转换的选择的沿义进行了形式化描述，并最终提出一个u m l 状态机“运行到完 成”操作的算法。通过上述这两部分的结合，从而提出了个完整的u m l 状态 机语义形式化的新方法。 最后，作者通过一个实例说明u m l 状态机语义的形式化描述可以证明那些 用u m l 描述的系统的一些重要属性是正确的。 关键词：形式化语义u m l 状态机r s l u m l 状态机的形式化语义研究 t h ef o r m a ls e m a n t i cs t u d yo fu m l s t a t em a c h i n e a b s t r a c t ：a sad e f a c t o o b j e c t o r i e n t e dm o d e l i n g s t a n d a r d l a n g u a g e ，t h e c o m p l e x i t y a n d m a g n i t u d e o fu m l ( u n i f i e dm o d e l i n gl a n g u a g e ) i si n e v i t a b l e h o w e v e r ，i ta l s oc o n t a i n sal o to f s t a n d a r de l e m e n t sw i t hv a g u ea n ds p a r s es e m a n t i c s i nt h eu m l s p e c i f i c a t i o n ，t h ee d i t o r sd e s c r i b et h es t a t i cs e m a n t i c si nf o r m a ll a n g u a g e o c l ( o b j e c t c o n s t r a i n t l a n g u a g e ) a n d n a t u r a l l a n g u a g e ，w h i l e t h e d y n a m i c s e m a n t i c si sa l m o s td e s c r i b e di nn a t u r a ll a n g u a g e u m ll a c k si nas t r i c td e f i n i t i o no f d y n a m i cs e m a n t i c s t h e r e f o r e ，t h ef o r m a ls e m a n t i cs t u d yo f u m i ，i sh e l p f u lf o rt h e i m p r o v e m e n to ft h ec l a r i f i c a t i o n ，e q u i v a l e n c e ，c o n s i s t e n c y , a n de x t e n d i b i l i t yo f t h e l a n g u a g e ，t h u so f f e r sap o w e r f u lt h e o r e t i c a lt o o lf o rt h ev a l i d i t yl ；) r o o f , t r a n s i t i o no f t h em o d e la n dt h ec o n s i s t e n c yc h e c ko f t h em o d e l i n gt o o l ss u p p o r t i n gu m l a t p r e s e n t ，m a n yo r g a n i z a t i o n sa n d i n d i v i d u a l sa r ee n g a g e di nt h es t u d yo fu m l f o r m a ls e m a n t i c s t h e ya t t e m p tt oi n f l u e n c et h ef u t u r eo fu m l t t l 】：o u g h t h es t u d yo f u m l t h em e t h o d sw h i c ht h e s e o r g a n i z a t i o n s a n di n d i v i d u a l su s ea r e m a i n l y s u p p l e m e n t a la p p r o a c ha n d0 0 - e x t e n d e df o r m a ll a n g u a g ea p p r o a c h b o t ho ft h e a p p r o a c h e s h a v et h e i ro w n a d v a n t a g e s a n d d i s a d v a n t a g e s b e c a u s e t h ef o r m a l l a n g u a g e i n s u p p l e m e n t a la p p r o a c hd o n t h a v et h eo b j e c t o r i e n t e d f e a t u r e ，u s i n g s u p p l e m e n t a la p p r o a c hm a k e s i td i f f i c u l tt oi n t e g r a t ew i t ht h ep r e s e n tp r a c t i c e w h i l e t h ew a yo fo o e x t e n d e df o r m a l 1 a n g u a g e a p p r o a c hc a l l td i r e c t l y f o r m a l i z et h e s e m a n t i c so fu m l m o d e l ，w h i c ha f f e c t st h er e a d e r s u n d e r s t a n d i n go fu m lm o d e l t b r m a l i z a t i o n b a s e do nt h o s ed i s a d v a n t a g e s ，t h ea u t h o rc o m b i n e st h et w om e t h o d sa n dp u t s f o r w a r dan e ww a yo ff o r m a ls t a t em a c h i n es e m a n t i c s t h a ti s ，f i r s t l y , a n a l y z et h e g r a m m a rs t r u c t u r eo ft h em e t a m o d e io fu m l s t a t em a c h i n e 。t h e nt h r o u g hr a i s e ( r i g o r o u sa p p r o a c ht oi n d u s t r ys o f t w a r ee n g i n e e r i n g ) w h i c hh a so b j e c t o r i e n t e d f e a t u r e sd i r e c t l yf o r m a l i z et h eo p e r a t i n gs e m a n t i c so fu m ls t a t em a c h i n e i nt h ep a r t o f g r a m m a rs t r u c t u r ea n a l y s i s ，t h ea u t h o rp u t sf o r w a r das t a t eh i e r a r c h i c a ls t r u c t u r e w h i c ha n a l y z e sa l lt h es t a t e so fu m ls t a t em a c h i n ea n dt h er e l a t i o n s h i pb e t w e e nt h e m u m l 状态机的形式化语义研究 a n dt h e na n a l y z et h es t r u c t u r eo ft h ee v e n t sa n dt r a n s i t i o n si nt l l r ：aa n df i n a l l yg e ta s u m m a r i z i n gf o r m a ld e s c r i p t i o no f t h eg r a m m a rs t r u c t u r eo fu m i _ ，s t a t em a c h i n e i n t h es e m a n t i cf o r m a l i z a t i o no fr u nt oc o m p l e t i o ns t e p ，u s i n gr s l ，t h ea u t h o ri nt u r n f o r m a l i z e ss e m a n t i c so ft h ee n a b l e dt r a n s i t i o n s ，c o n f l i c t so ft r a n s i t i o n s ，s o l u t i o no f c o n f l i c t s ，a n dt h es e l e c t i o no ft r a n s i t i o n s ，a n df i n a l l yp u t sf o r w a r daa l g o r i t h mo ft h e r u nt oc o m p l e t i o ns t e pi nu m l s t a t em a c h i n e c o m b i n i n gt h o s et w o p a r t s ，t h ea u t h o r p u t sf o r w a r dan e wc o m p l e t ef o r m a lm e t h o do f t h es e m a n t i c so f u m ls t a t em a c h i n e a tl a s t ，t h ea u t h o ru s e sa ne x a m p l et os h o wt h a tu s i n gt h ef o r m a ld e s c r i p t i o no f u m ls t a t em a c h i n es e m a n t i c sc a n j u s t i f yt h ei m p o r t a n tp r o p e r t i e so ft h o s es y s t e m s d e s c r i b e db yu m l k e y w o r d s ：f o r m a l i z e s e m a n t i c su m ls t a t em a c h i n er s l u m l 状态机的形式化语义研究 第一章前言 l 、背景 自从上个世纪4 0 年代第一台计算机问世以来，信息技术的变化日新月异， 已经深入到千家万户。随着计算机硬件性能的不断提高和价格的不断下降，其应 用领域也在不断扩大。人们在越来越多的领域希望把更多、更难的问题交给计算 机去解决。这使得计算机软件的规模和复杂性与日俱增，从而使软件技术不断地 受到新的挑战。上世纪6 0 年代软件危机的出现就是因为系统的复杂性超出了人 们在当时的技术条件下所能驾驭的程度。此后在软件领域，人们一直在为寻求更 先进的软件方法与技术而奋斗。 开发一个具有一定规模和复杂性的软件系统和编写一个简单的程序大不一 样。大型的、复杂的软件系统的_ 丌发是一项工程，必须按工程学的方法组织软件 的生产与管理，必须经过分析、设计、实现、测试、维护等一系列的软件生命周 期阶段。这是人们从软件危机中获得的最重要的教益。这一认识促使了软件工程 学的诞生。编程仍然是重要的但是更具有决定意义的是系统建模。只有在分析 与设计阶段建立了良好的系统模型，才有可能保证工程的正确实施。正是由于这 一原因，许多在编程领域首先出现的新方法和新技术，总是很快地被拓展到软件 生命周期的分析与设计阶段。 面向对象方法正是经历了这样的发展过程。继s m a l l t a l k 8 0 之后，2 0 世纪8 0 年代又有一大批面向对象的编程语言问世，标志着面向对象方法走向成熟和实 用。此时，面向对象方法开始向系统设计阶段延伸，出现了诸如b o o c h 8 6 、g o o d ( 通用面向对象的开发) 、h o o d ( 层次式面向对象的设计) 、o o s d ( 面向对象 的结构设计) 等一批o o d ( “面向对象的设计”或“面向对象的开发”的缩写) 方法。至1 9 8 9 年以后，面向对象方法的研究重点开始转向生命周期的分析阶段， 将o o a ( 面向对象的分析) 与o o d 密切地联系在一起，出现了一大批面向对象 的分析与设计( o o a & d ) 方法，如b o o e h 方法、c o a d y y o u r d o n 方法、j a c o b s o i i 的o o s e 、r u m b a u g h 等人的o m t 、s h l a e r m e l l o r 方法等等。 各种面向对象的分析与设计方法都为面向对象理论与技术的发展做出了贡 献。这些方法各有自己的优点和缺点，同时在各自不同范围内拥二茸自己的用户群。 各种方法的主导思想以及所采用的主要概念与原则大体上是一致的，但也存在一 u m l 状态机的形式化语义研究 些差异。这些差异带来的问题是，不利于面向对象向一致的方向发展，也会给用 户的选择带来一些困惑。将各种方法统一起来的呼声越来越高，1 9 9 5 年，r a t i o n a l 公司的g b o o c h 和j r u m b a u g h 决定将他们各自的方法结合起来成为一种方 法，称作“统一方法”( u n i f i e dm e t h o d0 8 ) 。此时，o o s e 的作者i j a c o b s o n 也 加入r a t i o n a l 公司，于是他也加入统一行动。于1 9 9 6 年6 月发布了u m l 0 9 。 鉴于统一行动的产物是一种建模语言，而不是一种建模方法，所以从0 9 版起， 改称“统一建模语言”。并于1 9 9 7 年1 月将u m l 提交到对象管理组织( o m g ) 申请成为种标准建模语言。1 9 9 7 年1 1 月u m l l 1 版被o m g 采纳。此后u m l 还在继续改进，曰前最新的版本是u m l 2 0 。 2 、u m l 语义的缺陷及形式化语义的必要性 u m l 自从其产生发布之日起，在得到广泛肯定的同时也受到了批评。尽管 u m l 的体系结构具有适合变化的功能，并且u m l 的改进的过程也是严格的和 合理的，但由于u m l 的复杂性并没有使得它本身不存在任何问题。与u m l 有 关的不同人员根据不同的专业背景分别从不同的角度提出了自己的意见。其中， 面向对象领域的学者对u m l 提出的观点与意见最为丰富，不同的学者分别就 u m l 的不同的侧面中存在的问题，提出了不同的观点，其中有许多观点集中在 对u m l 的理论探索尤其是针对u m l 的语义研究。有的学者认为尽管在u m l 中已经规定了形式化的语法，但大部分语义却是用自然语言描述的，因此存在许 多歧义和不一致性。德国软件方法学家g r e g o re n g e l s 在其论文中指出：“部分上 下文有关语法及语义并没有形式化的指明，这使得可以对个u m l 模型有许多 不同的解释”。因此很多学者使用了数学或形式化的工具进行分析，有的学者在 批评u m l 现有版本的同时，还提出了自己的套解决方案，试图用来影响u m l 后续版本的修订。 在u m l 规范中，u m l 的结构是基于四层元模型结构的。四层元模型结构依 次是：用户对象层、模型层、元模型层、元一元模型层。u m l 语义的描述是通 过元模型描述的。元模型是通过以下这些观点用半形式化方法描述u m l 的。 抽象语法用类图和支持的自然语言描述。用元模型表示元模型自己，这 本身存在理论限制。 良构规则用形式化语言对象限制语言o c l 和自然语言描述。 u m l 状态机的形式化语义研究 语义主要是自然语言以及一些已经被描述过的模型符号来描述。 鉴于u m l 存在缺乏一个精确的形式化的语义，目前许多组织与个人正在从事 形式化语义的研究工作。比较有代表性的从事u m l 形式化语义研究的组织是英国 的p u m l 组( p r e c i s eu m lg r o u p ) 。p u m l 组是一个由研究人员和实践人员组成的 国际性组织，其目标是运用浅显的数学知识将u m l 发展成为一种精确的( 形式的) 建模语言。对u m l 形式语义的研究，主要有以下优点： 清晰的解释：如果某一个u m l 组件在某一点上的意思存在混淆，形式化语义 可以作为参考来验证它的解释。因此，那些不是u m l 创造者设计系统他们 不会按照错误的解释进行设计。 严格的分析与设计：如果与模型有关的概念用形式化描述技术去表达，那么 将使得对图形执行严格的语义分析成为可能，从而以至于对系统进行严格的 评估和有系统地实施。在实践中0 0 图形的验证是非形式化的。这些非形式 化的技术是不充分的，以至于它们不能用来严格建立实施与模型的彼此一致。 有力的证据：形式化语义将为u m l 模型提供一个强有力的形式化分析与理由。 它将用于证明那些用u m l 描述的系统重要属性的证明和检查是正确的，比如 安全性。 扩展性的验证：形式化语义将使u m l 任何扩展的正确性得到验证。 等价性与一致性：它将对u m l 与其它技术和符号的比较和对比提供一个不具 有二义性的基础并且保证了u m l 内不同组件之间的一致性。 但是将形式化的方法作为手段去研究建模语言时，应该谨慎选择所使用的形式化 工具，不应单纯地强调其理论价值而忽视了业内大多数人对这科- 形式化方法的理 解。 3 、有关形式化语义的方法 目前，学术界对u m l 语义进行形式化的方法越来越多，p u m l 组织总结了两种 最常见的形式化语义的方法。 补充法：在这种方法中，直接用形式化规格语言对u m l 模型的语义进行形式 化。常见的形式语言如：z 、l s l ( l a r c hs h a r e dl a n g u a g e ) 具有面向对象扩展的形式语言方法：在这种方法里，用具有面向对象特征的形 式规格语言对u m l 的元模型进行形式化来作为对语义形式化的替代。常见的形 u m l 状态机的形式化语义研究 式语言如：o b j e c t - - z 。 上面两种方法各具有优点，但是在补充法中所使用的形式化语言不具有面向对象 特征，不能很好地运用到当前实践中，而具有面向对象扩展的形式语言方法又不 能直接对u m l 模型的语义进行形式化，影响了读者对u m l 模型形式化的理解。 为了更好地对u m l 进行形式化，本文将两种方法结合起来，先对u m l 的元模 型的语法结构进行分析通过具有面向对象特征的r a i s e 的说明语言r s l 直接 对u m l 模型的语义进行形式化。 u m l 状态机的形式化语义研究 第二章u m l 2 1u m l 的概貌 u m l 是一种绘制软件蓝图的标准语言。可以用u m l 对软件密集型系统的制品 进行可视化、详述、构造和文档化。它是一种表达力丰富的语言，可以描述各种 开发所需要的视图，然后以次为基础装配系统。虽然u m l 表达力比较丰富，但是 理解和使用它并不困难。要学习使用u m l ，一个有效的出发点是形成下述语言的 概念模型，这要求学习三个要素：u m l 的基本构造块、支配这些构造块如何放在 一起的规则和些运用于整个u m l 的公共机制。 ( 1 ) u m i ，的构造块 u m l 的词汇表包括三个基本构造块： a 事物 b 关系 c 图 事物是对模型中最具代表性的成分的抽象；关系把事物结台在一起；图聚集 了相关的事物。 1 ) 事物 在u m i 。中有四种事物：结构事物、行为事物、分组事物、注释事物。这些事 物是u m l 中基本的面向对象的构造块。用它们可以写出结构良好的模型。 a 结构事物 结构事物( s t r u c t u r a lt h i n g ) 是u 札模型中的名词。它们通常是模型中的 静态部分，描述概念或物理元素。共有以下7 种结构事物：类( c l a s s ) 、接口 ( i n t e r f a c e ) 、协作( c o l l a b o r a t i o n ) 、用( u s ec a s e ) 、主动类( a c t i l v ec l a s s ) 、构件 ( c o m p o n e n t ) 、节点( n o d e ) 。 b 行为事物 行为事物( b e h a v i o r a lt h i n g ) ；是u m l 模型的动态部分。它们是模型中的动词，描 述了跨越时间和空间的行为。共有以下两类主要的行为事物：交互和状态机。交 互和状态机这两种元素是可以包含在u m l 模型中的基本行为事物。在语义上，这 些元素通常与各种结构元素( 主要是类、协作和对象) 相关。 c 分组事物 分组事物( g r o u p i n gt h i n g ) ；黾u m l 模型的组织部分。它们是一些由模型分解成 的“盒子”。在所有的分组事物中，最主要的分组事物是包。 d 注释事物 注释事物( a n n o t a t i o n a lt h i n g ) 是u m l 模型的解释部分。这些注释事物用来描 述、说i g j 车【i 杯往模型的任何元素。有一种主要的注释事物，称为注解。 2 ) 关系 在u m l 中有4 种关系：依赖、关联、泛化和实现。 这些关系是u m l 的基本关系构造块，用它们可以写出结构良好的模型。 a 依赖( d e p e n d e n c y ) 是两个事物间的语义关系，其中一个事物( 独立事物) 发生 变化会影响到另一个事物( 依赖事物) 的语义。 b 关联( a s s o c i a t i o n ) 是一种结构关系，它描述了一组链，链是对象之间的连接。 c 泛化( g e n e r a l i z a t i o n ) 是一种特殊一般关系，特殊元素( 子元素) 的对象可替代 一般元素( 父元素) 的对象。 d 实现( r e a l i z a t i o n ) 是类元之间的语义关系，其中一个类元指定了由另外一个类元 保证执行的契约。 3 ) u m l 中的图 l 虱( d i a g r a m ) 是一组元素的图形表示，大多数情况下把图画成顶点( 代表事物) 和弧( 代表关系) 的连通图。为了对系统进行可视化，可以从不同的角度画图， 这样图是对系统的投影。在理论上，图可以包含任何事物及其关系的组合。在实 际中，它们要与5 种最有用的组成了软件密集型系统的体系结构的视图相致。 因此，u m l 包括了如下9 种这样的图：类图( c l a s sd i a g r a m ) 、 象- ( o b j e c t d i a g r a m ) 、用况图( u s e c a s e d i a g r a m ) 、顺序图( s e q u e n c ed i a g r a m ) 、协作图 ( c o l l a b o r a t i o nd i a g r a m ) 、状态图( s t a t e c h a nd i a g r a m ) 、活动图( a c t i l c i t yd i a g r a m ) 、构 件 ( c o m p o n e n td i a g r a m ) 、实施i g l ( d e p l o y m e n td i a g r a m ) 。 ( 2 ) u m l 的规则 像任何语言一样，u m l 有一套规则，这些规则描述了一个结构良好的模型 看起来应该像什么。一个结构良好的模型应该在语义上是前后致的，并且与所 有的相关模型一致。 u m l 有用于描述如下事物的语义规则： 6 u m l 状态机的形式化语义研究 a 命名：为事物、关系和图起名 b 范围：给一个名称以特定含义的语境 c 可见性：怎样让其他人使用或看见名称 d 完整性：事物如何正确、一致地相互联系 e 执行：运行或模拟动态模型的含义是什么 ( 3 ) u m l 中的公共机制 在u m l 中有4 种贯穿整个语言且一致应用的公共机制。这四种机制是：详述、 修饰、通用划分和扩展机制。 2 ，2u m l 的语言结构 u m l 足使用元模型f 式定义的。u m l 的语言体系结构是基于4 层元模型体系 结构的。元模型体系结构是4 层模型从上到下依次是：元一元模型、元模型、模 型层和用户对象层。元一元模型层形成了元模型体系结构的基础，元模型是元一 元模型的实例，模型是元模型的实例，用户对象是模型的实例。 元模型的体系结构模式已被证明可以用来定义复杂模型所要求的精确语义，这种 复杂模型通常需要被可靠地保存、共享、操作以及在工具之间进行交换。它的特 点如下： 它在每一层都递归地定义语义结构，从而使语义更精确、更正规。 它可用来定义重量级和轻量级扩展机制，如定义新的元类和构造型。 它在体系结构上将u m l 元模型与其他基于4 层元模型体系结构的标准( 比 如m o f 和用于模型交换的x m if a c i l i t y ) 统一起来。 在元模型层，u m l 元模型又被分解为三个逻辑子包：基础包、行为元素包 和模型管理包。( 如下图所示) u m l 状态机的形式化语义研究 基础包由核心、扩展机制和数据类型三个子包构成，它是描述模型静态结构 的语言底层结构，支持类图、对象图、构件图、部署图等结构图。 ( 基本包示意图) 行为元素包是描述模型动态行为的语言上层结构，支持不同的行为图，包括 u s e c a s e ( 用况) 图、顺序图、协作图、状态图和活动图。 幺 ( 行为元素包示意图) 8 u m l 状态机的形式化语义研究 模型管理包则定义了对模型元素进行分组和管理的语义，它描述了几种分组 结构，包括包、模型和子系统。行为元素包和模型管理包都依赖于基础包。 9 u m l 状态机的形式化语义研究 第三章r a i s e r a i s e ( r i g o r o u sa p p r o a c ht oi n d u s t r ys o f t w a r ee n g i n e e r i n g ) r a i s e 工业软件工程的严格方法是一个1 9 8 5 年到1 9 9 0 年的e s p r i t 项月，耗费了大约1 2 0 人年的工作量。d a n s kd a t a m a n t i kc e n t e ( 1 9 8 8 年被 c o m p u t e r r e s o u r c e si n t e r n a t i o n a l 接管) 是此项目的主要的承接者。s t c t e c h n o l o g y ( 现在称为8 n re u r o p e ) 是第二个参与者。n o r d i s kb r o w nb o v e r i ( 现在称为s y p r o ) 和部分i c l ( 现在属于f u j i t s u ) 也作为二 业实验者参加了 此项目。r a i s e 是在一个广谱的规范语言的基础上，提供一系列工具和转换技术。 形成一种开发软件的严格方法。 丌发r a i s e 项目的动力起初来自v d m ，v d m 存在两个明显的不足之处，第 它缺乏模块性，第二v d m 不能处理并发的情况，r a i s e 还使用了完全不同的方法， 代数法。该方法与v d m 和z 基于模型的方法在下面两方面存在不同之处，即如何 描述事物以及如何给规范语言赋予语义。基于模型的方法没有明确解决如何将这 两方面结合起来的问题。而r a i s e 规范语言r s l ( r a i s es p e c i f i c a t i o n l a n g u a g e ) 做到了这一点。这正是r a i s e 的成功之处。 r s l 中的模块性得益于代数语言( c l e a r ，a s l 等) 。而并发则是基于过程代数 ( 与c s p 和c c s 类似) ，但是又加入了内锁( i n t e r l o c k ) 操作符。 r s l 是一种广谱的语言，它既可以用于书写非常抽象的、初级的规范，也可 以用于书写易于甚至能自动转换成程序语言的更具体的规范。开发中需要一种广 谱的语言，希望在各个开发层次上都可以使用同一种语言，进而处于同一个语言 框架下面。事实证明，在同一个开发层次上甚至在同一模块内拥有结合不同抽象 程度定义的能力是非常有用的。 l 、r s l 的规约能力 下面通过一个比较基础的r s l 规范来把握其基本特点。这个规范描述了某协 会登记的数据库，它可以允许某人登记为会员，或者检查某人是否已经登记。规 范如下： d a t a b a s e = c l a s s t y p e 1 0 u m l 状态机的形式化语义研究 p e r s o n ， d a t a b a s e = p e r s o n s e t v a l u e e m p t y ：d a t a b a s e ， r e g i s t e r ：p e r s o n x d a t a b a s e - + d a t a b a s e ， c h e c k ：p e r s o n d a t a b a s e - - b 0 0 1 a x i o f f e m p t y ； ) ， v p ：p e r s o n ，d b ：d a t a b a s e r e g is t e r ( , 1 3 ，d b ) - - e p ) u d b ， v p ：p e r s o n ，d b ：d a t a b a s e , c h e c k ( p ，d b ) - e p e d b e n d ( 1 ) 模块 简单的模块定义有如下形式： id c l a s s d e c l a r a t i o n s e n d 每一个说明( d e c l a r a t i o n ) 可以由一个关键字( t y p e ，v a l u e ，a x i o m ) 开始，以 表明该说明的种类，接着是多个该种说明的定义。例如在d a t a b a s e 中定义了两 个类型p e r s o n 和d a t a b a s e ，三个值e m p t y ( 常量) 、r e g i s t e r ( 函数) 和c h e c k ( 函数) 以及三个公理。 ( 2 ) 类型说明 类型是逻辑上相关值的集合，这些值带有若干预定义的值文字( 代表值) 和 若干用于生成和操作该类型的值的操作符( 代表函数值) 。 固有类型( 即预定义类型) 的例子有n a t 。它包含了由文字0 ，l ，2 ，代 表的自然数。其中作用在自然数上的预定义操作符有加操作符+ 等，因此可以 书写如下形式的n a t 类型的值表达式5 + 7 。 除了固有类型，用户还可以自己定义类型，在前面的例子中便有这样的定义， p e r s o n 和d a t a b a s e 。 u m l 状态机的形式化语义研究 p e r s o n 被定义为新类型标识符，这样p e r s o n 是个抽象类型。除了= 和， 它没有其他预定义的生成和操作该类型值的操作符。 p e r s o n 被定义为抽象类型反映了定义者的需要。即不需要给出会员的姓名等 具体信息，即对此类细节进行了抽象。 d a t a b a s e 类型被定义为等于集合类型表达式p e r s o n s e t 。这是一种简写定 义，就是把名字d a t a b a s e 定义为p e r s o n s e t 的简写。 也可以把d a t a b a s e 定义为其他形式，但是既然没有人可以登记多次，而且 登记的顺序也无关，因此d a t a b a s e 被定义为集合形式是很自然的。 ( 3 ) 值的说明 在前面的例子中有三个值的定义，每个定义都给出了值的名字和类型。 第一个值定义给出了d a t a b a s e 类型的常量e m p t y ，这个值表示空的数据库。 标识符e m p t y 所代表的实际值并没有在值的定义中给出而是在公理中作了捕 述，其他几个值的定义也是如此。 在第二个值定义中定义了函数r e g i s t e r ，它将一个人添加到数据库。假设当 前数据库是d b ，而我们登记会员j o h n 。那么r e g i s t e r ( j o h n ，d b ) 就代表登记过 后的数据库。 r e g i s t e r 的类型由类型表达式p e r s o n x d a t a b a s e - - d a t a b a s e 表示。 这个类型表达式是由两个类型操作符( 就像定义d a t a b a s e 使用的- s e t ) 和一生成的。第一个操作符结合性更强，因此这个类型表达式中类型操作符( 笛 卡儿积) 作用于p e r s o n 和d a t a b a s e 上，而类型操作符一( 函数空间) 则是作用 于笛卡儿积的结果和d a t a b a s e 上的。 第三个值定义了函数c h e c k ，它作用于p e r s o n 和d a t a b a s e 上，并且返回固 有类型b 0 0 1 中的布尔值。b o o l 类型中包含了两个值，其文字表示为t r u e 和 f a l s e 。c h e c k 函数仅当这个人已经在数据库中登记返回t r u e 。 总之，在一个模块中可以定义零个或多个命名的类型以及零个或多个命名的 值。 ( 4 ) 公理的说明 公理表达了值的名字的属性。在前面的例子中有三个公理，第一个公理定义 名字e m p t y 代表( 人的) 空集。 1 2 u m l 状态机的形式化语义研究 主要其中使用了恒等符号= ，而不是相等符号= 。这两个符号在应用式规范 的上下文中含义几乎相同。而在基于状态和基于并行的上下文中，两者的含义有 根本的不同。为了取得一致性，符号= 在公理中通常被用作“最外层比较操作 符”。 第二个公理表明函数r e g i s t e r 通过取两个集合的并集，把一个人p 加入到 数据库d b 中，其中d b 是一个集合，而单集合 p 只包含p 。 这个公理是量化表达式，读作：对任意的人p 和任意的数据库d b ，r e g i s t e r 作用于( p ，d b ) 恒等于d b o p ) 。 第三个公理定义了函数c h e c k ，当一个人属于数据库这个集合时，此人已被 登记。 对于每一个值标识符，如果公理中能够确切地说明该表示符所表示类型的值 的情况。则公理集是完全的。例如，e m p t y 被定义为只代表空集。同样的，函数 r e g i s t e r 代表将其第一个参数添加到第二个参数中的唯一函数。 当然，公理不需要一定是完全的。最极端的情况是根本没有公理。这时值表 示符可以表示其类型内的任何值。 下面给出不完全公理集的例子。假设现在重新定义函数c h e c k ：对任何人p 和数据库d b 如果p 在d b 内，可能还满足其他条件，则函数返回值t r u e 。这个 定义可以用下面的公理描述： a x i o m v p ：p e r s o n ，d b ：d a t a b a s e c h e c k ( p ，d b ) p d b 这个公理表明对任何人p 和数据库d b ，如果谓词c h e c k ( p ，d b ) 成立，则有 p d b 。 这个公理是不完全的，因为有多个定义在p e r s o n x d a t a b a s e 一- b o o l 的c h e c k 函数满足该公理。其中之一是根据原先的公理定义的函数： a x i o m v p ：p e r s o n ，d b ：d a t a b a s e oc h e c k ( p ，曲) - = - p c d b 另一个函数满足以下公理： a x i o m v p ：p e r s o n ，d b ：d a t a b a s e , c h e c k ( p ，曲) - = p e d b a o l d e n o u g h ( p ) 1 3 u m l 状态机的形式化语义研究 这里函数o l d e n o u g h ( p ) 返回t r u e ，如果p 达到法定年龄。 如果一个标识符没有完全被公理指定( s p e c i f i e d ) ，称其为宋指定的 ( u n d e r s p e c i f i e d ) 。 为了整理文档的需求和在证明中引用方便起见，公理可以被命名。例如定义 e m p t y ，c h e c k ，r e g i s t e r 的公理可以写成如下形式： a x i o m e m p t y a x i o m e m p t y - = ) ， r e g i s t e r a x i o m v p ：p e r s o n ，d b ：d a t a b a s e r e g is t e r ( p ，d b ) 暮 p ) u d b ， c h e c k a x io m v p ：p e r s o n ，d b ：d a t a b a s e oc h e c k ( p 。d b ) ；- p e d b ( 5 ) 值和公理说明的结合 当公理具有特别的形式时，r s l 为值和公理说明的结合提供了简写形式。例 如，我们可以对常量e m p t y 作如下定义： v a l u e e m p t y ：d a t a b s e = ) 4 u m l 状态机的形式化语义研究 第四章u m l 状态机的形式语义研究 4 1u m l 状态机的抽象语法 u m l 状态机( s t a t em a c h i n e ) 是这样的一种行为，它描述了一个对象或一 个交互在生命期内n 向应事件所经历的状态序列。单个类或一组类之间协作的行为 可以用状态机来描述。显示一个状态机的图被称为状态图( s t a t e c h a r td i a g r a m ) 。 在u m l 标准规格说明中，u m l 状态机的语法结