（计算机应用技术专业论文）objectz规格说明的动画模拟技术研究和实现.pdf

| ，海人学颂1 学位沦文 1 1 t ep o s t g r a d u a t et h e s i so f , s h a n g h a iu n i v e r s i t y 摘要 形式化方法足种建立在严格数学基础上的软件开发方法。在软件开发过程 中使用形式化方法，既可以提高目标软件系统的正确性和可靠性，又能提高软件 的玎发效率。但是，_ f 因为形式方法以严格的数学理论为基础，所以用它束描述 的软什需求规格说明比较抽象难懂。而且，般柬既，形式化的规格况明语毒嗜b 是不可执行的，用户利领域专家对形式化规格说明及其符弓方面的知识了解甚 少，很难去理解形式化规格说明，也就难以确定规格说明是否与他们的需求相 致。为此，人们提出要划形式化的需求规格既明进行确认和验证。 本文主要研究了软件需求规格酏明的种确认方法动画模拟技术，并最 终研究开发了一个o b j e c t z 规格说明动画模拟系统o z a n i m a t o r ，该系统能 够模拟执行o b j e c t z 规格说明，帮助人们理解需求规格说明，从而实现对规格说 明的致性确认。 首先，本文为o b i e c t z 规格说明定义了一种通用的x m l 格式，动画模拟系 统将处理满足该格式的o b j e c t 。z 规格说明。 其次，在结构模拟部分，作者选择s i c s t u sp r o l o g 作为动画模拟语言，根据 o b j e c t z 规格说明语言的语法语义，制定了一系列由o b j e c t z 规格说明到p r o l o g 文件的转换规则，并使用x s l t 描述出来。在动i 画过程中，输入的o b j e c t z 规格 说明将根据这些转换规则自动转换成呵执行的p r o l o g 程序。 作者使用j a v a 语言+ 设计了个良好的动画模拟界面，该界面包含了o b j e c t z 规格说明的文档结构、类的属性和变化情况、用户的操作过程以及错误信息的显 示，实现了用户与规格说明的交互的需求和进行需求确认的目的。 最后以多个实例对本动画模拟系统进行了测试，证明本系统能够正确有效地 模拟执行o b j e c t z 规格说明，并且根据测试结果对这种动画模拟技术进行了相关 的讨论。 关键词：形式方法，形式规格说明，确认，验证，动画模拟，o b j e c t z ，p r o l o g 1 黼人学蛳卜学位论文 t h ep o s t o r a d u a t et i1 e s 】so fs h a n g l1 a 1u n i v e r s l t y a b s t r a c t f o r m a lm e t h o d sa r ek i n d so fs o f t w a r ed e v e l o p m e n tm e t h o d sb a s e do ns t r i c t m a t h e m a t i c s i tc a ni m p r o v ec o r r e c t n e s sa n dr e l i a b i l i t yo fs o f t w a r es y s t e ma n dt h e e f f i c i e n c yo fs o f t w a r ed e v e l o p m e n tb u tj u s tb e c a u s ef o r m a lm e t h o d sa r eb a s e do nt h e t h e o r y o fm a t h e m a t i c s t h o s e r e q u i r e m e n t ss p e c i f i c a t i o n s d e s c r i b e db yf o r m a l m e t h o d sa r ev e r ya b s t r a c ta n dd i f f i c u l tt ou n d e r s t a n d a tt h es a m et i m e ，i ng e n e r a l ， f o r m a ls p e c i f i c a t i o nl a n g u a g e sa r ea l m o s tn o n e x e c u t a b l e a n du s e r sa n dd o m a i n e x p e r t sh a v el i t t l ek n o w l e d g ea b o u tf o r m a ls p e c i f i c a t i o n sa n dn o t a t i o n t h e ya l m o s t c a l m o tu n d e r s t a n dt h e m ，s a y i n gn o t h i n gt ov a l i d a t et h ec o n s i s t e n c yb e t w e e nu s e r s i n f o r m a lr e q u i r e m e n t sa n df o r m a ls p e c i f i c a t i o n s o ，v a l i d a t i o na n dv e r i f i c a t i o no f f o r m a ls p e c i f i c a t i o nh a v eb e e ni n t r o d u c e d i n t h i st h e s i s w ed i s c u s st h ev a l i d a t i o nm e t h o do ff o r m a ls p e c i f i c a t i o n 一一一 a n i m a t i o n 挪】dd e v e l o pas t r u c t u r a la n i m a t i o ns y s t e mo fo b j e c t zs p e c i f i c a t i o nn a m e d o z a n i m a t o rw h i c hc a ns i m u l a t ea n de x e c u t eo l ! j e c t z s p e c i f i c a t i o n a n dt h e n i m p l e m e n tt h ev a l i d a t i o no fc o n s i s t e n c y f i l l s t w ed e f i n eag e n e r i cx m lf o r m a tf o ro b j e c t zs p e c i f i c a t i o n t h ea n i m a t i o n s y s t e mw i l ld e a lw i t ht h es p e c i f i c a t i o n si nt h i sf o r m a t s e c o n d ，i nt h ep r o c e s so fs t r u c t u r es i m u l a t i o n ，a u t h o rc h o o s e ss i c s t u sp r o l o ga s a n i m a t i o nl a n g u a g ea n dd e f i n e sas e to ft r a n s l a t i o nr u l e sf r o mo b j e c t - zs p e c i f i c a t i o n t op r o l o ga c c o r d i n gt ot h es y n t a xa n ds e m a n t i c so fo b j e c t ，zs p e c i f i c a t i o nl a n g u a g e ， t h e s er u l e sf i n a l l ya r ed e s c r i b e di nx s l t i na n i m a t i o n ，t h ei n p u t t e do b j e c t z s p e c i f i c a t i o nw i l lb et r a n s l a t e di n t oa ne x e c u t a b l ep r o g r a mi np r o t o g j a v ai su s e dt od e s i g nau s e rf r i e n d l yg u if o ra n i m a t i o ns y s t e m t h es t r u c t u r eo f o b j e c t zs p e c i f i c a t i o nf i l e 、p r o p e r t i e so fc l a s s e sa n dt h e i rc h a n g e s 、t h e u s e r s o p e r a t i o n sm a de r r o ri n f o r m a t i o na r ea l ls h o w n i nt h i sg u i ，w h i c hs h o u l ds a t i s f yt h e u s e r s r e q u i r e m e n t st oi n t e r a c tw i t hs p e c i f i c a t i o na n dt h ea i m t ov a l i d a t i o n f i n a l l y w ei l l u s t r a t e o u rs y s t e mb ys e v e r a le x a m p l e s t h ee x p e r i m e n tr e s u l t s s h o wt h a ti tc o u l di m p l e m e n tt h es i m u l a t i o no fs p e c i f i c a t i o n sc o r r e c t l y a tt h es a m e t i m e ，t h ei n s u f f i c i e n c i e si nt h i ss t r u c t u r es i m u l a t i o nt e c h n o l o g ya r ed i s c u s s e d k e yw o r d s ：f o r m a lm e t h o d s ，f o r m a ls p e c i f i c a t i o n ，v a l i d a t i o n ，v e r i f i c a t i o n ， a n i m a t i o n ，s i m u l a t i o n ，o b j e c t z ，p r o l o g ! 坚呈旦q ! ! 鱼垦垒旦竺垒! 曼! 旦垦坠! q ! ! 婪垒盟鱼旦垒! 堕塑! y 曼垦墨! ! 原创性声明 本人声明：所呈交的论文是本人在导师指导下进行的研究工作。 除了文中特别加以标注和致谢的地方外，论文中不包含其他人已发 表或撰写过的研究成果。参与同一工作的其他同志对本研究所做的 任何贡献均已在论文中作了明确的说明并表示了谢意。 签名 本论文使用授权说明 本人完全了解上海大学有关保留、使用学位论文的规定，即：学校有权保留论文及 送交论文复印件，允许论文被查阅和借阅：学校可以公布论文的全部或部分山容。 ( 保密的论文在解密后应遵守此规定) 签名 扛 导师签名：缝璐担：日期：鲨：兰：! j 枉 上海大学硕士学位论文 下h ep o s t g r a d u a t et h e s i s0 fs h a n g h a iu n i v e r s i t y 第一章绪论 需求工程是软件工程的个重要分支，覆盖了体系结构设计之前的各项开发 活动，其主要结果软件需求规格说明描述了整个软件系统的功能和性能，是 整个软件开发生命周期的基础，其正确性与否对于提高软件的质量、降低软件开 发代价有着极大的影响。因此，研究软件需求规格说明的确认和验证方法对于需 求工程乃至整个软件工程来说都具有极其重要的意义。 1 1课题的研究背景 1 1 1 需求工程、软件需求规格说明 需求工程( r e q u i r e m e me n g i n e e r i n g ) 是应用已证实有效的技术和方法进 行需求分析、确定客户需求、帮助分析人员理解问题并定义目标系统的所有外部 特征。它通过合适的工具和记号系统地描述待开发的系统及其行为特征和相关约 束，最后形成需求文档，并对用户不断变化的需求演化给予支持。 需求工程可以分为系统需求工程( 针对由软硬件共同组成的整个系统) 和软 件需求工程( 仅针对软件部分) 。软件需求工程是一个不断反复的需求定义、文 档记录、需求演化的过程，并最终在验证的基础上冻结需求。它可以分为五个独 立的阶段：需求获取、需求建模、形成需求规格说明、需求验证和需求管理。 软件需求工程的主要结果就是软件需求规格说明( s o f t w a r er e q u i x e m e m s p e c i f i c a t i o n ) ，它也是整个软件开发生命周期的基础。软件需求规格说明是关于 外部行为和系统环境接口的简洁完整韵描述性文档，它阐述了一个软件系统必须 提供的功能和性能以及它所要考虑的限制条件。它广泛适用于在各种应用领域中 对客户问题的理解与描述，实现用户、分析员和设计人员之间的通信，为软件设 计提供基础，并支持系统的需求验证和演化。 软件需求的基本内容包括行为需求和非行为需求。行为需求定义系统需要做 什么，描述系统输入输出的映射及其关联信息，完整地刻画系统功能，是整个软 件需求的核心。非行为需求则是定义系统的属性，描述与行为无关的目标系统特 性，包括系统的性能、有效性、可靠性、安全性、易维护性、可见性和顺应性。 一个良好的软件需求规格说明应该具有如下特点：正确性、无二义性、完整性、 可验证性、可修改性、可跟踪性、易理解性以及有好的注解等等。 1 1 2 非形式化方法、半形式化方法和形式化方法 t 海大学硕士学位论文 堕! q ! ! 鱼坠旦型i 些! 丛! j 坚q ! ! 坚皇盟垒旦垒! ! 型! y ! 垦! 型 现有的软件需求规格说明的描述方法总的来说有三种：非形式化方法 ( i n f o r m a lm e t h o d ) 、半形式化方法( s e m i - f o r m a lm e t h o d ) 和形式化方法( f o r m a l m e t h o d ，简称f m ) 。 表1 - 1非形式化方法、半形式化方法和形式化方法的比较 t a b l 1c o m p a r eo f i n f o r m a lm e t h o d s ，s e m i f o r m a lm e t h o d sa n df o r m a lm e t h o d s 非形式化方法半形式化方法形式化方法 语法直观形式化形式化 语义直观直观 形式化 歧义性最容易产生歧义有歧义歧义性较弱 可理解性最容易理解可以理解难以理解 精确性精确性最低较为精确最精确 从表1 1 中可以看出非形式化方法采用了丰富生动的自然语言，易于理解和 使用，但是它具有固有的二义性，因此表达的语义不明确，难以保证其正确性、 可维护性，也难以用计算机系统提供自动化的支持，这对于安全性的软件系统来 说可能会造成严重的人身伤害、环境破坏和经济损失。最常见的非形式化方法有 结构化分析法( s a ) 和各种面向对象分析法( o o a ) 。 半形式化方法在宏观上对语法有较为精确的描述，但在某些局部方面则允许 使用非形式化的自然语言。半形式化方法通常有两条途径：一是采用图形化方法 对语言的总体结构加以刻画；另一种途径是对系统需求所涉及的各个侧面加以总 结，通过较精确的语法对之进行刻画。这种方法的主要特点是既便于用户的表达 和理解，又可在某种程度上使用机器对需求规格说明进行管理和部分正确性检 查。目前备受关注的一种半形式化方法就是u l v 几( 可视化建模语言) 。 形式化方法是一种基于数学方法来描述目标软件系统性质的技术，它只描述 系统要干什么而不涉及怎么干，逻辑、代数、自动机、图论等构成其数学基础 2 1 。 形式化方法大致分为两类【3 】：一是面向模型的，即应用一系列数学结构构造系统 的模型，直接定义系统的行为；二是面向特征的，即通过给出系统必须满足的公 理集来描述系统的特征，从而间接地定义系统的行为。由于形式化方法能精确描 述对象的行为和特性，并且独立于程序编码，它是使系统设计走向工程化的一个 重要步骤，能有效弥补非形式化方法以及半形式化方法的许多缺点，因此，我们 可以在系统开发之前利用形式化方法来描述其功能，并通过用户的不断反馈加以 改进和接近实际模型。 形式化方法的主要研究内容包括形式化的需求规格说明和形式化验证。形式 化规格说明是使用具有精确语义的形式语言对系统“做什么”的数学描述，它是 设计和编制程序的出发点，也是验证程序是否正确的依据。形式化验证包括规格 2 上海大学硕士学位论文 ! ! ! ! q ! 里q 丛q 型! ! ；! ! ! ! 堡q ! ! 基垒型鱼基垒! ! 型! ! 垦! ! ! 说明验证和程序验证。当前，我们主要研究的是形式化规格说明的确认和验证。 1 1 3 形式化规格说明语言 一般来说，形式化规格说明是使用某种形式化规格说明语言，在某抽象层上 表达系统应该满足的特征集合。形式化规格说明语言提供了一个称为语法域的记 号系统和一个称为语义域的目标集合，以及一组精确地定义哪些目标系统满足哪 个规格说明的规则【5 l 。自2 0 世纪6 0 年代起，国内外就不断出现各种不同的形式 化规格说明语言。例如，z 语言是一种具有“状态操作”风格的形式化规格 语言。它以一阶谓词逻辑和集合论为基础，利用集合、关系、函数、序列和包等 数学概念，使用状态模式和操作模式对目标系统的状态和操作进行说明，具有简 明和精确的特点。z 语言在工业界和学术界得到了广泛的应用，常被称作是“软 件工程”语言。而本文所要研究的o b j e c t z 规格说明语言是对z 语言在面向对 象方面的一种扩充。图1 1 简单列出了形式化规格说明语言的发展历程。 所有的形式化规格说明语言大致可以分为以下两大类： _ 基于代数和公理，包括c l e a r , o b j ，l a r c h ，c a f e o b j ，l o t o s 等 基于模型，包括v d m ，z ，b ，o b j e c t - z 等 1 j 7 。 h o a r e 逻辑 抽 数据 l a r c h b c a f e o b j a s l 图1 - 1 形式化规格说明语言的发展史 f i 9 1 1t h ep h y l o g e n yo f f o r m a ls p e c i f i c a t i o nl a n g u a g e 使用形式化规格说明语言来描述软件的需求规格说明具有以下的优点： 形式化规格说明以严格的数学概念和理论为基础，因而避免了使用自然 语言描述时可能带来的模糊性和歧义性。 形式化规格说明语言具有很强的抽象性，避免了在需求分析阶段对数据 结构和算法细节的详细描述； 上海大学硕士学位论文 卫! g ! ! ! 塑坠q ! ! 婴堕型! 业! ! ! ! 鲤型竖! ! ! ! ! ! ! ! 说明验证和程序验证。当前，我们主要研究的是形式化规格说明的确认和验证。 1 l3 形式化规格说明语言 一般来说，形式化规格说明是使用某种形式化规格说明语言，在某抽象层上 表达系统应该满足的特征集合。形式化规格说明语言提供了一个称为语法域的记 号系统和一个称为语义域的目标集合，以及一组精确地定义哪些目标系统满足哪 个规格说明的规则口i 。自2 0 世纪6 0 年代起，国内外就不断出现各种不同的形式 化规格说明语言。例如，z 语言是一种具有“状态操作”风格的形式化规格 语言。它以一阶谓词逻辑和集合论为基础，利用集合、关系、函数、序列和包等 数学概念，使用状态模式和操作模式对目标系统的状态和操作进行说明，具有简 明和精确的特点。z 语言在工业界和学术界得到了广泛的应用，常被称作是“软 件工程”语言。而本文所要研究的o b j e c t z 规格说明语言是对z 语言在面向对 象方面的一种扩充。图1 - 1 简单列出了形式化规格说明语言的发展历程。 所有的形式化规格说明语言大致可以分为以下两大类： 基于代数和公理，包括c l e a r , o b j ，l a r c h ，c a f e o b j ，l o t o s 等 基于模型，包括v d m ，z ，b ，o b j e c t - z 等 b c a l e o b j c a s l 图l 一1 形式化规格说明语言的发展史 f i 9 1 1t h e p h y l o g e n y o f f o r m a ls p e c i f i c a t i o n l a n g u a g e 使用形式化规格说明语言来描述软件的需求规格说明具有以下的优点： _ 形式化规格说明以严格的数学概念和理论为基础，因而避免了使用自然 语言描述时可能带来的模糊性和歧义性。 _ 形式化规格说明语言具有很强的抽象性，避免了在需求分析阶段对数据 结构和算法细节的详细描述； 结构和算法细节的详细描述； ；| 辑墉im逻 e 海大学硕士学位论文 t h ep o s t g r a d u a t e1 h e s i so fs h a n g h a iu n i v e r s i t y 形式化规格说明可以通过自动化工具( 如定理证明器、模型测试器和动 画模拟等) 进行确认、验证以及求精变换，从而揭示或消除规格说明中 的不一致性、不完整性、重复性以及不明确性，增强对用户需求的洞察 和理解，鼓励软件可靠性、生产力和质量的改进； _ 形式化规格说明确切地指出了目标系统各方面的特性，有助于系统的实 现。 1 i 4 问题的提出 虽然使用形式化规格说明语言所描述的软件需求规格说明简洁而又紧凑，但 是同时它也比较抽象难懂。一般来说，形式化规格说明语言都是不可执行的，用 户和领域专家对形式规格说明和符号方面的知识了解甚少，很难理解形式规格说 明，也就难以确定规格说明是否与他们的需求相一致。为了清除形式规格说明中 的不一致性和模糊性，并确保能从规格说明中推断出所需的系统特征，我们必须 对形式规格说明进行确认( v a l i d a t i o n ) 和验证( v e r i f i c a t i o n ) 。 所谓确认就是对“软件满足用户需求”的描述进行一致性和完整性论证，即 “我们是否建立了一个正确的系统”。而验证则是对系统开发的每个阶段的输出 和前一个阶段的输出进行比较，从而确保新阶段的输出满足了其前一阶段输出所 提出的需求，通俗地讲，就是“我们是否正确地建立了一个系统”。本文所要研 究的规格说明的动画模拟技术( a n i m a t i o n ，简称为动画) 就是一种确认方法。 1 2 研究形式化规格说明的动画模拟的意义 形式化规格说明的动画模拟是将形式化规格说明转换成一种可模拟执行的 形式而不丢失规格说明所提供的语义【i2 1 ，从而检查在给定的限制条件下系统实现 的可行性，实现规格说明者和用户之间的交流，从而找到误解之处。 与形式推理相比较，虽然一个完整的形式推理能让我们对规格说明给予更大 的自信，但是同时需要广泛的专门技术，费时费力【l 叭，而动画方法相对而言就比 较简单，所花的代价也比较低。 快速原型和动画都是用来确保一个形式规格说明与用户所表达的非形式需 求之间的一致性，都是通过测试数据来运行软件的。但两者在抽象层次和获取逻 辑结果的可能性范围上有所不同：原型是构建目标软件的个版本，可能含有非 功能性的需求，面动画与目标软件的抽象相关；快速原型方法仅用于展示目标软 件的功能，而动画还可以显示规格说明中的逻辑关系1 6 j 。 总的来说，规格说明的动画模拟，其作用和目的有很多： 1 ) 、动画能被用来帮助开发者更好地理解用户需求以及确认规格说明 7 1 。 上海大学硕士学位论文 ! 婴! q i 卫坠旦堕! 匹瑾坠堡塑；丛型鱼奠垒! 竖! ! ! 垦i ! 卫 2 ) 、通过动画获得早期的反馈对于规格说明的验证来说是非常有用的瞄】，能 够帮助减少规格说明的错误【9 】。 3 ) 、动画使得规格说明文档的测试和调试在传统方式上成为可能【l “，通过交 互式的测试，很多问题都可以被检测出来i l 。 1 3形式规格说明的动画在国内外的发展状况 目前，所有的动画工具大多都是针对不同的规格说明语言特别是z 语言和b 语言进行研究和开发实现的。 1 3 1b 规格说明的动画工具 b z t t ( b z t e s t i n g t o o l s ) 【l5 】实现了b 规格说明的动画，它从初始状态开 始模拟操作序列的执行，显示不确定性操作的解决方案，这是一个典型的基于值 的动画，用户在动画模拟每个操作时需要提供值作为输入参数。 p r o b 【”是另一种b 模型检查器，它是使用s i c s t u sp r o l o g 的t c k t k 库进行 开发，并在其早期c s p 动画器的基础上加以构建。它支持b 模型一致性的自动 检查、基于约束的检查、可回溯的动画以及非确定性操作。 1 3 2z 规格说明的动画工具 z 是一种应用较为广泛的形式化规格说明语言，但是从许多用户的反馈信息 来看，z 语言描述大型系统进行规格说明时层次性的功能还不够强、模块化能力 不是很强，从而影响了z 规格说明的可理解性。 z a n s 1 3 】_ 【1 4 1 是d e p a u l 大学的x i a o p i n gj i a 等开发的一种z 动画工具，它实 现了z 规格说明的类型检查、模式表达式的扩充、表达式和谓词的计算以及确定 性操作模式的执行，但是不能处理非确定性的操作模式。 p o s s u m 【1 5 1 是由q u e e n s l a n d 大学的s v r c 小组开发的一种s u m 规格说明动画 工具，亦可以模拟z 规格说明。它最终采用了m e r c u r y 语言作为其动画语言。这 一工具的优点在于它提供了一个使用t c i t k 构建的g u i ，其中包含一个主要的 解释窗口、一个脚本窗口以及一个用于修改p o s s u m 变量行为的参数窗口，从而 方便人们在不熟悉规格说明语言的情况下通过该用户界面与规格说明进行交互； 它能创建、记录、保存和再次运行脚本。其主要缺点则是没有相应的文档支持。 除此之外，z 的动画工具还有p i z a 、p i p e d r e a m 方法、z a l 系统、z e t a z a p 工具等等。 随着面向对象方法的流行，人们在系统分析、系统设计、程序设计以及系统 上海大学硕士学位论文 ! 丛! ! 竺! ! g 坠望望! 堡! ! ! i 坚q ! ! 堕垒型鱼旦垒! ! 型盟! 垦! ! ! 测试方面都提出了新的观点和技术。为了更好的描述大型系统和面向对象的软件 系统，9 0 年代以后，国际上相继出现了多种z 规格说明语言的扩展方案，其中 较著名的有o b j e c t z ，z + + 等，在国内也设计了面向对象的结构化规格说明语言， 例如o o z s 。 1 3 3 o b j e c t z 规格说明的动画模拟技术研究现状 o b j e c t z 规格说明语言是q u e e n s l a n d 大学开发的一种z 语言的面向对象的 扩充，主要用于形式化描述面向对象的系统。到目前为止，只有q u e e n s l a n d 大 学的s v r c 小组对该规格说明语言提出了一种动画方法。这种动画方法的主要思 想是在z 中建立一个框架来管理对象和对象引用的动态实例。这个框架包含一个 明确的对象引用表，用来描述对象引用和对象之间的映射，并且在该表中所有来 自o b j e c t z 规格说明的操作都会被转换成z 的操作。在动画工具的实现方面， 他们利用已开发的z 动画工具_ p o s s u m ，为其创建了一个接口，用来执行由 o b j e c t z 到z 的必要转换，另外为用户提供一个交互式的接口，该接口允许对象 的动态实例化以及操作的调用。但是，这种方法存在一些问题：o b j e c t - z 语言 本身引入了许多z 语言未使用到的结构，一些特征( 如引用语义等) 的动画相对 而言比较简单，还有一些结构( 如使用递归定义的操作、对象的非限制性结构以 及向前构成等) 却给这种动画方法带来了挑战。另外，类对象的状态不变式可能 对系统中的其他对象给予了一定的限制，因此改变一个对象的属性可能会违背对 该对象保持引用的其他对象的状态不变式，这一特性也给动画带来了一定的困 扰，必须在动画中引入一个全局检查机制，用于保证在每个操作执行完以后没有 对象的状态不变式发生不协调的状况。 1 4 本文的主要研究内容 本文的研究主题是o b j e c t z 规格说明的动画模拟技术，是国家自然科学基金 和上海市教委科学技术发展基金资助的“面向对象的规格说明的构造与形式化验 证和确认”项目的一部分，研究的主要内容如下： 1 、介绍规格说明动画的相关概念，讨论分析动画的两种基本策略形式 化程序综合和结构模拟的优缺点，并以结构模拟动画技术为基础，简要说明本文 所要研究的o b j e c t z 规格说明的动画技术。 2 、定义动画文件格式：根据动画的特性，比较分析现存的各种o b j e c t - z 规 格说明的文件存储格式的优缺点，最后选择x m l 来描述作为动画器输入的 o b j e c t z 规格说明的文件格式，并通过分析o b j e c t z 规格说明的语法和语义结构， t ：拇大学坝士学位论文 王! ! ! 望j ! 望些垒望型! ! ! ! 型! ! 坚q ! ! 丛皇型垒坚垒! ! 型! ! 垦! ! ! ! 定义了一个通用的o b j e c t z 规格说明文件的x m l 模式，从而有助于简化整个动 画过程以及提高动画器的性能。 3 、定义转换规则：阐明选择s i c s t u sp r o l o g 作为o b j e c t - z 规格说明的动画 语言的原因和优点，通过分析o b j e c t z 规格说明各组成部分的作用和特点，详细 讨论和制定了由o b j e c t z 规格说明到p r o l o g 可执行程序的具体转换规则，并使 用x s l t 加以描述。 4 、设计和实现o b j e c t - z 动画器o z 蜘a r i n o r ：使用j a v a 语言编写一个用 户友好的动画界面，显示对规格说明的操作检测过程，并及时返回操作结果，实 现用户与规格说明之间的友好交互过程。 5 、分析实验数据和实验结果，对动画器的性能做出评价。 6 、总结和展望。 上海大学硕士学位论文 t h ep o s t g p , a d u a t et h e s i so fs h a n g h a iu n e r s l t y 第二章形式化规格说明的动画模拟 形式化规格说明的动画模拟技术是一种形式化确认方法，本章主要介绍动画 模拟技术的基本概念、基本策略以及动画语言的选择，并概括介绍了本文所提出 的o b j e c t - z 规格说明的结构模拟动画技术的基本方法和策略。 2 1 什么是动画模拟 所谓形式化规格说明的动画模拟就是将形式化规格说明转换成一种可模拟 执行的形式而不丢失规格说明所提供的语义，检查在给定限制条件下系统实现的 可行性，实现规格说明者和用户之间的交流，从而找到误解之处。它提供了一种 交互式动态测试模型的方法，能够帮助人们更好地理解形式规格说明( 见图2 1 ) ： 用户和领域专家可以通过动画与规格说明进行交互并观察其操作行为；说明者通 过动画检查规格说明是否反映了他们设计的预期特征，是否与用户所表达的非形 式需求相一致，从而定位误解之处；动画也可以应用到形式化规格说明的教学和 学习之中：老师可以通过动画向学生证明规格说明的作用，学生也可以通过动画 确定他们所书写的规格说明的意思：另外，为动画提供自动化的支持相对而言比 较容易，实现代价也比较低。鹅 d e v e 话d e r sc u s t o m e r 图2 - 1 动画环境结构图 f i 9 2 1t h es t r u c t u r eo f a n i m a t i o ne n v i r o n m e n t 上海大学硕士学位论文 1 h ep o s t g r a d u a t et h e s i so fs h a n g h a iu n i v e r s i t y 2 2 动画的基本策略 到目前为止，人们提出了很多形式化规格说明的动画模拟策略，例如将规格 说明转换成使用p r o l o g 、m e r c u r y 、o z 、j a v a 等语言所书写的可执行程序并加以 执行，还有人提出使用数据库的方式来实现对规格说明的动画【2 引。但总的来说， 这些动画方法可归结为两类【6 1 ：一类是形式化程序综合( f o r m a lp r o g r a m s y n t h e s i s ) ，也称之为直接动画；另一类是结构模拟( s t r u c t u r es i m u l a t i o n ) ，或称 为非直接动画。 形式化程序综合是指直接解释并执行规格说明，在动画之前不需要修改规格 说明，它的一个重要特征就是最终的可执行程序逻辑上是由形式规格说明所产生 的，因此，该可执行程序相对于规格说明的正确性就得到了保证。该方法的主要 缺点在于对于个具体的分解步骤，缺少精确的算法来判断哪个推理法则是最适 合的，这需要依赖于人的智慧和经验来作出判断和选择。 结构模拟技术是一种对规格说明的抽象接近，即将形式化规格说明语言的具 体语义与动画语言的近似语义联系起来。它除了形式化转换规格说明以外，它还 会识别出规格说明的基本特征并加以改编，这样规格说明的逻辑结构就尽可能地 被保留在可执行的结果模型当中。 本文所要研究的o b j e c t z 规格说明的动画是以结构模拟技术为基础，将 o b j e c t z 规格说明转换成s i c s t u s p r o l o g 可执行程序加以执行，从而实现o b j e c t - z 规格说明与用户需求的一致性确认。 2 3 o b j e c t z 规格说明的动画模拟技术 2 3 1 o b j e c t z 规格说明语言简介 本课题研究的主要内容是o b j e c t z 规格说明的动画技术。o b j e c t z 语言是一 个基于模型的面向对象的规格说明语言，它对z 进行了面向对象的扩充，包括类 和对象、继承和多态、引用类型语义等概念以及强大的模式计算，同时，现有的 z 语言的语法和语义在o b j e c t z 语言中仍然被保留。目前，o b j e c t - z 规格说明语 言已经在学术界和工业界得到了广泛的应用。 一个系统的o b j e c t z 规格说明由一系列的类模式所组成，每个类模式中都封 装了一定的状态模式和操作模式。通过继承和多态的方式，规格说明书写人员就 可以使用面向对象的方式来构造软件需求规格说明。在此，我们使用o b j e c t z 语言来描述个小型文件系统( 见图2 2 ) 。 在该类定义中，第一行是类的可见列表，明确定义类对象的环境中所有能被 p 海大学硕士学位论文 ! 旦! ! 竺! 堕坠里型苎堡! 旦! ! 堡盟! 坚趔鱼望型型! ! 垦! ! 坚 引用的类属性，包括常量、状态变量、初始状态模式以及操作；第二行定义了一 个基本类型f i l e i d ，用于限制在这文件系统中可用的文件范围；第三行是一个公 理定义，它引入一个局部常量m a x f i l e s ，指出系统可容纳的最大文件数目；接下 来分别是类的状态模式( 无模式名) 、初始状态模式i n i t 以及操作模式a d d f i d 。 另外，因为该类没有父类，所以其继承属性在图2 2 中没有明确地标识出来。 图2 - 2 小型文件系统的类模式图 f i 9 2 2c l a s ss c h e m ao f s i m p l ef i l es y s t e m 2 3 2 o b j e e t - z 规格说明动画语言的选择 规格说明可以转换成多种可执行语言来动画执行，例如： p r o l o g ( p i z a ：h t t p ：w w w n o o d l e s d e m o n c o u k p i z a p i z a h o m e h t m l ) ： - m e r c u r y ( p o s s u m ：h t t p ：s v r c i t u q e d u a u p o s s u m p o s s u m h t m l ) ： - h a s k e l l ( j a z a ：h t t p ：w w w c s w a i k a t o a c n z m a r k u i a z a ) 等等。 o b j e c t - z 语言是一种面向对象的规格说明语言，因此，使用一种面向对象的 可执行语言来动画o b j c c t - z 规格说明是一种比较好的选择，因为它具有动画所需 的特殊的功能符号和适应性。 上海大学硕士学位论文 塑! ! 垡j ! 垒丛旦型盟! 型型! 坐! 垡型垡旦型蜊! ! 坠! ! 兰 p r o l o g 语言是一种最常用的逻辑程序设计语言，它的编译程序和解释程序在 许多计算机上都是广泛可用的，并且提供了一种非常简单适用的查询方法，另外 它和o b j e c t - z 都是基于一阶谓词逻辑的，因此由o b j e c t z 模式自动转换成p r o l o g 子句是完全有可能的。而s i c s t u sp r o l o g 是p r o l o g 的所有版本中较为出色的，它 包含有对象库，可以满足o b j e c t - z 规格说明中面向对象特征的动画模拟需求，除 此之外，它的内部谓词非常丰富，提供了列表、有序集合、图、带权图等丰富的 库。另外，它还支持u n i x 和w i n d o w s 等各种操作系统平台以及限定( c o n s t r a i n t ) 程序设计。因此本课题决定采用s i c s t u sp r o l o g 作为o b j e c t z 规格说明的动画语 言环境，以下的所有p r o l o g 描述均是基于s i c s t u sp r o l o g3 1 0 1 版本。 2 3 3 o b j e c t z 规格说明的动画方法概述 本文所讨论的o b j e c t z 规格说明的动画方法以结构模拟动画技术为基础，制 定一系列由o b j e e t z 到s i c s t u sp r o l o g 的转换规则，最终将产生一个o b j e c t z 动 画器，该动画器处理x m l 格式的o b j e c t z 规格说明，通过转换规则将其转换成 p r o l o g 可执行程序并加以运行，从而实现对o b j e c t - z 规格说明的动画确认。 首先，定义o b j e c t z 规格说明的一个通用x m l 格式，只有符合该格式的 o b j e c t z 规格说明才能作为动画器的输入文件，继而被转换处理。 其次，制定o b j e c t z 的各个组成部分以及模式计算的转换技术规则，并使用 x s l t 模板描述该转换规则，使得x s l t 处理器能够解释o b j e c t z 规格说明，通 过遍历该规格说明的文档结构来获取所需的数据信息并进行相应的处理，最终形 成一个s i c s t u sp r o l o g 可执行程序。 最后，使用j a v a 设计一个友好的图形用户界面，用于显示目标系统的各种 功能、用户操作的前置条件、操作的过程和结果、错误及错误产生的原因等等， 方便用户与动画系统之间的交互，帮助人们理解该需求规格说明，从而确认软件 系统的功能和特征。 上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s i so fs h a n g h a iu n i v e r s i t y 第三章o b j e c t z 规格说明的动画格式定义 动画模拟0 b j e c t z 规格说明，首先要将规格说明清楚地显示在动画界面上以 便于规格说明者和用户的检查和修改：其次要对规格说明进行类型检查和结构确 认，保证动画输入文件的有效性；最后要从规格说明中取出所需的数据，通过一 定的转换规则将其转换成可执行程序并执行。为了尽可能容易地实现这些目标， 作为动画输入的o b j e c t - z 规格说明的文件格式是一个必须考虑的基本要素。本章 着重讨论作为动画系统的输入文件的o b j e c t z 规格说明的格式描述。 3 1b o x 格式、l a t e x 格式和x m l 格式 o b j e c t - z 语言是一种半图形化的规格说明语言，大多数信息是通过逻辑语句 表达出来的，还有些信息则是通过图形标记来进行传达，如图2 - 2 中小型文件系 统的规格说明描述就是采用了这种b o x 格式。使用这种格式来存储o b j e c t - z 规 格说明虽然阅读起来比较简单，但是它使得o b j e c t z 规格说明自动解析变得非常