（计算机软件与理论专业论文）z规格说明中集合论算子的自动求精研究及实现.pdf

沈阳工业大学硕士学位论文 摘要 采用自然语言描述的非形式的规格说明通常具有模糊性和歧义性，这往往不利于软 件质量和生产率的提高。为了克服自然语言描述规格说明的缺陷，人们提出了形式化方 法。z 是目前最为流行的一种形式规格说明语言，但就总体而言，z 规格说明的理论和 技术尚未达到可以在工业界广泛应用的程度。人们提出了z 规格说明到高级语言自动求 精的思想，但其实现却进展缓慢。基于以上原因，以自动求精的实现为目的，为研制一 套完整的编译环境，使其可以将z 规格说明自动转化为可编译的高级程序设计语言，本 课题研究了集合论算子的自动求精。 研究工作主要包含以下几方面内容：研究了z 规格说明的数据类型以及各类型之间 的关系：以z 的自动求精为目的，提出了用s t l 中的不同容器表示z 规格说明各数据 类型的思想；利用c h 及s t l 技术设计了z 中集合、关系、包、序列等数据类型的求 精规则：结合c 十+ 语言的模板、重载技术和s t l 模板库对数据结构和通用算法的强大支 持功能，为集合论中各操作算予到c 抖代码自动求精提供了相应的函数模板，制定了集 合论各算子的求精规则。 以上述研究工作为基础，设计了2 t o c 自动求精器，主要工作内容有：设计自动求 精处理过程的符号表；对于z 规格说明进行了词法分析；对于修改后的s m a r tz 设计语 法规则并采用自顶向下方法进行了语法分析，并给出相应出错处理；语义分析阶段主要 处理静态语义检查及更新符号表的信息；目标代码生成阶段根据语义分析的信息、符号 表的信息以及集合论算子的求精规则产生目标程序，即c + + 程序代码。 z 到高级语言自动求精的研究与设计对于形式化方法及形式规格说明应用于软件开 发的各个阶段具有非常重要的意义：确保了从需求分析阶段开始的软件开发周期的完全 形式化：避免了人工的误操作或演算错误导致的求精前后不一致，保证了系统的一致性 和完整性；由于求精过程避免了手工操作，因而z 规格说明自动精化为程序代码的编译 环境可以建立，这将会加速z 规格说明在工业界的推广应用。 关键词：z 规格说明，s t l ，集合论算子，自动求精，z t o c 自动求精器 沈阳工业大学硕士学位论文 s e tt h e o r yo p e r a t o ra u t o m a t i cr e f i n e m e n tr e s e a r c ha n d i m p l e m e n t a t i o ni nzs p e c i f i c a t i o n a b s t r a c t i ti sf r e q u e n t l yd i 韶d 、碰i 哮o l l st ot h ei m p r o v e m e n to fs o f t w a r eq u a l i t ya n dp r o d u c t i v i t y t h a ti n f o r m a ls p e c i f i c a t i o nd i s c r i b e db ym 咖r el a n g u a g ef 北q u e n u yi so b s c u r ea n dd i v e r g e n t f o r m a lm e t h o dw a sp r e f e r r e di no r d e rt oo v e r r i d ed e f i e i e n c yo fs p e c i f i c a t i o nd i s c r i b e db y 0 2 t r l r el a n g u a g e zi sp r e s e n t l yt h em o s tf a s h i o n a b l ef o r m a ls p e c i f i c a t i o n b u ta saw h o l e , t h e t h e o r ya n dt e c h n o l o g yo fzs p e c i f i c a t i o ni s n te x t e n s i v e l ya p p l i e di ni n d u s t r yf i e l d s o ，t h e t h e o r yo f a u t o m a t i cr e f i n e m e n tf r o mzs p e c i f i c a t i o nt oh i g hl a n g u a g ei sp r e f e r r e d h o w e v e r , i t s r e a l i z a t i o nm a k e ss l o wp r o g r e s s t h e r e f o r e ，t h i ss u b j e c ts t u d i e sa u t o m a t i cr e f i n e m e n to fs e t t h e o r yo p e r a t o ri no r d e rt od e v e l o pae n t i r ec o m p i l e rw h i c hc a nm a k eac o n v e r to fz s p e c i f i c a t i o nt oc o m p i l e dh i g h - l e v e lp r o g r a m m el a n g u a g e a tf i r s t , t h es u b j e c tm a i n l yd i s c u s s e sf o l l o w i n ga s p e c t s ：f i r s t , s t u d yzs p e c i f i c a t i o nd a t a t y p e sa n dr e l a t i o n s h i pa m o n gd a t at y p e s ；s e c o n d , p r e f e rt h et h o u g h tt h a tu s i n gc o n t a i n e r si n s t l e x p r e s szs p e c i f i 钮f i o nd a t at y p e si no r d e rt os t u d ya u t o m a t i cr e f i n e m e n t ；t h i r d , d e s i g nt h e r e f i n e m e n tr u l eo fs e t , r e f e r e n c e b a g , s e q u e n c ee t cd a t at y p e si nzu s i n gc + + a n ds t l t e c h n o l o g y ；f o u r t h o f f e rf u n c t i o nt e m p l a t ef o ra u t o m a t i cr e f i n e m e n tf r o mo p e r a t 。o r si ns e t t h e o r yt oc 抖c o d ea n dm a k e sr e f i n e m e n tr u l eo f o p e r a t o ri ns e tt h e o r yb yt e m p l a t et e c h n o l o g y i i lc + + l a n g u a g ea n ds t l t e m p l a t el i b r a r ys u p p o r t i n gd a t ac o n s t r u c t i o na n dg e n e m la l g o r i t h m t h e n , b a s i n g o na b o v es t u d y ，d e s i g nz t o ca u t o m a t i cr e f i n e r s t u d yi n c l u d e s ：f i r s t , d e s i g n t h es y m b o lt a b l ei na u t o m a t i cr e f i n e m e n th 锄d l i n gp r o c e s s ；s e c o n d , p m c c c dl e x i c a la n a l y s i so f zs p e c i f i c a t i o n ；t h i r d , d e s i g ng r a m m a rr u l e 妇s m a r tzm o d i f i e da n dp r o c e e dg r a m m a r a n a l y s i sb yt o p - d o w np a r s i n g , a n dg i v ee l i o rd e a l i n g ；f o u r t h , i ns t a g eo fs e m a n t i c sa n a l y s i s p r o c e e ds t a t i cs 跚l a i l t i c sc h e c k i n ga n dr e f r e s ht h ei n f o r m a t i o ni ns y m b o lt a b l e ；f i r kg e n e r a t e t a r g e ti r r o g r a r n m e ( c + + = c o d e ) i na c c o r d i n gt ot h ei n f o r m a t i o ni na n a l y s i so fs e m a n t i c sa n d s y m b o lt a b l e ，a sw e l la st h er e f i n e m e n tr u l eo f s e tt h e o r yo p e r a t o ri ng e n e r a t i n gt a r g e tc o d es t a g e i ti si m p o r t a n tf o rt h ea p p l i c a t i o no f f o r m a la p p r o a c ha n df o r m a ls p e c i f i c a t i o ni na l ls t a g e s o fs o l t w a r ed e v e l o p m e n tt os t u d ya n dd e s i g na u t o m a t i cr e f i n e m e n tf r o mzt o h i g h - l e v e l 2 沈阳工业大学硕士学位论文 l a n g u a g e ：i n s u r ec o m p l e t ef o r m a l i z n f i o ni na l ls t a g e so fs o f t w a r ed e v e l o p m e n t ；a v o i da n f i l o g y i nr e f i n e m e n td u et om i s t a k e no p e r a t i o no re o m p u t a t i v em i s t a k ea n di n s u r ec o n s i s t e n c ya n d i n t e g r i t yo fs y s t e m ；d u et oa v o i d i n gm a n u a lo p e r a t i o ni nr e f i n e m e n tp i x ) c e s s ，i ti sf e a s i b l et o b u l i dac o m p i l ee n v i r o n m e n tt h a tzs p e c i f i c a t i o na u t o m a t i cr e f i n ea n df o r mh i g h - l e v e l p r o g r a m m e ，t h i s w i l la c c e l e r a t e t h e p r o m o t i o n a n d a p p l i c a t i o n o f z i n i n d u s t r y k e yw o r d s ：zs p e c i f i c a t i o n , s t l ，s e tt h e o r yo p e r a t o r , a u t o m a t i cr e f i n e m e n t ，z t o c a u t o m a t i cr e f i n e r 3 一 独创性说明 本人郑重声明：所呈交的论文是我个人在导师指导下进行的研究工 作及取得的研究成果。尽我所知，除了文中特别加以标注和致谢的地方 外，论文中不包含其他人已经发表或撰写的研究成果，也不包含为获得 沈阳工业大学或其他教育机构的学位或证书所使用过的材料。与我一同 工作的同志对本研究所做的任何贡献均己在论文中做了明确的说明并表 示了谢意。 签名：耋蕴之鲶日期：竺堂- 聋! 璺! ! 日 关于论文使用授权的说明 本人完全了解沈阳工业大学有关保留、使用学位论文的规定，即： 学校有权保留送交论文的复印件，允许论文被查阅和借阅；学校可以公 布论文的全部或部分内容，可以采用影印、缩印或其他复制手段保存论 文。 ( 保密的论文在解密后应遵循此规定) 日期：盏! 主盘! 国i f 目 沈阳王业大学颈士学救澹文 i 绪论 1 1 研究背景 软件开发的过程楚从对魇户的嚣求进行分析舞始，经过设计和实现，最臌产生可以 正确执行的代码以及有必使雳和维护麴各种文档。宽成这个过程静方法称为软件开发方 法【l 】。 传统蛉软彳牛开发方法引入一些 形式的图形魏文字符号，提供一定的设计原则，协 助开发入爨按照一定的步骤，沈较嘲确和简练遗 毒碍设计文档，爝人工方式开发出所要 的软件。从各软件加工模型来看，用户需求的规格说明在软件开发过程中具脊a # 常重要 的地位。茭使用者包捂瘸户、系统分板员、设诗与绫程人员、测试毒珏验收人员。 诲多软件项目开发豹经验表蹲，软件开发费愆的大部分是髑于纠正在镬试阶段所发 现的各种错误。而更详细的调查告诫我们，这些错误中的很大一部分可追溯到项目的早 翅阶段，朝在实现耱镤试除段所花的凑颧费鼹是囊予需求分析秘设计酚段纛啜夔“节 省”所弓| 熬豹。需求分轿阶段的错误邋常就是规格说明酶描述不精确。 1 1 1 形式化方法 众蘑躅懿，采雳鑫然语言描述熬l 形式夔援糁落爨具有易读、易理纂我侠点，僵它 通常具有模糊性和鼓义能( - - 义性) ，经常是不精确和不完整的。这往往引越规格说明 的使用者对同一规格说明产生不同的理解，最终导致用户对已兜成的系统不满意。另 步 ，传统瓣开发方法由予聚震不严穆熬l 形式技恭箍述嚣据款转系统豹援掇说瞩，嚣 此超很难襻酗计算机的谢效支持，显然，这不利于软件质量和生产率的提高。 提高软件生产率的根本途径之一是软件开发过稷的自动化技术【2 】，另外，实现软件 秀发过程嚣除段豹垂动健瞧是款终工爨潍戆重要嚣豁之一。软磐爨魂毒乏数裁撬蹩形式忿 州，即以一种精确的方法严格地描述软件系统的定义和需求，并殿这种精确的表述方法 是建立在严格的数学基础上的；它通过集合、谓词逻辑、函数映射等数学方法，保证软 终系统从魏疆谖暖至g 代秘生成每一除段鹭毒一次影式交换帮畜严络靛数学摆溪秘正确莲 证明，从而保证其语义不变。 淀弼工堑大学醺圭学位论文 形式化方法的研究鞠应用己有3 0 多年的历史。最初的产生怒由d 电k s 毗秘h o m e 在 程序验谨方瑟的工俸秘s 牲，s t r a t c h e yl 冀及箕穗学者在程净语义方面静工佟基础上发 展起来的。形式化方法p “、7 】( f o r m a lm e t h o d s ) 怒一种新的软件开发范型，即通过形式 优、规范傀的数学理论，惩描述“傲传么”来取代“怎么做”。其基本思想是对系统建 立一个数擎模型，研究釉提供一种蘩予数学的或形式语义学静麓格说瞬语言，精这种语 言严格地描述所开发的软件功能，并豳自动程序设计的加工模型来得到可执行的代码。 形式能方法的优越之处在于它具蠢严格的数学蒸醚与描述性，在软 牛开发戆过程孛 使用形式纯方法具有下捌优点： ( 1 ) 形式规格说明是精确的； ( 2 盎误鼷弓l 惹熬绩误减少： ( 3 ) 形式规格说明利于系统实现； ( 4 )能够对形式规格说明进行溅确性证明。 软馋形式短格说明憝形式诧方法袋摹本戆部努，它耪礁遵攒逑了震户鲍鬟求、较终 系统的功能和各种性疑。形式忧方法的规格说明舆有良好的数学簇础，易手研究软件规 格说明性质，如规格说明的一致性、究备性以及规格说明间的等价l 生等，便于机器的自 稳处理。瓣 形式纯方法麴怒捂说明爨然在警写、壤惩帮使震上窍其独至l 黪俊点，虽逶 于描述软件需求规格说明，但其缺陷也是很明显的，那就是语义的歧义性和攒述的不完 备性对予较件的自动化增加的重重障碍。 1 1 2 形式嫒辫漉臻 。 形式他较件规格说辨不仅是对用户需求，也是对软件系统的严格定义，农软件开发 书布者相尚藿要的作用。另一方面，为了提高软件生产率，便于从软件规格说明自动或 i 蔓t ：，l 黉半黉确蟪导警正臻鹣程黪，对较馋麓楱说明语富矮应遮挺出了凝豹霉求，秘要袋它不 蔹要憨适龠撼述夫型软件，便于用户使用，利于软件产品的可靠性，而且还簧有利于机 器的自动处理。因此，将形式化的理论和方法用于需求分析与规格说明极为必要，也是 实魂软俸貊囊秽生产酶聚搴兹疆。 由于软件规格说明的重要性，因际上对软件规格说明方法和软件规格说明语言进行 了广泛的研究。z 是目前疑为流行的一种规格说明方法。它是7 0 年代末至8 0 年代初由 沈阳工业犬学硕上学位论文 英国o x f o r d 大学程序研究组v r g - ( p r o g r a m m i n gr e s e a r c hg r o u p ) 设计的。它采用了严格 的数学理论，可以产生简明、精确、无歧义且可证明的规格说明。z t 9 1 是一种具有“状 态操作”风格的形式化规格语言，它以一阶谓词逻辑和集合论为基础，利用集合、关 系、函数、序列和包等数学概念，使用状态模式和操作模式对目标系统的状态和操作进 行说明。z 语言在学术界得到了广泛的应用，常被称作是“软件工程”语言。 除z 之外，还有其他很多规格说明语言，例如：v d m 1 0 】、o b j 、l o t o s 、l a r c h 、 t r a c e 、g l i d e 、a d t s 。不同的规格说明语言在表达能力、术语、准确性以及支持形式 处理的能力方面有所不同，每种语言的侧重点也不同，针对所产生的背景而设计其特 性。同其他规格说明语言相比，z 语言一个主要的特点是可以对z 进行推理和证明，这 种特点使软件开发人员或用户能够很快找出规格说明的不一致、不完整之处，尽量避免 测试阶段才发现需求分析阶段的错误。 不过，就总体而言，形式规格说明的理论和技术尚未达到可以在工业界广泛应用的 程度，然而，形式规格说明的缺陷正逐步被克服，随着形式化方法研究的深入和支撑工 具的增加，许多具体的形式化方法研究中所提出( 或出现) 的技术在实践中正被广泛采 用，形式规格说明在工业界推广应用的可能性也在逐步增加。 1 2 研究意义 1 2 1 自动求精思想的提出 到目前为止，z 规格说明的支撑工具虽然很多，但就总体而言，形式规格说明的理 论和技术尚未达到可以在工业界广泛应用的程度，特别是对于大规模软件系统的设计更 是如此。形式规格说明抽象、难懂固然是原因之一，然而更重要的原因是z 不是一种实 现级语言，无法直接得到可执行程序，因而无法应用于软件生命周期的所有阶段。大量 工作仅限于文法及类型检查、定义域检查和定理证明方面，主要应用于需求分析阶段及 测试】阶段。如果有一种工具可以突破单纯的类型检查及测试阶段，将计算机不能识别 的z 规格说明自动转化为可编译的高级程序设计语言或计算机可识别的代码，形式规格 说明将会迅速地在工业界推广应用。基于z 研究发展中的这一问题，一些学者提出z 规 格说明到高级语言自动转换【l2 】的设想。 沈阳工业人学硕士学位论文 其实，将z 规格说明转换成高级语言属于软件求精范畴。软件求精1 3 1 是指从目标软 件系统的规格说明出发，经过一系列的步骤，每一步都增加一些可执行性，或是增加一 些执行效率，最终达到执行效率高的程序代码的演化过程。i i 前关于软件求精已经有很 多研究，但多是由人工完成或通过人机交互来完成，自动求精思想的提出，对于形式化 方法及形式规格说明应用于软件开发的各个阶段具有非常重要的意义： ( 1 ) 求精具有机械性。提出套完整的规则实现z 到高级语言的自动求精，可以 确保从需求分析阶段开始的软件开发周期的完全形式化，将形式化方法统一地应用于软 件开发的各个阶段。 ( 2 ) 避免人工的误操作或演算错误导致的求精前后不一致，保证了系统的一致性 和完整性。 ( 3 ) 求精过程避免了手工操作，z 规格说明自动精化为程序代码的编译环境可以 建立，这将会加速z 规格说明在工业界的推广应用。 1 2 2 课题的提出 由于z 是基于一阶逻辑和集合论【1 川的规格说明语言，实现一阶逻辑算子的自动求精 和集合论算子的自动求精成为z 规格说明语言自动求精的基础。 对于集合论算子，有大量的研究工作需要进行。z 中有8 0 余种常用符号，其中含 有大量的集合及集合运算、关系及关系运算、函数及函数操作。z 还引入了新的数据类 型：序列和包。求精过程中，这些数据类型及其中的大量算子需要转换为高级语言的数 据结构【煳。 除了算子的求精工作，还需考虑算法的实现。算法是对特定问题求解步骤的一种描 述，它是指令的有限序列，其中每一条指令表示一个或多个操作。设计算法时不仅要满 足算法的特性( 有穷性、确定性、可行性、输入和输出) ，还要尽量优化以期达到最 优，即保证算法的正确性、可读性、健壮性、效率与低存储量需求。 基于以上背景研究，特提出该课题：z 规格说明中集合论算子的自动求精研究及实 现。 沈阳工业大学硕士学位论文 2 叶s t l 由于z 规格说明基于集合论和一阶逻辑，而c + + s 1 l 具有v e c t o r 、s e t 、m a p 等高效 的容器用来表示集合、向量等结构，并且相应的操作非常完善，就此提出采用c + + s t l 的相应容器表示z 中的各数据类型，z 中的集合操作( 即集合论算子) 可用s t l 相应 的算法实现。 c + + s t l 不仅通用性好，而且安全机制完善，可以支持集合、序列、包等操作，将 一个软件系统视为抽象数据类型集合，可由机器进行从z 规格说明到c + + s t l 的自动 转换f 16 】。 2 1s t l 简介 s t l 1 7 1 ( s t a n d a r dt e m p l a t el i b r a r y ，标准模板库) 是一个c + + 通用库。从根本上 说，s t l 是一些“容器”的集合，这些“容器”有f i s t 、v e c t o r 、s e t 、m a p 等，此外， s t l 也是算法、迭代器和其他一些组件的集合。由于模板库相对于传统的由函数和类组 成的库来说，可以提供更好的代码重用，而且s t l 中的代码是采用模板类及模板函数 的方式，因此可以极大地提高编程效率。 s t l 技术是对原来的c + + 技术的一种补充，相对于c + + 语言而言，具有以下优点： ( 1 ) 具有非常优秀的通用性； ( 2 ) 具有无法比拟的高效性； ( 3 ) 数据结构非常简单，非常容易被程序员所掌握； ( 4 ) 安全机制完善，内存管理非常优秀。 2 2s t l 基本结构 s t l ( s t a n d a r dt e m p l a t el i b r a r y ) 由迭代器( i t e r a t o r s ) 、算法( a l g o r i t h m s ) 、容 器( c o n t a i n e r s ) 、函数对象( f u n c t i o no b j e c t s ) 和内存分配器( a l l o c a t o r s ) 五大部分组 成。下面主要介绍与本课题密切相关的部分：容器、算法和迭代器，其他部分可参考文 献 1 7 】。 沈阳工业大学硕士学位论文 2 2 1 容器( c o n m m e 巧) 和许多标准类库一样，s t l 主要包含容器类【1 8 1 ，容器类是可以包含其他对象的类， 就像数组、队列、堆栈等数据结构可以包含整数、小数、类等数据成员一样，s t l 包含 常见的向量类( v e c t o r ) 、链表类( d e q u e ) 、双向队列类( h s t ) 、集合类( s e t 和 m l l l f i s e t ) 和图类( m a p 和m f l f i m a p ) 等，它们中的每个类都是一种模板，并且这些模 板可以包含各种类型的对象。 s t l 提供的容器可以分成两大类：序列式容器( s e q u e n c ec o n t a i n e r s ) 和关联式容 器( a s s o c i a t es e q u c n c ec o n t a i n e r s ) 。表2 1 简单地介绍了s t l 各容器及其特点： 表2 1 标准库容器类 ( 1 ) 序列式容器。c + + 标准模板库提供三种序列式容器：v e c t o r 、l i s t 和d e q u e 。其 中v 。呦r 类和d e q u e 类是基于数组的，而h s t 类实现链表数据结构。 1 ) v e c t o r 对象是s t l 提供的最简单，也是最常用的容器类模板之一。它与数组之 间的相似性在于提供了对序列中的元素进行随机访问，但与传统的数组不同之处在于， v e c t o r 对象在运行时可以动态改变自身的大小以便容纳任何数目的元素。它提供了对数 沈潮工业 簿硕士掌链论文 组元素的快速、随枫访润，以及在序列尾部快速、随机的插入秘溅除操作。当然，它也 支持在序确中静其袍遗方插入和删除元素，但是效率会有所降低。 2 ) d e q u e 是一种双端队列容器，究成了标准的c + + 数据结构中队列的所脊功能。不 论在尾郝娥头熬插入元豢，都十分迅遮。在中间郝分捶八元素艇 e 较费时，因为必须移 动其铯元豢。这是一种麓枫访阔靛数攥类型，据供了在序歹日两端快速插入和删除操作的 功能，它w 以在需要的时候修改其自身大小。 3 ) l i s t 是一个双肉链表客器，完戚了标准躲c 数据结梅孛链表的所有凌貔。l i s t 与v e c t o r 和d 踟酹类戗，只不过其中的对象提供了对元素的随机访问。它不支持随机访 问的数组类型，访问链寝元素要指针从链表的某个端点开始。l i 毗对象在序列中的任何 位置放饕弱测除元素都楚蘸效静，与该元素在链表中妁位置无关。 ( 2 ) 关联式容器。s t l 关联式容器能通过关键字( 也称查拽字，s e a e h k e y ) 直接 访问从而存储和读取元豢。这四个关联容器是m u l t i s e t 、s e t 、m u l f i m a p 和m a p 。m u l t i s e t 积s e t 类掇供t 控嚣数镳潞黥操终，其中数篷楚关键字，露苓必雯鸯一令篷与每个关 键字相关联。m u l t i m a p 和m a p 类提供了操作与每个灏键字相关联的值的方法( 这些值 也称为映射值，m a p p e dv a l u e ) 。 i l ) s e t 是一秘笾橇京取羲容器，篡关键字纛数据元素是嚣一令焦。瞅辩象中兹瑟 有元素必须具有唯一值，也就是说它不能包含重复的元素。s e t 对象可以使程序按照次 序来存储一组数值。在一个集合中，元素既作为被存储的数据又作为数据的关键值。本 覆上一令黎会蘸缳一令蠢亭兹接列。 2 ) m u l t i s e t 与s e t 炭似，多重集合的元素既作为被存储的数据又作为数据的关键 值。与s e t 不同的是，窀可以包含重复的元素。 3 ) m a p 是一耪惫蛮残霹鼗援懿容器。其孛一拿篷是实嚣数据篷，舅争 一令是曩寒 寻找数据的关键值，一个特定的关键词只能与一个元素相联系。m a p 是由一对一对的键 值( k e y v a l u e ) 所组成的排序结构体，键值独一无二。 4 ) m 蠛f i m a p 是一静龛海密瑰羹麓关键篷鹣关联鼗缝窖嚣，然露与m a p 对象不曩， 它的一个笑键词可以与痧个元素相联系，m u l i m a p 允许键值重复。m u l t i m a p 与m a p 的关 系完全等闲于m u l t i s e t 与鳅的关系。 沈阳工业大学硕士学位论文 2 2 2 算法( a l g o r i t h m s ) s t l 提供了非常多的数据结构算法，可以巧妙地处理储存在容器中的数据。这些算 法在命名空间( n a m e s p a c e ) s t d 的范围内定义。下面列出应用于本课题的部分算法： f i n d 0 ，其功能是查找第一个能与引数匹配的元素。 c o t m t 0 ，其功能是计算元素出现的次数。 r e p l a c e ( ) ，其功能是用新的值替换元素。 c o p y ( ) ，其功能是复制( 拷贝) 元素。 s o r t 0 ，其功能是对元素排序。 e q u a l _ r a n g e 0 ，其功能是查找所有元素值相等的元素。 m e r g e ( ) ，其功能是合并有序的序列。 上述这些算法以及标准程序库中其他算法都可以应用于标准容器、字符串类和内建 数组。s t l 技术的一个灵活且优秀的措施是拥有大量的功能极强大运用灵活的算法，所 有这些算法都是基于函数模板实现的。对于这些算法在本课题中的具体应用，可参见附 录b 。 2 2 3 迭代器( i t e r a t o r s ) 无论从何种意义上来说，都可以认为迭代器就是一个指示器，然而，迭代器技术能 够使程序反复的对s t l 容器的内容进行访问，所以非常快捷和重要。对容器的内容进 行反复地访问，意味着一次就可以访问一个或多个元素。迭代器为访问容器提供了通用 的方法，类似于c + + 的指针。并且，迭代器保存所操作的特定容器需要的状态信息，从 而实现与每种容器类型相适应的迭代器，以上所讲述的序列式容器和关联式容器都支持 迭代器，并可以用迭代器遍历。 大多容器提供成员函数b e g i n 0 和e n d ( ) 。函数b e g i n 0 返回指向容器第一个元素的迭 代器，函数e n d 0 返回指向容器最后一个元素后面一位的迭代器( 是个不存在的元 素) 。如果迭代器i 指向特定元素，则+ + i 指向下一个元素，i 指向i 所指的元素。 i t e r a t o r 类型的对象指可以修改的容器元素，c o r l s ti t e r a t o r 类型的对象所指的是不可以修 改的容器元素。在集合论算子的自动求精中最常用到的是i t e r a t o r 类型( 见附录b ) 。 沈n _ t j i k 大学硕上学位论文 3 z 朔髂说明 3 1 研究动态 z 规格说明中的z 指著名数学家z e r m o l o ，他的主要成就是集合论，z t l 9 2 0 是基于 集合论和一阶谓词逻辑的软件形式规格说明语言。z 采用了严格的数学理论，可以产生 简明、精确、无歧义且可证明的规格说明，是一种具有“状态操作”风格的形式化规 格语言。z 以一阶谓词逻辑和集合论为基础，利用集合、关系、函数、序列和包等数学 概念，使用状态模式和操作模式对目标系统的状态和操作进行说明。z 的基本单位是 s c h e m a ，一个系统由若干个s c h e m a 组成，s c h e m a 可以用来描述类型、系统状态、操作 等。 将z 称为规格说明语言的关键思想是把软件开发中的需求规格说明阶段和软件设计 阶段分开。它不同于高级程序设计语言，没有顺序，选择，循环语句。在需求规格说明 阶段精确地描述软件“做什么”，而不涉及“怎么做”。编写规格说明与编写计算机程 序的不同之处在于规格说明是对目标软件系统的功能描述，而计算机程序口1 1 则是实现目 标软件系统功能的过程描述。 近二十年来，美国、加拿大、日本、澳大利亚、以及欧洲的一些国家尤其是英国， 对z 进行了深入的研究和开发。迄今为止，z 仍然是一种不可运行的强类型的规格说明 语言，尽管在z 的执行方面，人们已经做了不少研究工作，但目前仍缺乏可用的z 语 言编译工具。不过，在z 规格说明的检查方面已有了许多性能不错的工具，例如：美国 d ep a u l 大学研制的z t c 及英国y o r k 大学设计的c a d i z t 2 2 1 都是比较实用的z 规格说明 的类型检查工具，这些工具能够保证z 规格说明的语法及类型的正确性。以下是z 规 格说明的其他支撑工具：a l c o a 、c o g i t o 、f o r m a l i s e rzt y p e c h e c k e r 、h o lm e c h a n i c a l t h e o r e mp r o v i n gs y s t e m ，h i p p o ，h o l - z ，j a p e ，j a z a a n i m a t o r ，l a t h i a s ，m a t h s p r o j e c tzs y n t a x 、m o b y o z ，n i t p i c k ，o o z e ，p i z a 、p o s s u m 、p r e c czg r a m l n a r 、 p r o o f p o w e r l 2 3 、r 0 7 , 、- r o z e l i n k 、w i z a r d 、z 2 h t m lt r a n s l a t o r 、z e t a 、z a s t 、z b r o w e r 、z e u s 、z 恒v e s 刚、z o l a 。 沈鞲； ：叠匏大学硕士攀傲论文 3 2z 规格说明酶类型 z 的一个重要的耨锻就是类型亿，即z 是一个炎婆 纯的语害。类型系统癸求，在z 中，任何一个新的变量在被使用以前必须以一个类溅声明之，类型决定了变量可取值的 范围。藤髓，不仅变量蠢类型，每一令表达式，妻蟊袋会等也一定蠢一个类型。z 戆类型 是一个给怒集合盼名字，或是由简单的类型使用个或多个类羹构造符构造如来的复合 类型。基本类型是z 的炎型系统的重骚组成部分，对基本类型羹复使用类型构造符，可 梅造出萁锻麴幂集类型、笛专尔积类熬、枣到、龟簿复合类型。 3 2 1 基本类型 每一个z 规格说明都引入并使用了基本类型( b a s i ct y p e ) 。这些基本类型有时被称 秀绘定集合( g i v e ns e t s ) ，霹交一辩方疆号摇起寒瓣名溪缝藏的蘩本类型定义萼l 入。基 本类型定义就是一个类溅声明，它引入一个或多个基本类型。如 b o o k 、c a r 引入了 基本类型b o o k 和c a r 。通常对这些集合的内部结构荠不关心，感兴趣的是一个规格说 瞬弓 入德销骧轰裁有了诞镬露静类蘩，瞧 霹殴禹这魉类型寒声骥变量。 还要绘出的一个重灏的基本类型怒整数类型，它表示为z 。蒸本类型z 怒内定义类 型，不需鞭声明。 教举类整邀霾予基零类墼，毽与蒸零类鍪定义蕊不嚣静是，教举类型定义霹已蔑定 好该类型熙有的元素个数，并已对这几个元素给定名称。 3 2 2 复合赞型 ( 1 ) 幂集类型。傻震一令筑稳溪饔中弱基零炎蘩窝幂集稳逡祷；裁可渡产望一令 新的类型，称为该基本类型的幂集类烈。设a 是一个集合，由a 的所有子鬃所组成的 集合，称为集合a 的幂集，记作pa 。如果一个规格说明有基本类型s 和t ，则ps 和 pt 都蹩会法豹类鼙。酝褥其有稳弱瓷囊羊静怼象缀戎装集会零爨藏跫集会类整pt 戆 对象。 ( 2 ) 篱卡尔积粪型。笛卡尔积楚集合论中的慕本概念之一，在z 规格说明中，笛 “ 卡尔舔馋海类鍪鞠造餐，囊基翘戆类黧镌造窭薪熬炎鍪。绘定任露嚣令集合袋窝s ，萁 笛卡尔积r xs 是所有这样的序偶的黛合，这些序偶的第一个元索是r 中的一个元素， 其第二个元索是s 中的一个元素。笛卡尔积还可定义子三个或更多的集合。例如三个集 沈阳工业人学硕士学位论文 合r ，s 和t 的笛卡尔积r x s t 含有所有的有序的三元组的集合，第一个元素来自 r ，第二个元素来自s ，而第三个元素来自t 。 1 ) 关系。关系是一个多对多的映射，两个集合之间的关系称为二元关系。二元关 系是使用最广泛的关系，为了方便，简称为关系。两个集合x 和y 的一个关系r 是笛 卡尔积x y 的子集，也就是说，r 曼x x y ，故称关系是序偶的集合。在定义二元关 系的时候，需要声明该关系所关联的两个元素所属的集合，这两个集合分别被称为源集 ( s o u r c es e t ) 和目标集( t a r g e ts e t ) ，有时候源集和i f l 标集是同一集合。关系的定义域 ( d o m a i n ) 是关系源集的一个子集，关系的值域( r a n g e ) 是关系目标集的一个子集。 2 ) 函数。函数是一个大家较熟悉的概念，在数学中通常函数y - - f ( x ) 定义在实数 集合上，现在把函数的概念推广，函数是一种特殊的关系。对于函数，其定义域中的任 一元素只能映射到其值域中的一个元素。函数的性质可以形式地描述为： 设r 是一个类型为x 书- + y 的关系，则( x “y ) e r 八( x z ) e r - y = z 一般函数是部分函数，定义域与源集相同的函数称为全函数。在z 中还有几种特殊 的函数，它们是入射函数、满射函数和双射函数。 3 ) 序列。序列用来描述有序的数据对象的集合。在一个序列中，元素出现的次序 是有意义的，而且每个元素又可以出现多次，一个序列可以用一对尖括号来表示。例 如： 该序列有三个元素，与集合不同的是，序列中出现的元素是有次序的。所以有 用特殊的记号s e qx 来表示由集合x 的元素产生的所有序列的类型。即s e qx 是一 个类型，用它来声明的对象是一个序列，序列中的元素是集合x 中的元素。 4 ) 包。包用来描述元素在集合中出现以及出现的次数。一个对象的包与集合类似 的是，元素出现的次序是无关紧要的。包与集合不同的是，每一个对象出现的次数是重 要的。用b a gx 来表7 - m 3 e 合x 的元素的所有包的类型。在z 中，包是一个从包的元素 到正整数的函数，因此可有下述定义：b a gp e r s o n p e r s o n * n 一个包可以用一对方括号来表示。例如： 沈辩工整大学颈主学缎论文 l m n g ，l i i 】m n g ，w a n g g a n g ，胁a i l 出o n g ，z h a n g h o n g ，z h a n g h o n g 】 在这个包中，l i m i n g 密瑗了2 次，w 翻t g g a n g 爨现了1 次，z t m n g 赫n g 遗溪了3 次。上面的包实际上就怒函数： l i m i n gh2 ，w a n g g a n gh1 ，z l m n g h o n g 3 ) 以上怒z 规格说明姻所有类型，释类型及其之间的关系可以概括如图3 1 所示： 3 3z 规格说明的构造单元 黼3 1 z 规格说明姻类型 3 3 1 z 的犄号 标谈德是z 螽格诞绢中最楚莘豹语法攀位。z 除了含有一般豹程序设计谬言中誊箱 的a s c i i 码符号外，还禽有其他专用的数学符号，这些数学符号戚是运算符，或是具有 沈阳工业大学硕士学位论文 特殊含义的符号，如p 、n 、n l 、f 、z 等。z 的标准的运算符分为前缀、中缀和后缀三 种形式( 见附录a ) 。 由于z 规格说明并非作为一种直接由计算机处理的语言而设计的，在z 的符号集 中，许多符号都没有对应的键盘符，此现象成了计算机处理z 规格说明的障碍。结构化 规格说明语言z s 为这些符号设计了对应的键盘符或保留字，z s 不但易于记忆，且输 入方便、减少出错，为形式规格说明到高级语言的自动转换打下了基础。此外，对于规 格说明语言z 的各种框架结构，如公理化定义、模式等，在z s 语言中都设计了对应的 文本表示形式，其体内容参见文献 2 5 】。 3 3 2 模式 模式是用来书写形式规格说明的基本结构，这种结构具有较强的描述软件系统的抽 象状态和操作的功能。一个模式由一些变量的声明和限制这些变量的值的谓词两部分组 成，即：模式= 声明+ 谓词。声明部分引入变量，谓词部分表示了关于变量的值的要 求。模式有水平和垂直两种形式。 水平形式： s c h e m a n a m e 尘s c h e m a e x p 垂直形式： 这两种形式引入了一个模式名s c h e m a n a m e 。“兰”是定义符号。模式名或出现 在定义符号的左边或垂直方式模式框的顶端线中。在垂直方式的模式中，中间的横线上 面是声明部分，横线下面的是谓词部分。在水平方式中，定义符号右边是一个模式表达 式。 模式的垂直形式的可理解性和可读性更强，在大多数情况下，人们喜欢使用这种形 式，所以本文中均使用垂直模式。 z 的模式有两个主要用途： 沈阳工业大学硕士学位论文 ( 1 ) 说明软件系统的状态； ( 2 ) 说明状态的转化。 按照用途不同，z 的模式分为状态模式和操作模式。状态模式描述目标软件系统某 一部分数据类型的结构特征。通常一个模式描述系统的状态，实际上是指描述了系统数 据的状态。 操作模式描述的是操作执行前后系统某