（计算机软件与理论专业论文）par方法中关系数据库机制的描述与实现.pdf

p a r 方法中关系数据库机制的描述与实现 摘要 软件的可靠性差和开发效率低一直是困扰软件产业界的两大难题，高效率地 开发正确、可靠的软件已成为软件产业的迫切要求。软件开发的形式化与自动化 方法被认为是克服软件危机、提高软件开发效率和可靠性的有效方法。 如今数据库技术的应用已经深入到每个领域，随着各种大型数据库处理系 统，商业网站特别是一些尖端应用领域( 国防、医疗等) 对数据库应用程序的可 靠性、安全性和开发效率的要求不断提高，传统的数据库应用程序的开发方法已 经无法满足最终用户的需求。为了解决这些问题以及使p a r 方法能更全面地应 用到实际的软件开发中去，本文尝试在p a r 方法中加入数据库机制的描述并初 步实现。 薛锦云教授的p a r 方法对于快速开发可靠的算法程序已经取得了巨大的成 功，但是，p a r 方法还缺少对数据库数据操作和管理服务机制的描述和支持。目 前以关系数据模型为基础的主流数据库技术中，无论是关系代数，关系演算( 元 组或域) ，或者是介于这两者之间的s q l 语言，它们都是建立在严格的集合代数 理论或数理逻辑中谓词演算理论基础之上。正是这样具有严格数学基础的关系模 型，才使得在p a r 方法中加入数据库管理操作机制成为可能。 为此，本文以成熟的关系代数理论为基础，在p a r 方法( e a r 方法的a p l a 语言) 中加入关系数据库管理操作的形式化描述，制定可靠的j a v a 数据库部件 库包类l e e k o t a b l e 支持转换后得到的j a v a 数据库程序的正确运行，并给出每条 a p l a 数据库操作描述所对应的s q l 语句和库类1 a b l e 中的方法。然后以s q l s e e r2 0 0 0 为后台d b m s ，以p a r 方法中原a p l a j a v a 算法程序转换系统为基 础，构建了一个由a p l a 描述的数据库程序到j a v a 数据库程序的自动转换系统。 最后制定了大量有代表性的a p l a 数据库程序对我们的a p l a j a v a 数据库程序转 换系统进行测试，通过这些测试，证明该研究工作基本达到了我们预期的目标。 p a r 方法中关系数据库机制的描述与实现是以p a r 方法为指导思想，以关 系代数为理论基础，通过制定可靠数据库部件库，使得数据库应用程序的开发容 易得到理论上支持、优化和验证，并实现了数据库应用程序代码的部分自动化生 成，从而达到了快速开发正确可靠的数据库应用程序的目的。这样集关系数据库 机制的描述、转换和运行于一体的a d l a j a v a 数据库程序转换系统可应用到国 防、科研、教学、软件开发等各领域。 关键字：p ! a r 方法，r a d l ，a p l a ，关系代数，s o l ，j a v a 数据库程序，程序转换 队r 方法中关系数据库机制的描述与实现 a b s t r a c t t h ep o o rr e 王i a b i l i t yo fs o f t w a r ca n d l o we f f i c i e n c yo fd e v e l o p m e n ta r et h et w o m a i np m b l e m so fs o f 时a r ei n d u s t 珥1 od e v e l o pc o “e c t ，r e l i a b l es o f a r ee 舾c i e n t l y i sa nu r g e n tr e q u i r e m e n to fs o f l w a r ei n d u s t f yn o w a d a y s f o r m a l i z a t i o na n d a u t o m a t i z a t i o ni ns o f h v a r cd e v e l o p m e n ta r ev i e w e da st h ee f f e c t i v ew a y st os o l v e s o f t w a r ec r j s i sa n di m p r o v et h ee f ：i c i e n c yo fd e v e l o p m e n ta n dt h er e l i a b 丑i t yo f s o f t w a r e n o w a d a y s ，t h ea p p l i c a t i o no fd a t a b a s et e c h n o l o g yh a sa l r e a d yg o n ed e 印i n t ot o e a c hi e a l m 砧o n gw i t ht h ci c f e a s i n 出yd e m a n d 0 rt h er e l i a b i l i t y ，s e c u m ya n d d c v e l o p m e n te f f j d e n c yo fd a t a b a s e 印p l i c a t i 咖o fv 盯i o u sl a r g ed a t a b a s ep f o c e s s i n g s y s t e m s 觚db u s i n e s sw e b s i t e se s p e d a l l ys o m ea d v a i l c c da p p l i c a t i o nf i e l d s ( n a t i o n a l d e f e n c e ，m e d i c a lt r e a t m e n te t c ) ，t l l et r a d i t i o n a 王d e v e l o p m e tm e t l l o d so fd a t a b a s e a p p l i c a t i o nc a n o ts a t i s f vt t l ed e m a n d so fe n du s e r sa n ym o r e 1 or e s o l v et t l e s e p r o b l e m sa i l dm a k ei a rm e t h o db ea p p l i e dt os o 脚a f ed e v e l o p m e n tm o r e m p r e h e n s i v e ly ，t h i sp a p e rt r i e st oa d dd e s c r i p t i o no fd a t a b a s em e c h a n i s mt oi a r m e t h o da n di m p l e m c i i tj tp r e l i m i n a 珥 p r 0 x u ej i n y u n sp a rm e t h o dh a sa l r e a d ya c l l i e v e dg r e a ts u c c e s so nd e v e l o p i n g r e l i a b l ea l g o r i t h m j cp r o g 删 nr 印i d l y h o w e v c r ，p a rm e t h o dl a c k si nd e s a i p t i o na i l d s u p p o r to fd a t a b a s eo p e r a t i o na n dm a n a g e m e n ts e r v i c e s n o wa m o n gt h er e l a t i o n a l d a t am o d e l - b a s e dd a t a b a s et e c t l i l o l o g y w h i c hi ss t i l lt h em a i nd a t a b a s et e c h o l o g y ， r c l a t i o n a la l g e b r a ，r e l a t i o n a lc a l c u l u s ( t u p l ea n dd o m a i n ) a n ds q lw l l j c hi sb e t w e e n 也et w ol 孤g u a g e s ，a r ea nb a s e do ns t r i c ta g 掣e g a t ea l g e b r at h c o r yo rp r e d i c a t i o n c a l c u l a t i o ni i ls v m b o l i cl o 窟i c j u s tb e 叫s eo ft h es t r i c tm a t h e m a t i cb a s i so fr c l a i i o n a l m o d e l ，a d d i n gd a t a b a s em a n i p u l a t i o nm e c h a i l i s mt oi 慵rm c t h o di sp o s s i b l e a i l d s u i t a b l e t h e r c f o r e ，t h i sp a p e rt r i e st oa d df o 瑚a ld e s c r i p t i o no fr e l a t i o n a ld a t a b a s e m a n i p u l a t i o nt op a rm e t h o d ( a p l ai nb 娘) ，w h i c hi sb a s e do nm a t u r er c l a t i o n a l a 1 鼬b mt h e o r y a n dt h er e l i a b l ej a v ad a t a b a s el i b r a r yp a c k a g ed a s s1 e e k o t 的l et h a t s u p p o r tm ej a v ad a t a b a s ep m 举a mt r a n s f o 肌e dt omc o r r e c t l yw a sd e v e l o p e d a n d t h ec o e s p o n d i n gs q la n dm e t h o di nt a b l et ot h ed e s c r i p t i o o fe v c r yr e l a l i o n a l d a t a b a s em a l l i p u l a t i o nw e r ea l s og i v e n 1 飞e nw et a k es q ls e r v e r2 0 0 0a s b a c k 争o u n dd b m sa i l db a s eo na p l a j a v aa l g o r i t h m i cp r o 掣a mt r a n s f o n n a t i o n s v s t e mi nf o 加e rp a rm e t l l o dt o n s t m c ta na u t o t r a n s f o 皿a t i o ns v s t e mw h i c h t r a n s f b 肌d a t a b a s ep r o g r a md e s c 曲c db ya p l at oj a v ad a t a b a s ep r o 伊a m a tl a s t ， l a 堵en u m b e r so fr c p f e s e m a t i v ea p l ad a t a b a s ep m 铲a m sw e r ed e v e l o p e dt o t e s tt h e a p l a j a v ad a t a b a s cp r o g m ma u t o - t r a 璐f o 珊a t i o ns y s t e m t h r o u g l lt h e s et e s t s ，i ti s p m v e dt h a tw eh a v ea c h i e v e do u rp r o s p e c t i v eg o a lb a s i c a l ly t h ed e s c r i p t i o na n di p l e m e n t a t i o no fr c l a t i o n a ld a t a b a s em e c h a n i s mi nb r m e t h o da r ei n s t n l c t e db yp a rm e t l l o da l l db a s e do r e l a t i o n a la l g c b r at h e o r y b yt h e r c l i a b l ed a t a b a s ec l 嬲si i b m r i e sw ed e v e l o p e d ，t h ed a t a b a s ep r o g r a md e v e l o p m e m 队r 方法中关系数据库机制的描述与实现 b a s e do np a rm e t h o dc a nb es u p p o r t e d ，o p t i m i z e da n dv a l i d a t e db yt h e o r i e s w ea l s o d a n i a l l yr e a l i z e dt l l ea u t o m a t i cg e n e r a t i o no fd a t a b a s ep r o 伊棚c o d ea n dt n u sc o m e u pt ot h ep u r p o s eo fd e v e l o p i n gr e l i a b l ed a t a b a s ep i d g r a mr a p i d l y t h ea p l a j a v a d a t a b a s ep r o 罩锄 a u t o t r i m s f o r i n a t i o ns y s t e mw h i c hi n t e 擎a t e sd e s c r l p t l o n ， t r a n s f o 珊a t i o na n de x e c u t i o o fr e l a t i o n a ld a t a b a s em e c h 柚i s mi n t oi t s e l fc a nb eu s e d t od i 骶r e n tk i n d so fa p p l i c a t i o nr e a l m s s u c h a sn a t i o n a ld e f e n c e ， s c l e n t l f l c r e s e a r c h ，t e a c h i n g ，s o f 咐a r ed e v d o p m e n ta n d s oo n k e yw o r d ：p a rm e t h o d ，r a d l ，a p l a ，r e l a t i o n a la l g e b r a ，s q l ，j a v ad a t a b a s ep r o g m m ， p m g 舳t m s f o 衄a t j o n i l l p a r 方法中关系数据库机制的描述与实现 1 1 研究背景 第一章绪论 软件的可靠性差和开发效率低一直是困扰软件产业界的两大难题，高效率地 开发正确、可靠的软件已成为软件产业的迫切要求。软件开发的形式化与自动化 方法被认为是克服软件危机、提高软件开发效率和可靠性的有效方法i l 卅。 这一方向一直吸引着大批象d j j k s 打a 、h o a r c 、g r i e s 等著名的计算机科学家 的深入研究，产生了多种多样的软件形式化开发方法和技术，比如v d m 方法、 z 方法、模型检测方法、b 方法、x y z 方法等1 5 】。尽管出现了各种各样的软件形 式化开发方法和开发技术，但目前这些技术还远没有广泛地被软件产业界所接受 1 6 l ，原因在于许多方法的倡导者并没有真正研究软件开发者所面临的实际问题， 造成算法和程序研究相脱节，缺乏系统的算法程序设计和证明方法。事实上有相 当一部分软件形式化方法以及以这些方法为基础而建立的软件开发工具和自动 生成系统只能处理和生成一些玩具式程序( t o y s t y l ep m 蹦瑚) 。尚没有一种面向 实际的软件形式化方法及相配套的一系列辅助开发工具来切实地解决这两个问 题( 可靠程序的开发和证明) 。 薛锦云教授在国家8 6 3 和多项国家自然科学基金课题的资助下，根据多年从 事算法程序设计理论研究的成果，提出了一种简单实用的设计和证明算法的形式 化方法一p a r 方法卜1 3 】。这种方法结合形式化和非形式化方法，正确区分开软件 丌发过程中创造性和非创造性劳动。在该方法的指导下，定义了r a d l 算法设计 语言来描述算法规约和抽象算法，定义了a p l a 语言来描述抽象程序。根据n 堰 方法，由递推关系到循环不变式，及由算法到程序的开发，属于非创造性劳动， 完全可用形式化方法机械地变换得到，也就是可以构造一个自动变换工具由计算 机完成。这个工具就是蹦t 方法中的一系列自动程序转换系统1 1 4 j 。 薛锦云教授提出的p a r 方法和p a r 平台为现代大型软件特别军事、航天等 尖端领域软件的开发在安全性和可靠性方面提供了很好的技术支持和可靠保证。 在p a r 方法和p a r 平台基础上开发出高可靠的软件部件( 构件) ，而这些构件 是经过了p a r 方法严格的形式化推导和验证了的，这就确保了软件开发中核心 算法和操作的正确性和可靠性，而且p a r 方法中的一系列自动程序转换系统实 现了程序代码生成的部分自动化。因此p a r 方法大大提高了软件的可靠性性和 p a r 方法中关系数据库机制的描述与实现 开发效率。然而，目前p a r 方法主要能很好地对算法程序能进行描述、设计和 验证，并且有a p l a j a v a 、a p l a c + + 、a p l a d e l p h i 等一系列算法程序自动转 换系统，这些转换系统中目前也只能对算法程序进行转换，p a r 方法还缺少对数 据库管理操作机制的描述和支持1 1 4 j 。 如今数据库的应用已经深入到每个领域，随着各种大型数据库处理系统以及 商业网站特别是一些尖端应用领域( 国防、医疗等) 对数据库可靠性和安全性要 求的不断提高，陈旧的数据库应用程序的开发方法已经无法满足最终用户的需 求。目前数据库应用程序开发中的抽象化设计主要是集中在数据库建模上，即通 过数据库建模方法( e r 图和o d l 一对象定义语言等) 和工具 ( p o w e r d e s i g n e r e w w i n 等) 确定数据库的结构( 表属性及联系) 。而对于数据 库的管理和查询大都没有理论( 如有严格数学基础的关系代数理论等) 上的抽象 化设计，而是直接在软件开发中使用s q l 语句进行数据库操作。所以在数据库应 用程序开发过程中很难对数据库操作进行优化和验证，而且s q l 语句大都由编程 者手工完成，从而影响数据库应用程序的整体开发效率 “j 。为了解决这些问题 以及使得p a r 方法能更全面地应用到实际的软件开发中去，在p a r 方法中加入 数据库机制的描述和实现就显得尤为重要。 数据库技术是计算机科学技术中发展最快的领域，也是应用最广泛的技术之 一，它已成为计算机信息系统与应用系统的核心技术和重要基础。目前主流的数 据库技术仍然是以关系数据模型为基础的关系数据库技术，关系数据模型有严格 的数学基础，抽象级别高，而且简单清晰，便于理解和使用，从而得到了广泛的 普及【埘。无论是过程查询语言关系代数以及非过程查询语言关系演算( 元组或 域) ，或者是介于关系代数与关系演算之间的关系数据库标准结构化查询语言 s 0 l ，它们都是建立的严格的集合代数理论或者数理逻辑中谓词演算理论基础之 上的m 。正式由于关系模型严格的数学基础，所以使得在e a r 方法中加入数据 库操作管理机制成为可能。 本文中，我们以p a r 方法为指导思想，尝试基于成熟的关系代数理在p a r 方法( p a r 方法的a p l a 语言) 中加入关系数据库管理操作的形式化描述，研制 了可靠数据库部件库类t a b l e ，并给出每条数据库操作描述所对应的s q l 语句及 库类方法；然后以s q l s e e r 2 0 0 0 为后台d b m s ，构建了一个由a p l a 描述的数 据库程序到可执行目标语言的数据库程序的转换系统，由于本课题组和o a 课题 组结合比较紧密以及j a v a 语言本身的优越性，本文中的目标语言我们选择了 j a v a 。最后我们制定大量有代表性的a p l a 数据库程序对我们的a p l a j a v a 数据 库程序转换系统进行测试，通过这些测试，有效地保证了我们的工作基本达到预 期的目标。 2 p a r 方法中关系数据库机制的描述与实现 1 2 研究现状 e f c 0 d d 于1 9 7 0 年正式提出了关系数据库模型，进而又很快建立了完备的 关系代数和关系演算，从此为关系数据库奠定了坚实的理论基础，也把数据库系 统研究引上了健康发展的道路【切。 关系模型下的关系运算有过程查询语言关系代数、非过程查询语言元组演算 和域演算三种，相应的关系查询语言也已经研制出来，他们的典型代表是i s b l 语言、q u e l 语言和q b e 语言1 1 8 】。 i s b l ( i n f 0 册a t i o ns y s t e mb 船el a n g i l a g e ) 是1 b m 公司英格兰底特律科学中 心在1 9 7 6 年研制出来的，用在一个实验系统p r t v ( p e t e r l e er c l a t i o n a lt c s t v e h i c l e ) 上。l s b l 语言非常接近于关系代数，每个查询语句都近似于一个关系 代数表达式。 q u e l 语言( q u e f ) r 踟g l l a g e ) 是美国伯克利加卅i 大学研制的关系数据库系 统i n g r e s 的查询语言，1 9 7 5 年投入运行，并由美国关系技术公司制成商品推 向市场。q u e l 语言是一种基于元组关系演算的并具有完善的数据定义、检索、 更新等功能的数据语言。 q b e ( q u e r y b y e x a m p l e ，按例查询) 是一种特殊的屏幕编辑语言。q b e 是 m m z l o o f 提供的，在约克镇i b m 高级研究实验室为图形显示终端用户设计的 一种域演算语言，1 9 7 8 年在i b m3 7 0 上实现。o b e 使用起来很方便，属于人机 交互语言，用户可以是缺乏计算机知识和数学基础的非程序用户。现在，q b e 的思想己渗入到许多d b m s 中。 还有一个语言s q l ，这是介于关系代数和元组演算之间的一种关系查询语 言，现在已成为关系数据库的标准语言，我们将在第三章详细介绍。 p a r 方法中，目前只能对算法程序进行很好的描述、设计和验证，并且有 a p l a j a v a 、a p l a c + + 、a p l a d e l p h i 等一系列算法程序转换系统躬4j ，这些 转换系统中目前也只能对算法程序进行转换，p a r 方法还没有对数据库管理操作 机制的描述和支持。虽然课题组原成员施炜在a p l a d e l p h i 程序转换系统中曾 经做过添加数据库机制的研究【1 研，但是由于该研究并不是完全基于严格的关系 代数理论以及研究时间有限等因素，并未能很好地实现在p a r 方法中加入数据 库机制的描述和支持。 本文作为尝试性的后续研究，目的就是让p a r 方法能更全面地应用到实际 的软件开发中去，提高软件开发中数据库管理操作程序的可靠性和开发效率，并 使得数据库程序的形式化验证得到保证，为此我们尝试以关系代数理论为基础在 n 幔方法中关系数据库机制的描述与实现 r 攮方法中加入数据库管理操作机制的形式化描述并研制了a p l a j a v a 数据库 程序转换工具。 1 3 论文的主要内容 具体的研究内容主要包括以下几部分： 1 介绍了形式化方法的基本知识以及三种典型的软件形式化方法，并重点 介绍了导师薛锦云教授的p a r 方法，包括p a r 思想，r a d l 和a p l a 语言， p a r 转换工具等。p a r 方法与这些形式化方法有着本质的区别，具有自 身独特的优势。 2 讨论分析了关系数据库理论基础知识，并进行了在p a r 方法中加入数据 库管理操作机制的可行性分析和必要性研究。研究了o d b c 和j d b c 等 数据库访问接口，并制定了可靠j a v a 数据库部件库( 包) 类1 a b l e j a v a 支持转换后得到的j a v a 数据库程序的正确运行。 3 尝试以关系代数为理论基础在p a r 方法中添加a p l a 数据库管理操作机 制的形式化描述，并给出了每条数据库操作描述对应的s q l 语句及部 件库中的方法，为以后的a d l a 数据库程序转换工作奠定基础。 4 完成a p l a j a v a 数据库程序转换系统的设计与实现。包括：总体设计、 词法分析、语法分析，a d l a 数据库程序语句转换、界面设计等。 5 以s q l s e r v e r2 0 0 0 为后台d b m s ( 也可以是其他d b m s ) ，通过制定大 量有代表性的a p l a 数据库程序对a p l a j a v a 数据库转换系统进行了测 试，展现该系统运行效果，并给出系统的应用前景。 本文的也是基于以下的课题研究或者后续研究： “p a r 方法应用于j a v a 程序开发方法研究”。国家自然科学基金课 题，授权号：6 9 9 8 3 0 0 3 “基于p a r 方法的算法程序设计形式化和自动化研究”。国家自然科 学基金课题，授权号：6 0 2 7 3 0 9 2 “形式化方法制导的软件自动化研究”。科技部重大基础研究( 9 7 3 ) 前期研究专项课题，n o ：2 0 0 3 c c a 0 2 8 0 0 1 4 本文篇章结构 本文共分为六章 第一章：绪论。主要介绍课题背景、本文工作和论文的组织结构。 4 队r 方法中关系数据库机制的描述与实现 第二章：p a r 方法概述。介绍了形式化方法的基本知识，目前三种典型的软 件形式化方法，并着重介绍了p a r 方法，包括p a r 方法，r a d l 和a p l a 语言， p a r 转换工具等。 第三章：p a r 方法中加入数据库管理操作机制的可行性分析及准备工作。包 括：关系数据库概述，p a r 方法中加入数据库管理操作机制的可行性和必要性分 析，以及支持j a v a 数据库程序可靠部件库类t a b l e j a v a 的制定。 第四章：p a r 方法中关系数据库语言机制的描述。其中还包括每条数据库操 作形式化描述对应的s q l 语句及部件库中的方法。 第五章：a p l a j a v a 数据库程序转换系统的设计与实现。包括：总体设计、 词法分析、语法分析，a p l a 数据库程序语句转换、界面设计等。 第六章：a p l a j a v a 数据库程序转换系统运行效果和应用。制定了大量的 a p l a 数据库对系统进行测试，并给出相应运行结果，最后给出系统的应用前景。 第七章：总结和展望。对全文进行了总结，并指出下一步的工作方向。 p a r 方法中关系数据库机制的描述与实现 2 1 软件形式化方法 第二章p a r 方法概述 形式化方法的出发点是数学逻辑方法，其目的是开发可靠的软件产品。形式 化方法原则上就是用数学与逻辑的方法描述和验证软件1 5 】。从描述上讲，一方面 是系统或程序的描述，另一方面是性质的描述。这些可以用一种或多种语言来描 述。这些语言包括命题逻辑，一阶逻辑，高阶逻辑，代数，状态机，并发状态机， 自动机，计算树逻辑，线性时序逻辑，进程代数，丌演算，| 1 演算，特殊的程 序语言，以及程序语言的子集等。从验证来讲，主要有两类方法，一类是以逻辑 推理为基础，另一类则以穷尽搜索为基础。逻辑推理有n a t u r a ld e d u c t i o n ，s e q u e m c a l c u l u s ，r e s o l u t i o n 以及h o a r c 1 0 百c 等方法。穷尽搜索方法统称为模型检测。这 类方法与系统或程序以及系统性质的表示有很大的关系，比如说符号模型检测， 其基本原理是用命题逻辑公式表示状态转换关系，用不动点算法计算状态的可达 性以及这些状态是否满足某些性质【驯。 形式化方法可以分为形式化描述和建立在形式化描述基础之上的形式化开 发。形式化的描述就是用形式化的语言( 具有严格的语法语义定义的语言) 做描 述。形式化的软件开发，就是用形式化的语言来描述软件需求和特征，并且通过 推理验证来保证最终的软件产品是否满足这些需求和具备这些特征。这样的验证 当然得建立在严格的语法语义的基础之上的。在实际应用中，这是不容易做到的。 形式化方法研究的目的就是希望能够提供更好的理论、方法和工具，扩大形式化 方法的应用范围和使用价值【6 、2 “。 形式化方法在软件开发中能够起到的作用是多方面的。首先是对软件需求和 设计的描述。软件需求的描述是软件开发的基础，比如说一般非形式化的描述很 可能导致描述的不明确和不一致。如果描述的不明确和不一致导致设计，编程的 错误，将来的修改所要付出的代价就非常大了；如果导致的错误没有被发现，则 影响程序的可靠和使用。形式化方法则要求描述的明确性，而描述的不一致性也 就相对易于发现。形式化方法的优点对于软件要求的描述同样适用于软件设计的 描述。另外由于有了软件要求的形式化描述，我们可以检验软件的设计是否满足 软件的要求。该方面的意义在于它能帮助发现其它方法不容易发现的系统描述的 不一致，不明确或不完整，有助于增加软件开发人员对系统的理解，因此形式化 一6 一 p a r 方法中关系数据库机制的描述与实现 方法是提高软件系统，特别是s a f e t y c r i t i c a l 系统的安全性与可靠性的重要手段。 对于编程来讲，我们可以考虑自动代码生成。对于相对独立算法程序( 构件) 甚 至一些简单的系统，形式化的描述有可能直接转换成可执行程序，这就简化了软 件开发过程，提高了开发效率，节约了资源和减少了出错的可能性。另外，形式 化方法可以用于程序的验证，以保证程序的正确性。对于测试来讲，形式化方法 可用于测试用例的自动生成，这可以节约许多时间和在一定程度上保证测试用例 的覆盖率。i z l 埘j 2 2 软件形式化的国内外研究现状 形式化方法的研究早在2 0 世纪4 0 年代就开始了，象d j j k s t m 、h o a r e 、g r i e s 、 m 釉a 等著名的计算机科学家都涉足该领域进行了大量的研究，产生许多多种多 样的软件形式化丌发方法。这些方法在技术上都有一些相似性，太多数方法都以 逻辑、代数和范畴论等为基础，只是在表达上有所区别。下面我们给出几种有代 表性的形式化方法和工具。 2 2 1v 酬方法 v d m ( t h ev i e n n ad e v e l o p m e n tm e t h o d 维也纳开发方法) 是在1 9 6 9 年为开 发p l 1 语言时，由i b m 公司维也纳实验室的研究小组提出的，v d m 是一种功 能构造性规格说明技术i ”】。它通过阶谓词逻辑和已建立的抽象数据类型来描 述每个运算或函数的功能，这种方法在9 0 年代初在欧美许多研究机构或大学得 到了广泛的应用。) m 技术的基本思想是运用抽象数据类型、数学概念和符号 来规定运算或函数的功能，而且这种规定的过程是结构化的，其目的是要在系统 实现之前简短而明确地指出软件系统要完成的功能，由于这种形式化规格说明中 采用了数学符号和抽象数据类型，从而可使软件系统的功能描述在抽象缴上进 行，完全摆脱了实现细节，这样为软件实现者提供了很大的灵活性，此外，这种 形式化规格说明还为程序正确性证明提供了依据。应用v d m 技术进行系统开发 包含了形式化规格说明、程序实现和程序正确性证明三个部分。 使用v d m 规定形式化规格说明具有以下三个明显的优点： 1 1 只告诉计算机做什么； 劲提供了程序正确性证明的依据； 3 1 使规格说明描述简练、精确。 除了这三个明显的优点外，使用v d m 还可以培训程序设计者牢固树立先抽 象、后具体的不断证明其正确性的逐步分解的自顶向下的开发思想，从而在整个 p a r 方法中关系数据库机制的描述与实现 程序开发的全过程中用系统而严密的方法保证所丌发的程序的正确性。 但是，v d m 也存在一些不足之处： 1 ) 由于v d m 对抽象数据类型预先定义了运算，而某些用户定义的类型在 规格说明描述中无需这么多运算，因而产生了运算冗余。 2 ) v d m 目前还未能建立一整套描述机制，将一个大型系统分解为许多运 算而描述出这些运算之间的关系。 3 ) 由于采用数学符号和抽象数据类型，v d m 形式规格说明过于形式化往 往不容易理解，这有可能造成未读懂形式规格说明而错误地实现其软件 的情况。 此外，尽管v d m 的规约语言已由i s o 标准化并得到许多成熟工具的支持， 但是目前还没有一个满意的工具来支持验证。 2 2 2z 方法 z 以经典集合论和一阶谓词逻辑为基础，提供了一种称为模式的结构，以此 来描述一个规格说明的状态空间和操作。z 规格说明由一系列模式组成，每个模 式定义一个抽象对象或操作，并用谓词判定描述给出新的对象或操作的语义约 束。z 模式说明可以组合成新的z 模式，新的z 模式继承其成分模式的一切属性 和约束。这样，软件系统的z 模式规格说明可以按一定的层次结构给出。模式 的使用为规格说明提供了一种演算，通过这种演算，无论多么大型系统的规格说 明都可以通过一个个小的部分来构成。基于一阶谓词和集合论的形式规格说明 语言z ，利用模式和模式演算对目标软件系统的结构和行为特征进行抽象描述， 其中状态模式对目标软件系统的结构特征进行抽象描述，操作模式对目标软件系 统的行为特征进行抽象描述。i 嬲】 z 已经成为世界上最流行的形式化规约语言之一。有大量的工具支持，他 们主要集中在规约的编辑和显示以及语法和类型检测方面，也有些工具支持它的 规约推理和精化，比较有影响的工具有：f o 肿a l i s e r 、p r o o f p o w e r 、z o l a 、c a d j z 、 f o r m o o z 、五吧s 等【2 9 1 。 这是一种具有特色的有效的形式化方法，但是z 语言还存在如下缺点： 1 、z 语言对大型系统的模块化能力不足。因为在z 语言中，目标软件系统 的结构和特征都用模式来描述，随着系统的增大，模式也会越来越多， 而z 语言中没有更加有效的机制来管理这些模式，最终导致z 规格说明 难以阅读。 2 ) 难以识别影响某一状态模式的所有操作模式。因为在z 语言中，一个操 作模式可能涉及多个状态模式，为了确定能影响特定状态模式的所有操 p a r 方法中关系数据库机制的描述与实现 作模式，就需要逐个检查全部操作模式的声明部分，这对于大型软件系 统的规格说明来说是不实际的。 3 1 不能支持规格说明的重用。z 语言中没有提供重用机制。 4 1z 语言难以由计算机直接处理。 因为在设计z 语言时，只是考虑到把z 语言作为一种严格的描述手段并没 有考虑到将来由计算机辅助进行z 语言应用，所以许多z 语言符号在计算机中 没有对应的键，难以进行规格说明的输入和自动化处理。为了克服z 语言这些 缺陷，8 0 年代末到9 0 年代初相继提出了一些z 语言的扩展方案，也进行了一些 标准化工作，国际上在9 0 年代初提出形式化方法和面向对象方法相结合的思想， 虽然有所发展，但因缺少商品化的工具支持等到诸多原因，而不能大量的实际应 用，因而还需进一步完善【捌。 2 2 3b 方法 b 方法于8 0 年代初产生于法国，由法国计算机科学家j r a b r i a l 提出，9 0 年代中期发展成熟。它是在v d m 和z 的基础上发展起来的，和z 尤其相似p 。 b 是计算机辅助软件工程中b 技术、方法和工具集的简称，b ( 包含b 方法，b 工具，b 工具盒) 是一种健全的面向实际软件过程的基于数学理论的技术，b 方 法所用的符号和方法支持大部分的软件过程：需求分析、规格说明、软件设计、 实现和维护，分层软件的逐步构造伴随着逐步的验证和校验是b 方法的指导性 原则；b 工具盒包括有大量的工具，所有的工具集成在一个基于窗口的软件开发 环境中，这些工具能集成地自动运行，因而支持运用b 方法开发软件的整个软 件过程；b 工具支持软件的逐步构造，其中的验证过程可用静态分析，动态分析 采用模拟技术，正确性证明则使用集成的定理证明器1 2 ”。 b 严密管理控制整个软件过程，在软件开发早期规格说明阶段，开发人员将 对照用户的需求来验证测试系统需求模型的一致性，在每个开发阶段，每个设计 描述都将与规格说明的需求文档对照其一致性，最低一级的设计部件由预先定义 的可靠的部件库组装得到，并翻译成可执行代码，可靠的预定义的构件通过测试 或重用生成( 许多部件已经为b 工具集所应用) ，新的低层构件也可以进一步添 加，这些添加的构件可通过已存在的可靠的部件开发，并测试得到他们的属性。 b 方法有个工具包( b t o o l l 【i t ) ，其中所有的工具都集成与w i n d o w s 的环境下， 它可以让用户编写程序，可以通过使用模拟来进行静态或动态的验证以确保程序 的正确性。但使用b 方法书写需求规范比较复杂。p l j 另外美国k e s t r e l 研究所在软件形式化开发和自动化生成代码方面也取得了 比较大的成功【3 5 】，有关k e s t r e l 【3 1 _ 3 4 】的详情请见h t t p ： 聊，、 ，k e s t r c l e d u 。 p a r 方法中关系数据库机制的描述与实现 2 3p a r 方法 p a r 方法支持软件开发的全过程，是形式化软件开发中p a r 思想、技术、 语言和工具集的简称【川。主要有四个部分组成： ( 1 ) p a r 方法的算法描述语言r a d l ( 2 ) p a r 方法的抽象程序设计语言a p l a ( 3 ) 统一的算法设计和证明方法 ( 4 ) 系列自动程序转换工具。 2 3 1p a r 方法的总体思想 p a r 方法是薛锦云教授在多年承担国家8 6 3 和国家自然科学基金项目课题的 基础上，通过对现存算法程序设计方法局限性和寻找问题求解序列递推关系的深 入研究，进而提出的一种统一的算法程序设计和证明方法，它并不是对国际上某 些形式化方法的修补，而是本着“从源头上创新”的原则，参考众多形式化开发 方法的优缺点，结合在大量开发实例中摸索出的经验、心得，创造性地提出的一 种新的形式化软件开发方法。其基本指导思想是，分离创造性劳动和非创造性劳 动，通过不断地提出新的理论、方法，尽可能多得把创造性劳动转化为非创造性 劳动，对创造性劳动采用部分形式化理论进行描述、推导、演算，对非创造性劳 动用相关工具进行机械转换。并对循环不变式重新定义，提出了递推关系、问题 求解序列等一系列新的概念，结合分化、递推等思想及大量开发实例，探索出求 解循环不变式的两种策略及其总结出一套行之有效的开发步骤，提出了形式化描 述语言r a d l 及抽象描述语言a d l a ，并在此基础上研制了一系列转换工具，。使得 p a r 方法很快在众多方法中脱颖而出。大量实践证明，p a r 方法不仅开发小程 序切实可行，而且开发复杂算法也十分有效。在教学过程中，用p a r 方法的思 想来讲解算法也收到了十分令人满意的效果。p a r 方法在高可靠性领域的丌发也 已初见成效。p a r 方法因其卓越的成绩受到计算机科学最高奖获得者硒u t h 和中 科院张景中院士等国际国内多位著名计算机科学家的高度赞扬【7 _ 1 3 】。 2 3 2p a r 方法的语言 r a d l 语言和a p l a 语言是薛锦云教授为实现算法程序形式化和半自动丌发的 p a r 方法而定义的两种基于递归关系的算法和抽象程序设计语言，是p a r 方法 的重要组成部分。目前r a d l 语言和a p l a 语言主要适用于高可靠( s a f e t y c r i t i c a l ) p a r 方法中关系数据库机制的描述与实现 软件部件( 构件) 的开发【3 3 。4 1 。 2 3 2 1 算法设计语言r a d i r a d l 语言是我们为实现算法程序形式化和半自动化开发的p a r 方法而定义 的一种基于递推关系的算法设计语言，它是p a r 方法的重要组成部分【1 2 1 。它主 要功能是描述问题的规约、规约变换规则和描述算法，所以r a d l 由算法规约语 言和算法描述语言两部分组成。r a d l 用作a p l a 语言的前端语言主要面向用户， 适应传统的数学习惯，且具有引用透明性，便于算法的形式化推导证明。r a d l 的一个重要特色是它的数据类型系统，它提供了标准数据类型、自定义简单类型、 预定义a d t 和自定义a d t 机制。用户