（计算机软件与理论专业论文）基于切片的objectz规格说明的sql动画模拟技术.pdf

上海大学硕士学位论文 t 呱p 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 | t y 摘要 形式化方法是一种用数学方法来描述和验证目标软件系统性质的方法它 通常用形式规格说明语言来描述软件需求。由于用数学符号描述的软件规格说 明比较抽象。而且是不可执行的，因此非专业人员不太容易理解，很难判断所 给出的规格说明是否与他们的需求一致。这就需要对规格说明进行确认。本文 研究的规格说明的动画模拟就是一种规格说明的确认方法，它将不可执行的规 格说明转换成一种可执行的程序，用户执行转换后的程序，根据执行后的反馈 信息判断该规格说明是否符合他们的需求。 由于s q l 在动画模拟中的诸多优点，因此在本文的研究中将s q l 作为动 画模拟o b j e c t - z 规格说明的目标语言。从o b j e c t - z 到s q l 的转换是本文的研究 重点，本文利用两种语言之间的相似性，制定了相应的转换规则，提出了利用 数据表表示各种类型的数据变量的方法；并提出模块封装的思想，即用存储过 程表示类、对象和模式等模块，用户通过调用执行存储过程确认规格说明是否 满足其需求。 在动画模拟过程中首先需要进行规格说明语言到s q l 语言的转换。通常动 画模拟都是针对规格说明的某个部分进行的，因此就没必要对整个规格说明转 换，只需要提取相关的部分即可。为此，本文提出了分层的规格说明切片方法， 并将它运用于规格说明的动画模拟中，提高了动画模拟的效率和准确性。 本文还讨论了用x m l 描述o b j e c t z 规格说明的方法，根据动画模拟的特 点用x m ls c h e m a 分别对规格说明中的变量和各种模块定义了格式，使规格说 明的描述格式尽量为动画模拟带来方便。 最后根据研究的方法开发了一个规格说明的动画模拟工具，该工具可以自 动将用户输入的规格说明转换成s q l 程序，并将执行转换后的结果显示在界面 上，以方便用户对规格说明的一致性做出判断。 关键词：o b j e c t - z ，s q l ，动画模拟，切片，x m l v 上海大学硕士学位论文 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 y a b s t r a c t f o r m a lm e t h o di sam a t h e m a t i c a lm e t h o du s e dt od e s c r i b et h ea i m e ds o f t w a r e s y s t e ma n d t ov e r i f yt h ep r o p e r t i e so f t h e s y s t e m 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 e o f t e nu s e dt od e s c r i b et h es o f t w a r er e q u i r e m e n t s s i n c et h ef o r m a ls p e c i f i c a t i o n d e s c r i b e dw i t hm a t h e m a t i cs y m b o l si sa b s t m c la n di sn o te x e c u t a b l e ，i ti sd i f f i c u l tt o u n d e r s t a n df o rt h o s ew h oa r en o tp r o f e s s i o n a l a n di ti sa l s od i f f i c u l tt oj u d g e w h e t h e rt h es p e c i f i c a t i o na c c o r d sw i t ht h eu s e r sr e q u i r e m e n t s b e c a u s eo ft h e r e a s o n sa b o v e ，i ti sn e c e s s a r yt ov a l i d a t et h ef 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 no f s p e c i f i c a t i o ns t u d i e di n t h i sp a p e ri sn a m e l yam e t h o do ff o r m a lv a l i d a t i o n i t c o n v e y st h es p e c i f i c a t i o nw h i c hi sn o te x e c u t a b l et oa ne x e c u t a b l ep r o g r a m 。u s e r s c a nv a l i d a t et h es p e c i f i c a t i o na c c o r d i n gt ot h ef e e d b a c ka f t e rr u n n i n gt h ec o n v e r t e d p r o g r a m d u et ot h ea d v a n t a g e so fs q li nt h ea n i m a t i o n ，s q li sc h o s e nt ob et h eo b j e c t l a n g u a g ei nt h es t u d y t h i sp a p e rf o c u s e so nt h et r a n s f o r m a t i o nf r o mo b j e c t - z s p e c i f i c a t i o nt os q la s e to f t r a n s f o r m a t i o nr u l e sa r ee s t a b l i s h e d t h em a i ni d e ao f t h em e t h o di s d e n o t i n gk i n d so fd a t av a r i a b l e sw i t hd a t a s h e e la n dm o d u l e e n c a p s u l a t i o n , n a m e l yd e n o t i n gc l a s s e s ，o b j e c t s ，s c h e m a sa n de t e w i t hs t o r a g e p r o c e d u r e s ，u s e r sc a nv a l i d a t et h es p e c i f i c a t i o nt h r o u g hc a l l i n gt h ep r o c e d u r e s t h el a n g u a g et r a n s f o r m a t i o ni st h ef i r s ts t e pa n di t u s u a l l ya i m st op o r t i o n d u r i n gt h ea n i m a t i o n ，i ti su n n e c e s s a r yt ot r a n s f o r mt h ew h o l es p e c i f i c a t i o n ，b u to n l y t h ec o r r e l a t i v ep a r t s s ot h el a y e r e dm e t h o do f t h es p e c i f i c a t i o ns l i c i n gi sp r o p o s e di n t h i sp a p e r , a n di ti sa p p l i e dt ot h ea n i m a t i o nt oi m p r o v et h ee f f i c i e n c ya n dp r e c i s i o n t h ep a p e ra l s od i s c u s s e st h ed e s c r i p t i o no fo b j e c t - zs p e c i f i c a t i o nw i t hx m l d e f i n i n gt h ef o r m a to ft h ev a r i a b l ea n dd i f f e r e n tk i n d so fm o d u l e sa c c o r d i n gt ot h e c h a r a c t e r i s t i co fa n i m a t i o nw i t hx m ls c h e m a ，s oa st om a k et h ed e s c r i p t i o nf o r m a t 那c o n v e n i e n tf o ra n i m a t i o n 越p o s s i b l e f i n a l l ya l la n i m a t i o nt o o li sd e v e l o p e d t h et o o lc a nc o n v e r t st h es p e c i f i c a t i o n i n p u tb yu s e r st os q la u t o m a t i c a l l y ，a n ds h o wt h ee x e c u t i o nr e s u l to nt h ei n t e r f a c e t h r o u g hw h i c hu s e r sc a nj u d g et h es p e c i f i c a t i o nc o n s i s t e n c yc o n v e n i e n t l y k e y w o r d s ：o b j e e t - z ，s q l 。a n i m a t i o n ，s l i c i n g ，x m l v l 上海大学硕士学位论文 1 1 正p o s t g r a d u a t et h e s i so fs h a n g h a lu n i v e r s i t y 原创性声明 本人声明：所呈交的论文是本人在导师指导下进行的研究工作。 除了文中特别加以标注和致谢的地方外，论文中不包含其他人已发 表或撰写过的研究成果。参与同一工作的其他同志对本研究所做的 任何贡献均已在论文中作了明确的说明并表示了谢意。 签名： 本论文使用授权说明 本人完全了解上海大学有关保留、使用学位论文的规定，即： 学校有权保留论文及送交论文复印件，允许论文被查阅和借阅；学 校可以公布论文的全部或部分内容。 ( 保密的论文在解密后应遵守此规定) 签名：导师签名：日期： 上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s l so fs h a n g h a u n v e r s i t y 第一章绪论 软件质量越来越受到人们的重视，软件形式化方法是提高软件质量的有效 方法。在软 孛开发中使用彤式化方法克服了用自然语言描述规格说明的模糊性， 使软件开发效率明显提高。形式化方法用规格说明语言来描述软件需求。为了 确信用规格说明语言描述的需求与用户需求一致，可以使用规格说明的确认方 法。 1 1 形式化方法 1 1 1 形式化方法简介 随着信息技术的不断发展，计算机已广泛应用于社会的各个领域，人们越 来越重视软件的质量。大量软件项目开发的事实表明：大部分的软件开发费用 是用于纠正在测试阶段发现的各种错误，而这些错误中的很大一部分是由于在 需求分析阶段对规格说明描述不耩确引起的。为了克驻采用自然语言和程序设 计语言描述规格说明的缺陷，人们提出了形式化方法。它是一种严谨的软件 开发和设计方法，基本思想是对系统建立一个数学模型，研究和提供一种基于 数学的和形式语义学的软件规格说明语言，用这种语言严格、精确地描述所开 发软件的功能，采用形式推理的方法来保证所给出的规格说明是一致的，并且 符合用户的需求，然后将它转换成可执行的代码。 形式化方法的优越之处在于其具有严格的数学基础与描述性，在软件开发 过程中使用形式化方法有下列优点：( 1 ) 规格说明是精确的；( 2 ) 由误解引起 的错误减少；( 3 ) 规格说明有利于系统实现；( 4 ) 能对形式规格说明进行正确 性证明。使用形式化方法不仅可提高软件系统的正确性和可靠性，而且还可提 高软件开发的效率。该方法日益受到计算机界和工业界的高度重视，并将得到 越来越广泛的应用。例如。美国的交通碰撞避免系统t c & s 玎、髓公司的 a n a l y s i si n f o r m a t i o nl i b r a r y 、欧洲e s p r i t 项目的l a r g ec o r r e c ts y s t e m 等都使用了形式化方法。 1 i 2 形式化规格说明语言 形式化方法采用形式规格说明语言来描述和验证软件系统。形式规格说明 语言提供了一个称为语法域的记号系统和一个称为语义域的目标集合，以及一 组精确地定义哪些目标系统满足哪个规格说明的规则。到目前为止，已出现了 很多形式规格说明语言，这些语言的方法和理论基础所设计的领域十分广泛， 上海大学硕士学位论文 ! 堡丝! ! 垒坠! ! ! 坚! 堕堕q ! ! 坠! 鱼坠! 型! ! 墅堕 包括集合论、谓词逻辑、模式演算基础、代数基础和范畴论基础等。不同的规 格说明语言在表达能力、术语以及支持形式处理的能力方面有所不同，每种语 言的侧重点也不同。根据对目标软件系统进行说明的方法，可将形式化规格说 明语言分成两类【l 】：基于模型的规格说明语言和基于代数的规格说明语言。其 中，z 、o b i e c t - z 、v d m 、b 就是基于模型的规格说明语言，c l e a r 、a c t o n e 、 o b j 是基于代数的规格说明语言。 1 1 3 形式化方法的支持工具 目前已有一些支持形式化方法的工具，如对于z ，有英国o x f o r d 大学开发的 b t o o l 和f u z z 、y o r k 大学开发的c a d i z 。j ，它能对z 规格说明进行语法检查和类型 检查，并支持排版，允许用户通过人机交互的方式查看规格说明中的某些特性。 美国芝加哥d ep a u l 大学研制的类型检查工具z t c 3 ，它可接受l a t e x - z e d 格式的 规格说明。国内也已开发了一些形式化方法的支持工具，如江西师范大学开发 的c 0 0 z t o o l s 。：，本课题组开发的zu s e rs t u d i o 。5 。和o b j e c t - z 编辑工具。但是 遗憾的是现在尚未出现支持形式化方法全过程的软件环境。 1 2 o b j e c t z 规格说明语言 o b j e c t z 陋培言是一种面向对象的形式规格说明语言，它是面向对象技术和 形式化方法的统一。它对z 语言在面向对象方面进行了扩充，同时z 语言现有的 语法和语义在o b j e c t - z q b 仍被保留。随着面向对象技术的广泛使用，面向对象的 规格说明语言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 规格说明是由一系列封装的模块一类组成的，类定义包 括一个定义了类名的模式框，类名中可能会含有形式参数。在这个模式框中可 能会依次包含以下几个部分：定义类接口的可见列表、继承类、局部定义、状 态模式、初始状态模式和操作模式( 见图i 1 ) 。 其中可见列表定义了类的接口，它明确地列出了类中可以被其他类或对象 引用的属性，这些属性包括常量、状态变量、初始状态模式和操作模式。继承 2 上海大学硬士学位论文 ! 壁翌! ! 鱼坠! ! 盟! 壁墅堕! 坠! 鲤垒! 型堕坠堕 类定义了这个类所继承的所有父类。局部定义包括基本类型定义( b a s i ct y p e s d e f n i t i o n s ) 、公理定义( a x i o m a t i cd e f i n i t i o n s ) 、缩写定义( a b b r e v i a t i o nd e f i n i t i o n s ) 和自由类型( f r e et y p e s ) 。状态模式定义了一个类的状态变量，它和局部的公理 描述一起，定义了类的可能状态。初始状态模式定义了类的初始状态，即类的 对象没有经过任何操作时所处的状态。操作描述了操作执行前后系统状态值之 间的关系，操作前后的状态都处于状态空间之中。操作和初始状态模式一起， 定义了类可能达到的状态。 图1 1o b j e c t z 规格说明的类模式框 图1 2 是一个用o b j e c t - z 规格说明语言书写的队列系统。这个系统由类 q u e u e t 和c q 岭u e 【1 组成，其中类c q u e u e 【1 继承了类q u e u e t ，也就是说 类c q u e u e t l 的定义，包括局部定义、状态和初始状态模式以及操作模式，都 要和它继承的类的定义合并。 图1 2o b j e c t - z 规格说明的队列系统 上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s i so fs | i a n g 队iu n i v e k s i t v 1 3 问题的提出 在软件开发中使用形式化方法提高了软件系统的可靠性、正确性和软件开 发效率，但是“我们如何保证所写的规格说明确实具有所要求的性质? ”，“如 何知道最后所写的程序与所写的规格说明是一致的? ”首先，规格说明比 较抽象，需要有较强的数学基础，不少开发人员感到不易理解。其次，规格说 明一般是不可执行的。如果用户和领域专家对形式规格说明方面的知识了解甚 少，就很难理解形式规格说明，也就难以确定规格说明是否与他们的需求相一 致。为了清除形式规格说明中的不一致性和模糊性，必须对形式规格说明进行 确认( v a l i d a t i o n ) 和验证( v e r i f i c a t i o n ) 1 7 。 所谓规格说明的确认就是对插述软件需求的规格说明进行检查，根据检查 的反馈结果，确定其所描述的系统功能是否满足最终用户的需求，即“我们是 否建立了一个正确的系统”。而规格说明的验证则是确定系统开发中一个给定阶 段的输出和上一个阶段确定的输出进行比较，从而确保新阶段的输出满足了其 前一阶段输出所提出的需求，即“我们是否正确地建立了一个系统”。本文研究 的动画模拟方法 s ( a n i m a t i o n ) 是- - 种规格说明的确认方法。 1 4 课题研究的意义 本文研究的课题是基于切片的规格说明的动画模拟方法。其中规格说明的 动画模拟就是将形式化规格说明转换成可模拟执行的程序而不丢失规格说明所 提供的语义，通过执行这个转换后的程序来检查靓格说明所描述的软件系统是 否与用户需求相一致。 使用规格说明的动画模拟主要有以下优点： ( 1 ) 动画模拟可以模拟系统的状态和行为，使得用户对规格说明的理解比 较直观； ( 2 ) 用户通过动画模拟的反馈信息确认规格说明，提高了规格说明的正确 性； ( 3 ) 动画模拟是执行转换后的程序，交互性较强，有利于用户和规格说明 之间的交流； ( 4 ) 动画模拟就是执行转换后的程序，为用户确认规格说明带来了方便。 在这个课题中切片是用来辅助动画模拟的，规格说明的切片是指从源规格说 明中抽取对规格说明中特定点上的特定变量有影响的语句和控制条件，组成新的 规格说明，即切片，然后就可以通过分析切片来分析源规格说明所描述的操作。 根据动画模拟的定义在动画模拟时先要把规格说明转换成一种可执行的程 序，但是动画模拟通常是对部分规格说明进行的，因此就没必要费时费力地转 4 上海大学硕士学位论文 ! 壁盟! ! g 坠! ! 坚! ! 些! ! ! 堕! 坠型鱼坠! 型堕墅坠 换整个规格说明。为此，我们在动画模拟前引入了切片以提取相关部分。在动 画模拟前使用切片技术使得动画模拟中需要转换的规格说明的范围大大缩小， 降低了整个过程的复杂性，提高了动画模拟的效率和准确性。 1 5 本文的组织结构 本文主要介绍了基于切片的o b j e c t z 规格说明的s q l 动画模拟技术，共有 七章组成，下面是各章的主要内容： 第一章绪论，介绍了形式化方法，o b j e c t z 规格说明语言，课题的提出， 其研究意义及本文的组织结构。 第二章介绍了规格说明的切片方法，先介绍程序切片及其发展，然后分析 了传统的切片，并提出了分层的规格说明切片技术及其在动画模拟中的应用， 最后给出了一个实例说明。 第三章介绍了规格说明的动画模拟技术，主要介绍了动画模拟的概念和方 法，以及当前国内外的发展情况。 第四章给出了o b j e c t - z 规格说明的s q l 动画模拟方法，详细介绍了将 o b j e c t - z 转换成s q l 的各种转换规则，并提出使用数据表表示规格说明中的变 量，利用存储过程表示模式等各模块。 第五章关于o b j e c t - z 动画模拟工具的设计和实现，介绍了o b j e c t z 规格说 明的x m l 格式，x m l 文件的解析方法和动画模拟器的主要部分的代码实现， 最后是工具的演示。 第六章总结和展望，对整个研究工作做了总结，并提出了需要改进的地方。 上海大学硕士学位论文 t 旺p 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 【v e r s r r y 第二章0 b j e c t - z 规格说明的切片 为了提高动画模拟的效率，我们应该尽可能地缩小动画模拟的范围，选取 动画模拟的相关部分。那么如何确定那些相关部分昵? 在此我们主要使用规格 说明的切片技术进行相关部分的提取。本文在已有的相关研究的基础上提出了 分层的规格说明切片技术，并用一个实例进行了说明。 2 1 切片技术简介 2 i 1 程序切片方法 目前对切片技术研究较多的是程序切片技术。程序切片是由w e i s e rm 【l0 l 提 出的一种重要的程序分析和理解方法，它是指从源程序p 中抽取对程序中特定点p 上的特定变量v 有影响的语句和控制条件。组成新的程序，即切片，然后通过分 析切片来分析源程序的行为，其中 为切片标准。 自从w e i s e rm 提出程序切片这个概念以来，许多专家学者纷纷对切片技术 进行了研究和应用开发，并取得了一些具有理论和应用价值的成果。二十年来 人们提出了静态切片1 1 0 1 和动态切片【1 3 】、前向切片和后向切片、过程问切片 和过程内切片【j6 】、面向对象的切片i 期、条件切片”8 1 、并发程序切片【1 9 1 等各种切 片类型。同时各种计算切片的方法也被先后提出，切片的计算方法主要分为四 个发展阶段。 第一阶段( 1 9 7 9 1 9 8 4 ) ：这一阶段主要是w e i s e rm 的研究阶段。该阶段的特 点主要是基于控制流图( c f g ) ，利用控制流和数据流来计算程序切片【lo 】。这种 方法主要适用于顺序结构和简单结构的程序的切片计算，而不适用于复杂结构 程序的切片计算。 第二阶段( 1 9 8 4 1 9 8 7 ) ：这一阶段是基于程序依赖图( p d g ) 的程序切片阶段。 它主要是基于程序依赖图利用图形可达性算法进行程序切片的计算【2 0 1 。这种方 法适合于计算过程内后向程序切片。 第三阶段( 1 9 8 8 1 9 9 4 ) ：这一阶段是基于系统层依赖图( s d g ) 的程序切片阶 段。h o r w i t z ，t r e p s 和d b i n k l e y 等人引入前向切片的概念及其算法和过程 间切片概念及其两阶段图形可达性算法【l ”，k o r e l 和l a s k i 引入动态切片的概 念和算法【2 l 】。这一阶段被认为是程序切片技术发展最成熟的阶段。 第四阶段( 1 9 9 4 至今) ：这一阶段是面向对象的程序切片阶段。随着面向对 象技术的出现，人们开始对面向对象程序进行切片研究，同时出现了多种类型 的程序切片。 6 上海大学硕士学位论文 ! 壁丝! ! 鱼坠望旦! 坚! 壁! ! ! 堕! 坠! 鱼坠! 竖! ! ! 堕坐 由于程序切片能够提取程序，简化问题，程序切片技术在程序分析、理解、 优化、调试、测试、度量、复用、程序变换、模型检查、软件维护、软件逆向 工程、软件再工程中都得到了广泛的应用。 2 1 2 规格说明的切片方法 虽然程序切片技术已有了二十年的研究，但是对形式规格说明切片方法的 研究才刚刚起步。目前很多的规格说明的切片方法研究都是基于程序切片方法 的。o d at 和a r a k ik 【2 3 】最先于1 9 9 3 年把程序切片的思想引入n z 形式规格说明 中，提出了用二元依赖关系计算静态形式规格说明切片的方法。此后c h a n gj 和r i c h a r d s o nd j 口j 于1 9 9 4 年在o d at 和a r a k ik 研究的基础上提出了静态形式 规格说明和动态形式规格说明。l e m i n e nj 【2 5 】把o t tl 研究并开发出的基于程序 切片的模块内聚度度量方法应用到z 形式化方法中，他还研究了模式内的数据切 片，并于1 9 9 4 年提出了形式规格说明算法，主要是把模式中的子句根据转换关 系转换为依赖范式，然后求解子句间的数据依赖关系。 2 2 o b j e c t z 规格说明的分层切片技术 2 2 1 传统的切片技术分析 在传统的切片技术中一般都用图形化的方法把程序中的信息表现出来以帮 助理解，基于程序依赖图和系统依赖图是计算程序切片的一个有效办法，目前 已有人提出了多种高效的构建程序依赖图和系统依赖图的方法及基于依赖图的 切片计算方法。传统的系统依赖图是在控制流图、数据流图、控制依赖图、数 据依赖图、过程依赖图和程序依赖图基础之上建立起来的一种语法分析树。在 图中结点表示各种程序构造、输入输出参数和调用位置等；边则表示节点之问 的各种依赖关系。 面向对象的切片方法相对于般的切片方法而言，它在面向对象方面进行 了扩充( 如类、对象、继承等) ，主要加了类层次图( c h g ) 以表示类之间的层次关 系。现在大部分的面向对象切片技术一般都采用“自底向上”的方法，即从方 法、过程等各种基本模块开始建过程依赖图( p d g ) ，然后依次建立类依赖图 ( c d g ) 、类层次图( c h g ) 、控制依赖图( c 1 d g ) 和数据依赖图( d d g ) ，最后建立 整个系统的系统依赖i 蛩( s d g ) 见图2 1 ) 。在实现程序的系统依赖图以后再根据 切片算法计算关于切片标准的切片。 上海大学硕士学位论文 t 旺p o s t g r a d u a t et h e s i so fs i i a n g h a il 厂m v e r s l l y 2 2 2 分层切片模型 图2 1 传统的面向对象切片技术 在以上过程中，随着从过程依赖图到系统依赖图的建立，表示程序构造、 输入输出参数等的节点数目急剧膨胀，结点之间的关系也愈加复杂，图的复杂 性随之提高从而增加了切片计算的难度影响了切片计算的准确性。 为了克服以上产生的问题，并结合o b j e c t - z 规格说明的特点，我们提出了 o b j e c t - z 规格说明的分层切片技术，它与传统面向对象切片技术的过程截然相 反，即“自顶向下”。这个方法的基本思想足：自项向下，逐步求精。在此把整 个规格说明分成三个层次，分别为系统层( s y s t e m ) 、类层( c l a s s ) 和模式层 ( s c h e m a ) ( 见图2 2 ) 。其中系统层是指整个o b j e c t - z 规格说明，它主要是由各个 类和全局变量组成；类层是指这个类中所有元素的集合，包括状态模式、初始 化模式和操作模式及类成员变量；模式层则是指每个模式中的谓词和变量。 系统层( s y s t e m ) ll 、l j r 类层( c l a s s ) l l 多 模式层( s c h e m a ) 图2 2o b j e c t - z 规格说明的层次模型 8 上海大学硕士学位论文 1 1 征p o s t g 凡d u a t et h e s i so fs h a n g h a iu n i v e r s l l y 2 2 3 分层切片方法 定义2 1 从源规格说明s 中抽取对规格说明中特定点p 上的特定变量v 有 影响的语句和控制条件，组成新的规格说明，即规格说明切片，然后通过分析 切片来分析源规格说明的行为。萁中 p ，砂称为规格说明的切片标准。 o b i e c t z 规格说明自顶向下求关于切片标准 的切片过程主要分成三 步，即依次对每个层次求与 相关的切片。在每一步的求精中根据每个层次 的相关依赖图进行求解。前两步的求精结果我们称之为粗粒度规格说明切片， 因为在这两步的求精过程中考虑的只是针对类或模式及相关的全局变量，并未 涉及模式内的每个谓词，在第三步中求得的结果则称之为细粒度规格说明切片， 也就是我们最后的期望结果。显然，对于一个规格说明关于同一切片标准 的粗粒度切片w 和细粒度切片t ，细粒度切片t 是粗粒度w 的子集，即有w t 成立。 1 ) 系统层 在计算有关切片标准 的系统层规格说明切片时，首先要根据整个规格 说明中的所有类、全局变量这些元素之间的关系建立系统层依赖图( s h d g ) ，系 统层依赖图的结点表示类或全局变量，边则表示类之间、全局变量之间或类和 全局变量之间的依赖关系，例如类之间的继承、类对其它类的引用、类对全局 变量的引用等，根据类或全局变量之间的依赖方向决定图中各条边的方向。 定义2 。2 设有两个类c 。和，其中c 。是c 。的子类，则称c ：类依赖于c 。 定义2 3 设有两个类c 。和c 2 ( 或c 。是一个全局变量) ，其中c ：引用c 。，则称 c 2 引用依赖于c 。 如果c ：类依赖( 引用依赖) 于c 。，那么类层次图中有向边的起点为c z ，有向边 的终点则为c 。根据图的可达性算法找出与包含p 和v 的类有关的类和全局变量， 删除那些无关的类和全局变量。通过这个步骤的计算所有无关的类和变量被删 除，图形中的元素个数明显减少，为后续的计算带来了方便。这一步骤得到的 切片是规格说明切片关于切片标准 的粗略版本s ( p ) “，设原规格说明为 p - - s ( p ) o ，则有s ( p ) o ：s ( p ) 1 成立。 2 ) 类层 类层计算的切片是对上一个步骤的精化，主要是找出与包含p 和v 的模式 有关的模式、类成员变量及上一步得到的全局变量。这个层次的切片计算首先 要建一个类层依赖图( c h d g ) ，就是把经过上一个步骤计算以后保留下来的类依 9 上 荤天掌坝士字但论文 ! 里堕! ! 鱼坠! ! 塑! ! 壁堕旦! ! 坠! 鱼坠! 型! 塑型垡 次展开，分别用它们的模式( 包括状态、初始化和操作模式) 和类成员变量表示。 在类层依赖图中结点表示类的各模式、类成员变量和经过第一步计算以后保留 下来的全局变量，边则表示模式之间、类成员变量之间、模式和成员变量之间 或模式和全局变量之间等各种依赖关系。在这个步骤的计算中除了要考虑一般 的依赖关系，还要考虑模式演算关系，包括模式运算，模式包含和模式修饰等， 通过模式演算以后，同个类的不同模式之间或不同的类的模式之间的变量或 谓词就会存在某种依赖关系，因此需要根据各种模式演算的不同特点进行分析。 假设存在模式s 1 、s 2 和s 3 ，下面选取几种模式演算来分析它们之间的依赖关 系。 模式包含( 、宴) 模式包含的目的是为了使规格说明的长度缩短，以使我们能够比较清 楚而简明地说明复杂操作。其中表示这个操作前后状态变量的值发生了变 化，而互则表示定义的操作不引起系统状态的任何改变。 对任意的模式s 。和s ：，如果s 。包含s 。那么模式s ：中变量的变化有可能 会使模式s 。中的变量也发生变化；如果s 。包含e s ：，模式s ：可能会使用模式s ： 中的变量来定义它自己的变量，由此推出模式s 依赖于模式s 。 模式复合( 8 ) 对任意的模式s 。、s 。和s ，如果有s 。毫s 稿s 。那么模式复合是用第一个 模式s ：的后状态变量关联第二个模式s 。的前状态变量。其中在模式s z 中变量 v 。变为变量v 2 ，模式s ，中变量v ：变为变量u ，那么s 。中则是由变量v 。变为变量 v 。，由此推断模式s 。依赖于模式s 。、s 。 模式合取运算( ) 对任意的模式s ，、s 。和s 。，如果有s 。兰s ：n s 。成立，模式合取运算就是第三 个模式s 的声明部分和谓词部分分别由前两个模式s 。和s 。的声明部分和谓词 部分组成。那么当模式s ：或s 。中的变量发生变化时可能会引起模式s 中的变 量发生变化，因此模式s 。依赖于模式s ：和s 。 模式蕴含( j ) 运算 对任意的模式s ，、s ：和s 。，如果有s 皇s ：j s 3 成立，模式蕴含运算就是把 两个模式s ：和s ，的声明部分合并得到第三个模式s 。的声明部分，而第三个模 i o 上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s i so fs h a n g 卧iu n i v e r s l l y 式s 的谓词部分则是由模式s ，和s 。的谓词部分经过j 运算得到。那么当模式 s ：，s 。中的变龟发生变化时可能会引起模式s 中的变量发生变化，因此模式 s ，可能模式依赖于模式s ：和s a 。 模式之间除了由于模式演算而存在模式依赖关系外，还有模式之间共用同 一全局变量，其中一个模式修改公共变量会使其它模式的其它变量也发生变化， 因此其它模式依赖于这个模式。除了模式之间的依赖关系外，还有类的成员变 量和模式、上一个步骤保留下来的全局变量和模式以及成员变量之间等都存在 依赖关系。 如果存在c 依赖于c 2 ，那么在表示类层依赖图时，c 。为图中有向边的起点， & 则是有向边的终点。同样利用图的可达性算法计算该层次的切片，保留与p 和 v 相关的模式和类成员变量及全局变量，删除那些无关的模式和类成员变量。经 过这次切片计算以后，一部分无关的元素又被删除。设这一步骤计算得到的关 于切片标准 的切片为s ( p ) 2 ，则有s ( p ) 0 2s ( p ) 1 js ( p ) 2 成立。 3 ) 模式层 经过前面两个步骤的计算以后，那些无关的类、模式和变量被删除。这个 层次的切片计算是在前两个步骤的基础上进一步细化，考虑的是模式中或模式 间的谓词或变量之间的依赖关系。 定义2 4 设p 。和p ：是规格说明中的任意两个谓词，若存在变量v 满足下列条 件，则称谓词p 。依赖于谓词p ：。 ( 1 ) p i 定义了v ，r 使用了v 的值： ( 2 ) p 2 的适用与否取决于p 。 计算这个层次的切片时，要把前一步骤结果中的模式依次展开，用模式层 依赖图( s h d g ) 表示，模式层依赖图( s h d g ) 可借鉴程序依赖图( p d g ) 的构造方法进 行构造。在构造模式层依赖图时，先把每个模式表示成一个图，其中节点表示 谓词或变量，边则表示谓词之阃的依赖关系，对于每个模式都会有一个入口节 点表示这个模式的入口。在用节点表示变量的过程中，模式中每个值未被该模 式改变的参数表示为f o r m a l i n 类型，而值被该模式改变的参数表示为 f o r m a l - o u t 类型。因此前状态变量和输入参数是f o r m a l - i n 类型，后状态变量和 输出变量是f o r m a l o u t 类型。最后根据模式之间、变量之间或模式和变量之间 的关系将它们连接成模式层依赖图( s h d g ) ，并用两阶段图的可达性算法计算关 于切片标准 的切片s ( p ) 3 。其中图的可达性算法见文献 1 5 。 经过这个步骤的计算以后，我们得到的是关于切片标准 最后的规格说 明切片s ( p ) ，显然有s ( p ) o ：s ( p ) 1 js ( p ) 2 ：s ( p ) 3 成立。 上海大学硕士学位论文 ! 壁! q ! ! 鱼坠里! 丝! ! 壁墅竺! 坚垒! 鱼坠! 型坚墅! 型 分层切片方法通过把整个系统分成三个层次，采用边构造边计算的方法， 避免了依赖图构造中元素个数的急剧膨胀，简化了整个计算过程，提高了切片 计算的效率和准确性。 2 2 4 规格说明切片在动画模拟中的应用 目前程序切片技术的应用已相当广泛，涉及软件开发过程中的很多方面， 而规格说明切片技术的应用范围则相对比较狭小，主要应用在规格说明的调试、 测试、理解和度量上。在本文的研究中，我们将规格说明的切片技术应用在动 画模拟中，利用切片技术提取需要动画模拟的部分和与其相关的部分，这样就 只需要将提取出来的部分进行转换即可。如果在规格说明确认时需要动画模拟 某个操作模式的行为特征，也可以进行粗粒度的切片计算，即从整个规格说明 中提取这个操作模式以及与其相关的模式和变量等，也就是只进行分层切片中 的系统层和类层的切片计算。因此，动画模拟的范围明显缩小，降低了整个过 程的复杂性，提高了动画模拟的效率。 2 3 实例研究 图2 3b i r t h d a y 系统的o b j e e t - z 规格说明 1 2 上海大学硕士学位论文 ! 堕堕! 堡坠望! 竺! ! 堕堕堕! 坠堕里坠! 坚塑坚墅坠 图2 3 是一个b i r t h d a y 系统( b b 表示这个类的状态模式) ，这个系统包括 三个类，其中类b i r t h d a y b o o k 是类c h i l d b i r t h d a y 和a d u l t b i r t h d a y 的父类，类 c h i l d b i r t h d a y 和a d u l t b i r t h d a y 分别表示孩子和成人。下面我们以这个规格说明 为例求它的关于切片标准 的切片，按上文提出的规格说明的分层 切片方法分以下步骤进行： 1 ) 系统层：确定包含谓词p 4 和变量b i r t h d a y 的类是b i r t h d a y b o o k n a m e ， d a t e 】，建立系统层依赖图( s h d g ) 见图2 4 ( a ) 。因为在系统中类 c h i l d b i r t h d a y 和a d u l t b i r t h d a y 依赖于类b i r t h d a y b o o k ，根据以上介绍的 方法关于切片标准 在系统层的切片s o ) 1 = ( b i r t h d a y b o o k n a m e ，d a t e ) ( 见图2 4 ( b ) ) ，显然s ( p ) o ：s ( p ) 1 成立。 ( a ) 切片前 切片后 图2 4b i r t h d a y 系统的系统层依赖t 羽( s h d g ) 2 ) 类层：把类b i r t h d a y b o o k n a m e ，d a t e 】展开，建立类层依赖图 ( c h d g ) ( 见图2 5 ( a ) ) 。确定包含i w i i - j p 4 和变量b i 曲d a y 的模式是a d d ， 由图2 5 可看出模式a d d 只依赖于模式b b 。因此s ( p ) 2 = b b ，a d d ( 见 图2 5 ) 。 ( a ) 切片前 ( b ) 切片后 图2 5 b i r t h d a y 系统的类层依赖i 虱( c h d g ) 3 ) 模式层：按照程序依赖i 翌i ( p d g ) 的构造方法把图2 5 ( b ) 中的模式b b 和 a d d 分别展开，建立包含这两个模式的模式层依赖图( s h d g ) ( 见图2 6 ) 。 上海大学硕士学位论文 t h ep o s t g r a d u a t et h e s | so fs h a n g h a lu n l v e p s i t y 利用两阶段图可达性算法计算模式层依赖图的切片s ( p ) 3 = k n o w n ， b i r t h d a y ，b i r t h d a y ，n a m e ? ，d a t e ? ，d 2 ，p l ，p 3 ，p 4 ) ( 见图2 7 ) ，显 然s ( p ) o ：s ( p ) 1 ：s ( p ) 2 ) s ( p ) 3 成立。 图2 6b i r t h d a y 系统的模式层依赖图( s h d g ) 1 4 上海大学硕士学位论文 t h ep c , s t