（计算机软件与理论专业论文）radl→apla自动程序转换系统研究与实现.pdf

摘要 从 “ 软件危机”爆发至今，有很多新方法和新工具被提出，致力于解决 “ 软 件危机” 的各个方面。 但现有的这些解决方案并没有使人们彻底地从“ 软件危机” 中 解脱出来。用形式化方法开发正确、高效的算法程序，被当今计算机界誉为克 服 “ 软件危机” ，提高软件可靠性和生产效率的革命性途径。 薛锦云教授在国家8 6 3 和多项国家自 然科学基金的资助下，根据多年从事算 法程序设计理论研究的成果，提出了一种简单实用的设计和证明算法的形式化方 法 p a r 。 在该方法的 指导下， 定义了r a d l ( r e c u r r e n c e - b a s e d a l g o r i t h m d e s i g n l a n g u a g e ) 抽象算 法设计语言来 描述算法规约和抽象算法， 定 义了a p l a ( a b s t r a c t p r o g r a m m i n g l a n g u a g e ) 语言 来描述抽象程序。 本项研究作为p a r方法研究的一个重要组成部分， 目 标是开发一个自 动程序 转 换 系 统， 该系 统能 将 用r a d l 语言 描 述的 算 法转 换 成抽 象 语言 程序a p la 程 序。 围绕转换系统的设计与实现，本文主要做了一下工作: 1 、 对r a d l 算法 描 述 语言 和柳la 抽 象 程序 语言 进 行了 归 纳 和 整 理。 2 、 归 纳总 结r a d l 语言 到a p l a 语言的 程 序变 换规 则。 3 、 基本 上 实 现了由r a d l 算 法语言 程序到a p l a 程序 语言 程 序的自 动转 换。 4 、用一些典型的算法程序对转换系统进行测试。 r a d l - a p l a 自 动 转换系统已 经 将r a d l 语言书写的 数组求 和、 立方问 题、 层次 遍 历二 叉 树、 图 的 遍 历等 算 法 转 换为a p l a 程 序并 运行 得到 正 确结 果。 本研究主要进行了如下创新: 1 、 实 现了r a d l 语言中 的 无 序递 推 关 系式 到a p l a 程 序的 转 换 2 、 实 现了r a d l 语言中 的隐 式 递推 关 系 式 到a p la 程 序的 转 换 关键字:p a r 方 法， r a d l , a p i a ， 程序 转 换 r a d l - a p l a 自 动程序转换系统研究与实现 ab s t r a c t s i n c e s o f t w a r e c r i s i s b r o k e o u t , t h e r e h a v e m a n y n e w m e th o d s a n d n e w t o o l s a v a i l a b l e t o s o l v e p r o b l e m s r e s u l t e d f r o m i t . h o w e v e r , t h e s e e x i s t i n g s o l u t i o n s c a n t l i b e r a t e p e o p l e f r o m s o f t w a r e c r i s i s t h o r o u g h l y . d e v e l o p i n g二二c t a n d e ff i c i e n t a l g o r i t h m i c p r o g r a m s w i t h f o r m a l m e th o d s i s c a l l e d r e v o l u t i o n a ry a p p r o a c h b y c u r r e n t c o m p u t e r w o r l d t o o v e r c o m e , s o f t w a r e c r i s i s a n d i m p r o v e s o f t w a r e s r e l i a b i l i t y a n d p r o d u c t i v i t y . a c c o r d i n g t o 于 . ， . r r_ f o f s e e :r r 1 p r o j e c t s s u p p o r t e d b y 8 6 3 h i - t e c h p r o g r a m m e arid n a t i o n a l n a t u r e 3 : i c n c e r t - u r :rl - 一 理 弓 o f c h i n a , p r o f e s s o r x u e p r o p o s e d a s i m p l e a n d p r a c t i c a b l e a p p r o a c h f o r f o r m a l d e v e l o p m e n t a n d p r o v i n g o f a l g o r i t h m i c p r o g r a m s . 一 一p a r a p p r o a c h . i n a d d i t i o n , r a d l i s d e f i n e d f o r d e s c r i b i n g a l g o r i t h m i c s p e c i f i c a t i o n s a n d a l g o r i t h m s , a n d a p l a i s d e f i n e d f o r d e s c r i b i n g a b s t r a c t p r o g r a m s . t h is p a p e r s r e s e a r c h w o r k i s a n i m p o rt a n t c o m p o n e n t o f t h e p a r m e t h o d . t h i s r e s e a r c h s g o a l i s t o d e v e l o p a n a u t o p r o g r a m t a n s f o r m i n g t h e a l g o r i t h m p r o g r a m d e s c r i b e d b y r a d l i n t o th e a p l a p r o g r a m . t h e f o l l o w i s t h e m a i n w o r k s o f t h e p a p e r : 1 , i n d u c t a n d c o o r d i n a t e t h e r a d l a n d a p l a l a n g u a g e . 2 , s u m m a r y t h e r u l e s f o r t r a n s f o r m a t i o n fr o m a n a l g o rt i t h m d e s c r i b e d b y r a d l i n t o a n a p i a p r o g r a m. 3 , i m p l e m e n t t h e a u t o m a t i c t r a n s f o r m a t i o n f r o m a n a l g o r t h m d e s c r i b e d b y r a d l i n t o a n a p l a p r o g r a m . 4 , u s i n g s o m e t y p i c a l a l g o r i t h m s t o t e s t t h e s y s t e m t h i s t r a n s f o r m e r h a s a l r e a d y tr a n f o r m e d s o m e t y p i c a l a l g o r i t h m s d e s c r i b e d b y r a d l s u c h a s s u m a r r a y , c u b e p r o b l e m , p r e - t r a v e l t r e e a l g o r i t h m s a n d t r a v e l g r a p h a l g o r i th m s i n t o a p l a p r o g r a m . d u r i n g t h e t i m e o f r e s e a r c h a n d i m p l e m e n t a t i o n , w e m a k e th e f o l l o w i n g i n n o v a t i o n s : 1 , i m p l e m e n t th e t r a n s f o r m a t i o n f r o m o u t - o f - o r d e r r e c u r r e n c e s d e s c r i b e d b y r a d l i n t o a p i a p r o gr a m . 2 , i m p l e m e n t t h e t r a n s f o r m a t i o n f r o m c o n n o t a t i v e r e c u r r e n c e s d e s c r ib e d b y r a d l i n t o a p l a p r o gra m. . k e y w o r d s : p a r m e t h o d , r a d l , a p l a , p r o gr a m tr a n s f o r m i n g i al一 a p l a自 动程序转换系统研究与实现 引 言 夸 1研究背景 从 6 0年代以来，人们一直受到 “ 软件危机 “ 的困扰，软件的可靠性和开发 效率远远满足不了社会发展的需要。一方面，软件故障给人们的生命和财产造成 巨大的损失， 如欧共体在1 9 9 7 年6 月的阿里亚那一5 型火箭发射事故中损失了几 十个亿，而事故的主要原因就是在于软件的故障;又如在许多造成人身伤亡的重 大医疗事故中， 也有大部分是由医疗设备的软件故障所引起的。 随着社会的发展， 计算机在人们的工作生活中越来越普及，然而计算机软件的质量却一直不容乐 观。另一方面，虽然人们对计算机软件、硬件的需求日 益增加，但据国外研究调 查显示:资深的程序员一年平均所能编写的有效代码仅为一千多行。由此可见， 软件的生产速度远远满足不了市场的需要12 1 。因此，如何才能有效地提高软件的 生产效率和可靠性也就成为计算机科学家研究的热点。 众所周知，用形式化方法开发软件，被当今计算机界誉为克服 “ 软件危机气 提高生产效率和可靠性的革命性途径。特别是对于一些安全性、可靠性至关重要 的 军事系统和医 用系统来说， 形式化方法就显得 尤为 重要2 1 。 在过去的3 0 多 年里， 己经出现了许多种形式化方法，然而这些方法并没有被软件界广泛接受，主要原 因在于对形式化的软件开发方法认识上的误区和缺少相应的开发工具。当务之急 就是需要研究一种面向实际问题、 简单可行、便于广大软件开发者使用的形式化 方法以 及相应的辅助工具。在这种情况下，一些计算机科学家冷静地分析了软件 开发中存在的问题，指出形式化地进行软件开发必须正确地区分软件开发过程中 的创造性劳动和非创造性劳动，采用部分形式化和完全形式化相结合的方法，探 索软件开发的本质和规律， 把软件开发中 尽可能多的 创造性劳动转化为非创造性 劳 动， 逐步扩大软件开发中 可形式 化的 部分1 2 1 薛锦云教授按照软件部分形式化和完全形式化相结合的思想，对算法程序的 开发进行研究，正确区分开发算法中的创造性劳动和非创造性劳动，提出了算法 程序开发中的问题求解序列的递推关系的概念，循环不变式的开发新策略。 基于 这些概念和技术， 对许多典型复杂算法程序进行推导和证明，进而提出了一种同 i al一 a p l a自 动程序转换系统研究与实现 引 言 夸 1研究背景 从 6 0年代以来，人们一直受到 “ 软件危机 “ 的困扰，软件的可靠性和开发 效率远远满足不了社会发展的需要。一方面，软件故障给人们的生命和财产造成 巨大的损失， 如欧共体在1 9 9 7 年6 月的阿里亚那一5 型火箭发射事故中损失了几 十个亿，而事故的主要原因就是在于软件的故障;又如在许多造成人身伤亡的重 大医疗事故中， 也有大部分是由医疗设备的软件故障所引起的。 随着社会的发展， 计算机在人们的工作生活中越来越普及，然而计算机软件的质量却一直不容乐 观。另一方面，虽然人们对计算机软件、硬件的需求日 益增加，但据国外研究调 查显示:资深的程序员一年平均所能编写的有效代码仅为一千多行。由此可见， 软件的生产速度远远满足不了市场的需要12 1 。因此，如何才能有效地提高软件的 生产效率和可靠性也就成为计算机科学家研究的热点。 众所周知，用形式化方法开发软件，被当今计算机界誉为克服 “ 软件危机气 提高生产效率和可靠性的革命性途径。特别是对于一些安全性、可靠性至关重要 的 军事系统和医 用系统来说， 形式化方法就显得 尤为 重要2 1 。 在过去的3 0 多 年里， 己经出现了许多种形式化方法，然而这些方法并没有被软件界广泛接受，主要原 因在于对形式化的软件开发方法认识上的误区和缺少相应的开发工具。当务之急 就是需要研究一种面向实际问题、 简单可行、便于广大软件开发者使用的形式化 方法以 及相应的辅助工具。在这种情况下，一些计算机科学家冷静地分析了软件 开发中存在的问题，指出形式化地进行软件开发必须正确地区分软件开发过程中 的创造性劳动和非创造性劳动，采用部分形式化和完全形式化相结合的方法，探 索软件开发的本质和规律， 把软件开发中 尽可能多的 创造性劳动转化为非创造性 劳 动， 逐步扩大软件开发中 可形式 化的 部分1 2 1 薛锦云教授按照软件部分形式化和完全形式化相结合的思想，对算法程序的 开发进行研究，正确区分开发算法中的创造性劳动和非创造性劳动，提出了算法 程序开发中的问题求解序列的递推关系的概念，循环不变式的开发新策略。 基于 这些概念和技术， 对许多典型复杂算法程序进行推导和证明，进而提出了一种同 r a d l 一 a p l a 自 动程序转换系统研究与实 现 一的 算 法 程 序 设 计 和 证明 的 方 法一 p a r 方 法 ( p a rt i t io n a n d r e c u r ) ， 这 种方 法 含盖 了目前普遍使用的枚举法、分治法、贪心法、动态规划法、回朔法等算法设计方 法， 是一 种简单、 统一的算法设计方法， 也是克服软件危机、 实用的形式化方法。 采用p a r方法推导出的递推函数关系式可以自然方便的书写成循环不变式， 使得 算法程序的推导和证明成为一体。 2本文的工作和组织 本文做的主要工作 1 、 对r a d l 算法描述语言和a p l a 抽象程序语言进行了归纳和整理。 2 、 归 纳总 结r a d l 语 言到a p l a 语 言的 程 序 变 换 规 则。 3 、 基本上实 现了由r a d l 算法语言 程序到a p l a 程 序语言 程序的自 动 转换。 4 、用一些典型的算法程序对转换系统进行测试。 本文分六章进行阐述，第一章:介绍软件形式化与自 动化的发展概况。 第二 章: r a d l - a p l a自 动程序转换系统的总体设计， 包括系统结构和运行界面的设计。 第三章: 介绍r a d l - a p l a 自 动程序转换系统的具体实现。 第四章: 介绍r a d l - a p l a 自 动程序转换系统的一些具体应用。第五章;对工作的总结与展望。 以上研究是下列课题研究的成果和继续: 1 、国 家自 然科学基金课题 “ 部分实现理论及其性算法程序形式化推导和证明中 应用” 2 ,国家自 然科学基金高技术探索项目“ 实用的软件形式化方法及其开发工具研究” 3 、国家8 6 3 计划课题 “ 一种统一的算法设计研究” 4 、江西省跨世纪学术带头人项目“ 高可靠性计算机程序开发系统” r a d l 一 a p l a 自 动程序转换系统研究与实 现 一的 算 法 程 序 设 计 和 证明 的 方 法一 p a r 方 法 ( p a rt i t io n a n d r e c u r ) ， 这 种方 法 含盖 了目前普遍使用的枚举法、分治法、贪心法、动态规划法、回朔法等算法设计方 法， 是一 种简单、 统一的算法设计方法， 也是克服软件危机、 实用的形式化方法。 采用p a r方法推导出的递推函数关系式可以自然方便的书写成循环不变式， 使得 算法程序的推导和证明成为一体。 2本文的工作和组织 本文做的主要工作 1 、 对r a d l 算法描述语言和a p l a 抽象程序语言进行了归纳和整理。 2 、 归 纳总 结r a d l 语 言到a p l a 语 言的 程 序 变 换 规 则。 3 、 基本上实 现了由r a d l 算法语言 程序到a p l a 程 序语言 程序的自 动 转换。 4 、用一些典型的算法程序对转换系统进行测试。 本文分六章进行阐述，第一章:介绍软件形式化与自 动化的发展概况。 第二 章: r a d l - a p l a自 动程序转换系统的总体设计， 包括系统结构和运行界面的设计。 第三章: 介绍r a d l - a p l a 自 动程序转换系统的具体实现。 第四章: 介绍r a d l - a p l a 自 动程序转换系统的一些具体应用。第五章;对工作的总结与展望。 以上研究是下列课题研究的成果和继续: 1 、国 家自 然科学基金课题 “ 部分实现理论及其性算法程序形式化推导和证明中 应用” 2 ,国家自 然科学基金高技术探索项目“ 实用的软件形式化方法及其开发工具研究” 3 、国家8 6 3 计划课题 “ 一种统一的算法设计研究” 4 、江西省跨世纪学术带头人项目“ 高可靠性计算机程序开发系统” r a d l 一 a n l a自 动程序转换系统研究与实现 第一章 软件形式化和自 动化 1 . 1 形式化方法 形式化方法的研究早在4 0 年代就开始了， 是公理方法发展的高级形态。 它把 逻辑推理过程完全量化了，完全抽掉了语句的具体内容而代之以符号 “ 运算”来 完成其证明。形式公理化方法具有高度的形式化和抽象化，其中的基本概念、基 本关系的表达、全部命题的陈述、证明 都要符号化，具体地讲， 它的对象、基本 关系不仅用抽象的符号表示，而且将命题表示成由符号组成的公式，命题的证明 用一 个公 式串 来表达， 它主要采用数理 逻辑 作为 它的演 绎推理工具 1 71 。 形式 化程 序设计方法以 提高软件可靠性和生产效率以 及实现程序设计自 动化为目 标。 它用 谓词逻辑和数学公式精确地描述算法和程序的功能或需求，构成形式化规约。 这 种形式的规约精确而没有二义性， 便于进行数学的 变换，为开发正 确的 算法程序 提供了有力的支持。 v d m, z , r a i s e等就属于这种类型的形式化程序设计方 法。更高层次的形式化方法不仅支持形式功能规约的开发，还支持算法程序开发 的全过程，也就是能够基于形式功能规约，通过一系列形式化数学变换，推导出 正确的程序;或者对已 有的程序， 用数学的方法进行严格的正确性证明。 这样的 形式化程序设计方法为实现程序设计自 动化提供了有力的支持。由法国学者 a b r i a l 发明的b 方法，以 及】 a r方法都属于这类形式化方法h a l 妇， 2形式化软件开发方法及其研究意义 互 1 . 2 . 1 软件 开发 的 一般 方法 目前软件开发的主要方法是自 顶向下、逐步求精法。这类方法强调开发过程 是由问题到解答、由总体到局部、由一般到具体。自 顶向下方法提供了从高层次 ( 问题定义)到低层次 ( 编程实现)的分层分解的决策策略和决策方式，并在具 体的开发方法中给出相应的描述工具和设计步骤。自 顶向 下方法体现了逐步求精 和信息隐藏的原则。所谓逐步求精即从最能直接反映间题的基本概念和总体结构 出发、逐步精化、具体化、补足细节，直到成为可以在机器上执行的程序。逐步 求精离不开信息隐藏， 在精化的每一层上把其组成部分的 详细内容，留 给下层来 设计。所以逐步求精使得软件具有较好的层次结构。 r a d l 一 a n l a自 动程序转换系统研究与实现 第一章 软件形式化和自 动化 1 . 1 形式化方法 形式化方法的研究早在4 0 年代就开始了， 是公理方法发展的高级形态。 它把 逻辑推理过程完全量化了，完全抽掉了语句的具体内容而代之以符号 “ 运算”来 完成其证明。形式公理化方法具有高度的形式化和抽象化，其中的基本概念、基 本关系的表达、全部命题的陈述、证明 都要符号化，具体地讲， 它的对象、基本 关系不仅用抽象的符号表示，而且将命题表示成由符号组成的公式，命题的证明 用一 个公 式串 来表达， 它主要采用数理 逻辑 作为 它的演 绎推理工具 1 71 。 形式 化程 序设计方法以 提高软件可靠性和生产效率以 及实现程序设计自 动化为目 标。 它用 谓词逻辑和数学公式精确地描述算法和程序的功能或需求，构成形式化规约。 这 种形式的规约精确而没有二义性， 便于进行数学的 变换，为开发正 确的 算法程序 提供了有力的支持。 v d m, z , r a i s e等就属于这种类型的形式化程序设计方 法。更高层次的形式化方法不仅支持形式功能规约的开发，还支持算法程序开发 的全过程，也就是能够基于形式功能规约，通过一系列形式化数学变换，推导出 正确的程序;或者对已 有的程序， 用数学的方法进行严格的正确性证明。 这样的 形式化程序设计方法为实现程序设计自 动化提供了有力的支持。由法国学者 a b r i a l 发明的b 方法，以 及】 a r方法都属于这类形式化方法h a l 妇， 2形式化软件开发方法及其研究意义 互 1 . 2 . 1 软件 开发 的 一般 方法 目前软件开发的主要方法是自 顶向下、逐步求精法。这类方法强调开发过程 是由问题到解答、由总体到局部、由一般到具体。自 顶向下方法提供了从高层次 ( 问题定义)到低层次 ( 编程实现)的分层分解的决策策略和决策方式，并在具 体的开发方法中给出相应的描述工具和设计步骤。自 顶向 下方法体现了逐步求精 和信息隐藏的原则。所谓逐步求精即从最能直接反映间题的基本概念和总体结构 出发、逐步精化、具体化、补足细节，直到成为可以在机器上执行的程序。逐步 求精离不开信息隐藏， 在精化的每一层上把其组成部分的 详细内容，留 给下层来 设计。所以逐步求精使得软件具有较好的层次结构。 r a d l 一 a p l a 自 动程序转换系统研究与实现 6 0年代中期，在大型软件系统的开发中遇到 “ 软件危机， ，促使人们去考察 软件设计木身固有的问题。自 顶向下方法就是在这一背景下，与结构程序设计及 软件工程同时产生的，并一直伴随和促进着软件工程的发展。 自 顶向下方法源于结构程序设计，结构程序设计方法的引入从方法学上说是 程序设计技术的一场革命，其意义不仅在于当时为解决 “ 软件危机”的实用性一 面，而更深远的意义还在于它使程序设计技术成为一种系统的方法，使程序设计 从依赖设计者个人的技艺变成一门科学。 使m j 自 顶向 下的 方法开发软 件分为以 下几个步 骤4 6 一、分析 ( 需求定义) 。即理解和表达用户对程序功能的需求，明确程序的 总任务这项工作也叫做建立程序系统的规格说明。 二、总体设计。按照程序的要求，把总任务分解为一些功能相对独立的子任 务 ( 目 标)的组合。分解工作可以反复进行，以达到每个子目 标只专门完成单一 的逻辑功能。因此总体设计就是对总任务进行分解，以确定程序的模块结构和各 模块的功能。 三、模块设计 ( 详细设计) 。对于以上目 标，按照它们各自的功能要求，逐 一明确 “ 怎么做”即给出其算法。 四、编码。将算法用计算机可以识别的语言适当地描述出来，即编程序。 五、验证或测试。程序证明，就是使自己和别人都能确信程序正确的论述。 这种意义下的证明，正如k n u t h 所说，实际上是指一种理解。证明可以是从公理 出发的形式推导，也可以是非形式的。 从以卜 步骤可以发现，自 顶向下逐步求精的方法只适用于逻辑关系简单的问 题。对那些逻辑关系复杂的子目 标 ( 模块或算法) 用自 顶向下的方法往往就难以 奏效。因此需要研究新的算法程序开发方法解决这一问 题。 1 . 2 . 2 形 式 化软 件开 发方 法 按传统软件开发方法设计与开发的软件产品， 尤其是要求高可靠性的实时控制软 件和军用软件 ( 包括顺序、并行和实时软件) 等大型软件系统，普遍存在着系统 正确性及可靠性难以保证等问 题，且难于实现软件自 动化。八十年代以 来，形式 r a d l 一 a p l a 自 动程序转换系统研究与实现 6 0年代中期，在大型软件系统的开发中遇到 “ 软件危机， ，促使人们去考察 软件设计木身固有的问题。自 顶向下方法就是在这一背景下，与结构程序设计及 软件工程同时产生的，并一直伴随和促进着软件工程的发展。 自 顶向下方法源于结构程序设计，结构程序设计方法的引入从方法学上说是 程序设计技术的一场革命，其意义不仅在于当时为解决 “ 软件危机”的实用性一 面，而更深远的意义还在于它使程序设计技术成为一种系统的方法，使程序设计 从依赖设计者个人的技艺变成一门科学。 使m j 自 顶向 下的 方法开发软 件分为以 下几个步 骤4 6 一、分析 ( 需求定义) 。即理解和表达用户对程序功能的需求，明确程序的 总任务这项工作也叫做建立程序系统的规格说明。 二、总体设计。按照程序的要求，把总任务分解为一些功能相对独立的子任 务 ( 目 标)的组合。分解工作可以反复进行，以达到每个子目 标只专门完成单一 的逻辑功能。因此总体设计就是对总任务进行分解，以确定程序的模块结构和各 模块的功能。 三、模块设计 ( 详细设计) 。对于以上目 标，按照它们各自的功能要求，逐 一明确 “ 怎么做”即给出其算法。 四、编码。将算法用计算机可以识别的语言适当地描述出来，即编程序。 五、验证或测试。程序证明，就是使自己和别人都能确信程序正确的论述。 这种意义下的证明，正如k n u t h 所说，实际上是指一种理解。证明可以是从公理 出发的形式推导，也可以是非形式的。 从以卜 步骤可以发现，自 顶向下逐步求精的方法只适用于逻辑关系简单的问 题。对那些逻辑关系复杂的子目 标 ( 模块或算法) 用自 顶向下的方法往往就难以 奏效。因此需要研究新的算法程序开发方法解决这一问 题。 1 . 2 . 2 形 式 化软 件开 发方 法 按传统软件开发方法设计与开发的软件产品， 尤其是要求高可靠性的实时控制软 件和军用软件 ( 包括顺序、并行和实时软件) 等大型软件系统，普遍存在着系统 正确性及可靠性难以保证等问 题，且难于实现软件自 动化。八十年代以 来，形式 r a d l 一 ) a o l a自 动程序转换系统研究与实现 化软件开发方法的研究及应用为解决上述问题找到了一条有效的途径，使用形式 化方法开发软件可以提高软件的可读性、可靠性和可维护性以及软件的开发效 率，并为实现软件开发的自 动化奠定基础。 软件开发的形式化方法是以一般形式化方法为基础的。形式化方法为计算机 系统的规约、 实现和验证提供了合理的数学基础， 首先对系统进行独立于实现的、 基于一定形式化语义的抽象描述，然后经过逐步求精及变换，利用规约的数学特 j性 检验其一致性，直至生成最终的软件系统。其优点在于它严格、精确地定义了 用户需求，形式化规约的求精过程具有可推导、易证明的特性，从而有利于保证 程序的正确性和实现软件自 动化。 尤其适宜于高安全性系统的开发，这也是形式 化方法目 前最主要的应用领域。 但是，形式化方法要求使用者具有较好的数学背 景，因而不便于最终用户参与开发过程，阻碍了它的进一步发展。另外，某些形 式化方法缺乏描述软件结构的强有力机制，对大型软件的开发不太理想。 一个形式化的软件开发方法一般包括一套思维方法、一套描述方法、一种开 发手段 ( 如规范描述的原则、程序开发的一般过程、描述语言等)和支持工具， 使开发者能利用数学概念和表示方法恰当合理地构造形式规范，根据开发过程的 框架及设计原则进行规范描述和系统化的设计求精，并使用证明的概念对规范的 性质和设计步骤进行分析和验证;方法还应该有工具的支持，使开发过程可行且 高效。 夸 1 . 2 . 3 形 式 化 软件开发 方法的 分 类 形式化方法按其形式化程度来分， 主要有两种: 完全形式化方法和部分形式化 方法，5 。 1 、完全形式化方法。 对于一个给定的算法程序设计问题， 先用符号化的规范描述语言，写出这个 问题的形式化规范， 然后采用变换方法， 将问题的形式规范变换成可执行的程序。 变换的开始、中间 到结束、产物是一符号串， 这种形式化方法称为完全形式化方 法。使用完全形式化方法产生程序的过程可以用计算机机械地产生。但目 前用这 方法只能产生没有创造性劳动的简单程序。 r a d l 一 ) a o l a自 动程序转换系统研究与实现 化软件开发方法的研究及应用为解决上述问题找到了一条有效的途径，使用形式 化方法开发软件可以提高软件的可读性、可靠性和可维护性以及软件的开发效 率，并为实现软件开发的自 动化奠定基础。 软件开发的形式化方法是以一般形式化方法为基础的。形式化方法为计算机 系统的规约、 实现和验证提供了合理的数学基础， 首先对系统进行独立于实现的、 基于一定形式化语义的抽象描述，然后经过逐步求精及变换，利用规约的数学特 j性 检验其一致性，直至生成最终的软件系统。其优点在于它严格、精确地定义了 用户需求，形式化规约的求精过程具有可推导、易证明的特性，从而有利于保证 程序的正确性和实现软件自 动化。 尤其适宜于高安全性系统的开发，这也是形式 化方法目 前最主要的应用领域。 但是，形式化方法要求使用者具有较好的数学背 景，因而不便于最终用户参与开发过程，阻碍了它的进一步发展。另外，某些形 式化方法缺乏描述软件结构的强有力机制，对大型软件的开发不太理想。 一个形式化的软件开发方法一般包括一套思维方法、一套描述方法、一种开 发手段 ( 如规范描述的原则、程序开发的一般过程、描述语言等)和支持工具， 使开发者能利用数学概念和表示方法恰当合理地构造形式规范，根据开发过程的 框架及设计原则进行规范描述和系统化的设计求精，并使用证明的概念对规范的 性质和设计步骤进行分析和验证;方法还应该有工具的支持，使开发过程可行且 高效。 夸 1 . 2 . 3 形 式 化 软件开发 方法的 分 类 形式化方法按其形式化程度来分， 主要有两种: 完全形式化方法和部分形式化 方法，5 。 1 、完全形式化方法。 对于一个给定的算法程序设计问题， 先用符号化的规范描述语言，写出这个 问题的形式化规范， 然后采用变换方法， 将问题的形式规范变换成可执行的程序。 变换的开始、中间 到结束、产物是一符号串， 这种形式化方法称为完全形式化方 法。使用完全形式化方法产生程序的过程可以用计算机机械地产生。但目 前用这 方法只能产生没有创造性劳动的简单程序。 r a d l 一 a p l a 自 动程序转换系统研究与实现 2 、部分形式化方法。 对于给定算法程序设计问题，先写出该问题的形式化规范，然后使用形式化 和非形式化相结合的方法，开发或证明算法程序正确，这种方法常称为部分形式 化方法或数学家的形式化方法。使用这种类型的形式化方法常常可以设计和证明 一类相当复杂的算法程序和软件。目 前在各类数学和程序设计方法学专著和教材 中使用的方法就是属于部分形式化方法。使用这种方法进行软件或算法程序设计 或证明时，非形式化方法不能够由 计算机机械地进行。 由前面的叙述可知，软件开发的形式化方法作为一般形式化方法的特例，也 存在其固有局限性，因此软件开发过程不可能完全形式化。所以，目 前软件开发 的形式化方法主要是以部分形式化方法为主。 形式化软件开发方法大致可分为以 下五类4 5 1 基于模型的方法。给出系统 ( 程序)状态和状态变换操作的显式但亦是 抽象的定义，但对于并发没有显示的表示，z 和v d m 即属于该类方法。 2 ，代数方法。通过联系不同操作间的行为关系而给出操作的隐式定义，而 不是定义 状态。同 样， 它亦未给出并发的显式表示， 如0 叮，c l e a r 方法。 3 .过程代数方法。给出并发过程的一个显式模型，并通过过程间允许的可 观察的通讯上的限制 ( 约束)来表示行为，如:c s p . c c s . 4 .基于逻辑的方法。有很多方法采用逻辑来描述系统的特性，包括程序行 为的低级规范和系统时间行为的规范，如:时态逻辑。 5 基于网络的方法。根据网 络中的数据流显式的给出系统的并发模型，包 括数据在网中从一个节点流向另一个节点的条件。如: p e t r i 网、谓词变换网。 1 . 3 国内外形式化方法研究现状 l 3 . 1 v d m 方法 v d m ( t h e v i e n n a d e v e l o p m e n t m e t h o d 维也纳开发方法) 是一种使用较早、 应 用较广的基于模型的形式化开发方法，也是当前较为成熟的形式化开发方法之 。七十 一 年代初由工 b m 公司的c . b . j o n e s 等在维也纳开发出其早期形式。 r a d l 一 a p l a 自 动程序转换系统研究与实现 2 、部分形式化方法。 对于给定算法程序设计问题，先写出该问题的形式化规范，然后使用形式化 和非形式化相结合的方法，开发或证明算法程序正确，这种方法常称为部分形式 化方法或数学家的形式化方法。使用这种类型的形式化方法常常可以设计和证明 一类相当复杂的算法程序和软件。目 前在各类数学和程序设计方法学专著和教材 中使用的方法就是属于部分形式化方法。使用这种方法进行软件或算法程序设计 或证明时，非形式化方法不能够由 计算机机械地进行。 由前面的叙述可知，软件开发的形式化方法作为一般形式化方法的特例，也 存在其固有局限性，因此软件开发过程不可能完全形式化。所以，目 前软件开发 的形式化方法主要是以部分形式化方法为主。 形式化软件开发方法大致可分为以 下五类4 5 1 基于模型的方法。给出系统 ( 程序)状态和状态变换操作的显式但亦是 抽象的定义，但对于并发没有显示的表示，z 和v d m 即属于该类方法。 2 ，代数方法。通过联系不同操作间的行为关系而给出操作的隐式定义，而 不是定义 状态。同 样， 它亦未给出并发的显式表示， 如0 叮，c l e a r 方法。 3 .过程代数方法。给出并发过程的一个显式模型，并通过过程间允许的可 观察的通讯上的限制 ( 约束)来表示行为，如:c s p . c c s . 4 .基于逻辑的方法。有很多方法采用逻辑来描述系统的特性，包括程序行 为的低级规范和系统时间行为的规范，如:时态逻辑。 5 基于网络的方法。根据网 络中的数据流显式的给出系统的并发模型，包 括数据在网中从一个节点流向另一个节点的条件。如: p e t r i 网、谓词变换网。 1 . 3 国内外形式化方法研究现状 l 3 . 1 v d m 方法 v d m ( t h e v i e n n a d e v e l o p m e n t m e t h o d 维也纳开发方法) 是一种使用较早、 应 用较广的基于模型的形式化开发方法，也是当前较为成熟的形式化开发方法之 。七十 一 年代初由工 b m 公司的c . b . j o n e s 等在维也纳开发出其早期形式。 r a d l 一 a p l a 自 动程序转换系统研究与实现 2 、部分形式化方法。 对于给定算法程序设计问题，先写出该问题的形式化规范，然后使用形式化 和非形式化相结合的方法，开发或证明算法程序正确，这种方法常称为部分形式 化方法或数学家的形式化方法。使用这种类型的形式化方法常常可以设计和证明 一类相当复杂的算法程序和软件。目 前在各类数学和程序设计方法学专著和教材 中使用的方法就是属于部分形式化方法。使用这种方法进行软件或算法程序设计 或证明时，非形式化方法不能够由 计算机机械地进行。 由前面的叙述可知，软件开发的形式化方法作为一般形式化方法的特例，也 存在其固有局限性，因此软件开发过程不可能完全形式化。所以，目 前软件开发 的形式化方法主要是以部分形式化方法为主。 形式化软件开发方法大致可分为以 下五类4 5 1 基于模型的方法。给出系统 ( 程序)状态和状态变换操作的显式但亦是 抽象的定义，但对于并发没有显示的表示，z 和v d m 即属于该类方法。 2 ，代数方法。通过联系不同操作间的行为关系而给出操作的隐式定义，而 不是定义 状态。同 样， 它亦未给出并发的显式表示， 如0 叮，c l e a r 方法。 3 .过程代数方法。给出并发过程的一个显式模型，并通过过程间允许的可 观察的通讯上的限制 ( 约束)来表示行为，如:c s p . c c s . 4 .基于逻辑的方法。有很多方法采用逻辑来描述系统的特性，包括程序行 为的低级规范和系统时间行为的规范，如:时态逻辑。 5 基于网络的方法。根据网 络中的数据流显式的给出系统的并发模型，包 括数据在网中从一个节点流向另一个节点的条件。如: p e t r i 网、谓词变换网。 1 . 3 国内外形式化方法研究现状 l 3 . 1 v d m 方法 v d m ( t h e v i e n n a d e v e l o p m e n t m e t h o d 维也纳开发方法) 是一种使用较早、 应 用较广的基于模型的形式化开发方法，也是当前较为成熟的形式化开发方法之 。七十 一 年代初由工 b m 公司的c . b . j o n e s 等在维也纳开发出其早期形式。 r a d l 一 a p l a 自 动程序转换系统研究与实现 v d m 包含一个称为 “ v d m - s l ( v d m s p e c i f i c a t i o n l a n g u a g e ) 的规约语言; 一组用于在抽象的需求规约和代码级的详细设计规约间建立链接的数据求精和 操作求精规则:一套证明理论，其中可用严格的参数来操作指定系统的属性和保 证设计决策的正确性t27) v d m 方法提供了程序正确性证明的依据， 使规格说明描述简练、 精确。 但v d m 也存在以下不足之处:v d m 的每一个求精步骤都是上一个求精步骤的具体化，由 于各个求精步骤之间并不存在着严格的推导关系，因此整个的算法推导过程不够 严 谨; 其正 确性是 在算 法推导完成后再回头 验证其每一求 精步骤来保证的， 若 有 错误又得重新推导算法，然后再对推导过程进行重新验证;同时v d m 的每一求精 步骤都包含 “ 数据精化”和 “ 操作分解”两个不同的过程， 将数据结构和算法分 离，这些都导致使用v d m 来开发算法效率不够高。 尽管v d m 的规约语言已由工 s o 标准化并得到很多成熟的工具的支持，但目 前 仍没有一个满意的工具来支持验证。 1 . 3 . 2 z 方法 z方法是以程序公理语义为基础的形式化开发方法，它的规范说明语言基于 模式演算，提供了丰富的操作运算，但不可执行。z语言有模式匹配的符号，使 用了具有强大功能的操作符，还使用了一些非形式化的英语解释，给出的规范说 明比较短，易于阅读和理解。 z语言己经成为世界最流行的形式化规约语言。现有大量的工具支持，它们 主要集中于规约的编辑和显示以 及语法和类型检查方面，也有些工具支持规约的 推理和精化。l 匕 较有影响的工具有:f o r m a l i s e r , p r o o f p o w e r , z o l a , c a d i z , f o r m o o z , z / e v e s 等。 z 语言存在以 下一些缺陷: ( 1 ) z 语言对大型系统的模块化能力不足。 ( 2 ) 没有提供重用机制。 ( 3 ) z 语言难以 用计算机直接处理。 ( 4 ) 不支持软件开发的全过程。 r a d l 一 a p l a 自 动程序转换系统研究与实现 v d m 包含一个称为 “ v d m - s l ( v d m s p e c i f i c a t i o n l a n g u a g e ) 的规约语言; 一组用于在抽象的需求规约和代码级的详细设计规约间建立链接的数据求精和 操作求精规则:一套证明理论，其中可用严格的参数来操作指定系统的属性和保 证设计决策的正确性t27) v d m 方法提供了程序正确性证明的依据， 使规格说明描述简练、 精确。 但v d m 也存在以下不足之处:v d m 的每一个求精步骤都是上一个求精步骤的具体化，由 于各个求精步骤之间并不存在着严格的推导关系，因此整个的算法推导过程不够 严 谨; 其正 确性是 在算 法推导完成后再回头 验证其每一求 精步骤来保证的， 若 有 错误又得重新推导算法，然后再对推导过程进行重新验证;同时v d m 的每一求精 步骤都包含 “ 数据精化”和 “ 操作分解”两个不同的过程， 将数据结构和算法分 离，这些都导致使用v d m 来开发算法效率不够高。 尽管v d m 的规约语言已由工 s o 标准化并得到