（计算机软件与理论专业论文）radl→apla程序生成系统及其可靠性研究.pdf

摘要 随着信息技术的发展，计算机软件已经应用到了生活的各个方面，软件的可 靠性也越来越受到关注，人们不仅对安全性至关重要软件系统提出了高可靠的要 求，而且对于普通的应用软件也希望尽可能不出错。众所周知，传统的软件测试 手段并不能满足人们对高质量软件的要求，而形式化开发方法因其具有严格的理 论基础，可以用于开发正确、高效的程序。 本文实现了由r a d l 算法程序到a p l a 程序的映射过程，其中使用r a d l 语言来 描述由p a r 方法开发的算法程序，选用a p l a 语言作为映射的目标语言。为了使 这种映射过程具有高可靠性，本文采用形式化的描述方法分别从词法、语法和语 义三个层次精确地定义r a d l 语言，保证了r a d l 语言描述的程序正确地反映了推 导所得算法的逻辑思想；并且基于r a d l 语言属性文法，以r a d l 语法产生式作为 最小映射单元，定义了r a d l 语言映射单元到a p l a 语言语义单元的语义等价映射 规则；同时采用形式化推导方法，根据r a d l 语言词法、语法、语义及r a d l 算法 程序到a p l a 程序的映射规则的定义，推导出r a d l 语言词法分析、语法分析和语 义分析实现的代表性算法。基于形式化推导的语法制导翻译的方法，将r a d l 算 法程序按映射规则映射成a p l a 程序，保证了所实现的系统是在相关理论的指导 下进行的，并且高可靠的实现了相关理论的要求。 本文主要做了如下几方面工作，其中某些方面具有一定的创新性： 1 分别形式化的定义r a d l 语言的词法、语法和语义。 2 以r a d l 语法产生式为单元，系统定义由r a d l 生成a p l a 程序的生成规则。 3 采用形式化推导方法得到生成系统的核心代表性算法。 关键词：p a r 方法；r a d l ；程序生成；算法推导 a b s t r a c t w i t ht h ed e v e l o p m e n to fi n f o r m a t i o nt e c h n o l o g y , c o m p u t e rs o f t w a r eh a sb e e n a p p l i e dt oe v e r ya s p e c t ，a n dp e o p l ep a ym o r e a n dm o r ea t t e n t i o nt ot h er e l i a b i l i t yo f s o f t w a r e u s e r sn o to n l yr e q u i r eh i g hr e l i a b i l i t yf o rs a f e t y - c r i t i c a ls o f t w a r es y s t e m ， b u ta l s oh o p et h a tg e n e r a la p p l i c a t i o ns o f l r w a r ea l s od o e s n tg ow r o n g a sw ea l lk n o w , t r a d i t i o n a ls o f t w a r e t e s t i n gc a nn o tb e a b l et o s a t i s f yp e o p l e s d e m a n d sf o r h i g h - q u a l i t ys o r w a r e o nt h ec o n t r a r y , f o ri t sr i g o r o u st h e o r y , f o r m a ld e v e l o p m e n t m e t h o d o l o g yc a nd e v e l o pc o r r e c ta n de f f i c i e n tp r o c e d u r e s t h i sp a p e rh a sa c h i e v e dt h em a p p i n go fr a d la l g o r i t h mt oa p l ap r o g r a m t h e p a p e ra d o p t sr a d lt od e s c r i b et h ea l g o r i t h md e v e l o p e db yp a rm e t h o d ，a n dc h o o s e s a p l aa st h et a r g e tl a n g u a g eo fm a p p i n g i no r d e rt ol e tt h em a p p i n gp r o c e s sh a v eh i g h r e l i a b i l i t y , t h i sp a p e ru s e s f o r m a lm e t h o dt od e f i n et h es o u r c el a n g u a g e r a d l l a n g u a g ep r e c i s e l yi nt h r e el e v e l sr e s p e c t i v e l y , w h i c ha r em o r p h o l o g y , s y n t a xa n d s e m a n t i c s i ta s s u r e st h a tt h ea l g o r i t h md e s c r i b e db yr a d lr e f l e c t sa c c u r a t e l yt h e l o g i c a lt h i n k i n go fa l g o r i t h md e r i v e d b a s e do na t t r i b u t eg r a m m a ro fr a d ll a n g u a g e a n dl e t t i n gr a d ls y n t a xp r o d u c t i o nr u l e sa st h em i n i m u mu n i to fm a p p i n g ，t h ee q u a l m a p p i n gr u l ei sd e f i n e d a tt h es a m et i m e ，a c c o r d i n gt ot h em o r p h o l o g y , s y n t a x ， s e m a n t i c so fr a d la n dt h ed e f i n i t i o no fm a p p i n gr u l e so fr a d lt oa p l a ，f o r m a l d e r i v a t i o nm e t h o di sa d o p t e dt od e r i v et h ec o r ea l g o r i t h mo fl e x i c a la n a l y s i s ，g r a m m a r a n a l y s i sa n ds e m a n t i ca n a l y s i so fr a d l u n d e rt h em e t h o db a s e do nf o r m a ld e r i v ea n d s y n t a xd i r e c t e dt r a n s l a t i o n ，r a d lp r o g r a mi sm a p p e dt oa p l ap r o g r a mb ym a p p i n g r u l e s ，a n di ta s s u r e st h a tt h es y s t e mi si nt h eg u i d a n c eo fr e l a t i o n a lt h e o r ya n dr e a l i z e s t h ed e m a n d so fr e l e v a n tt h e o r yi nh i 曲r e l i a b i l i t y t h i sp a p e rm a k e st h r e ei n n o v a t i v ej o b sa sf o l l o w i n g ： 1 d e f i n em o r p h o l o g y , s y n t a xa n ds e m a n t i c so fr a d ll a n g u a g er e s p e c t i v e l y ； 2 u s er a d ls y n t a xp r o d u c t i o na st h em i n i m u mu n i t ，d e f i n et h eg e n e r a t i o nr u l e s o fr a d lt oa p l as y s t e m i c a l l y ； 3 a d o p tf o r m a ld e r i v a t i o nm e t h o dt oo b t a i nt h ec o r ea l g o r i t h m so fs y s t e m k e yw o r d s ：p a rm e t h o d ；r a d l ；p r o g r a mg e n e r a t i o n ；d e r i v ea l g o r i t h m 独创性声明 本人声明所呈交的学位论文是本人在导师指导下进行的研究工 作及取得的研究成果。据我所知，除了文中特别加以标注和致谢的地 方外，论文中不包含其他人已经发表或撰写过的研究成果，也不包含 为获得或其他教育机构的学位或证书而使用过的材料。与我一同工作 的同志对本研究所做的任何贡献均已在论文中作了明确的说明并表 示谢意。 学位论文作者签名：签字日期：年 月 日 学位论文版权使用授权书 本学位论文作者完全了解江西师范大学研究生院有关保留、使用 学位论文的规定，有权保留并向国家有关部门或机构送交论文的复印 件和磁盘，允许论文被查阅和借阅。本人授权江西师范大学研究生院 可以将学位论文的全部或部分内容编入有关数据库进行检索，可以采 用影印、缩印或扫描等复制手段保存、汇编学位论文。 ( 保密的学位论文在解密后适用本授权书) 学位论文作者签名： 签字日期：年月 日 导师签名： 签字日期：年 月 日 r a d l - ) a p l a 程序生成系统及其可靠性研究 第1 章引言 1 1 研究背景 随着信息化时代的来临，计算机已经深入到人们生活与生产中的各个领域。 各种应用软件的需求急剧增加，而传统的软件开发方法及使用软件开发后的测试 来保证软件的正确性，使得软件的开发效率及其可靠性都远远不能满足社会的需 要。人们不仅仅需要更多的应用软件，还对软件的可靠性有更高的要求。尤其在 安全性至关重要的领域，软件系统的可靠性关乎人们的生命及财产安全，频繁出 现的软件故障给人们带来了巨大损失。形式化的开发方法通过严格的数学化定 义软件的需求及处理过程，精确的刻画软件的本质特征，一直被认为是提高软件 可靠性、生产效率和实现软件自动化的重要途径。 形式化开发方法建立在严格的数学理论之上，需要使用者具有扎实的数学基 础和较高的数学素养，正因为如此，造成了形式化开发方法在很长一段时间内都 难以推广。随着一系列形式化支撑工具，如规约描述语言、定理证明器及模型检 测器等，使得程序员可以不必要精通形式化理论，也不必要精通很深的定理证明 理论就可以享受使用形式化开发带来的好处。形式化开发方法已经走出了实验 室，开始在工业中得到广泛的应用【2 】。 形式化开发方法虽然已经开始得到应用，但由于目前形式化方法及其支撑工 具自身存在着一定的局限性及现实生活中各类应用系统的复杂性，使得欲使用形 式化方法贯穿整个系统的开发全过程就显得力不从心。综观应用系统的整个开发 过程，或多或少需要人的主观创造性劳动支持，如系统需求的定义等，这类劳动 不可能由机器自动实现，一定需要人的参与。这就迫使在使用形式化方法时，要 求使用者考虑开发过程中哪些任务是q g , l 造性的，哪些任务是创造性的。q g , l 造 性劳动实现过程可以不需要人的参与，其机械化程度高，较容易使用机器来实现， 对于创造性劳动，可以通过经验积累，找出问题内在规律，将创造性劳动转化为 q g , l 造性劳动，以最大限度的将人的劳动从机械的非创造性劳动中解放出来，从 而提高软件的可靠性及开发效率。但是，使用支撑工具来实现软件开发中的非创 造性劳动，从一定程度上避免了人为错误的发生，并且，只要通过有效的手段来 保证支撑工具的正确性，那么通过使用该支撑工具所实现的非创造性劳动是能满 足问题的形式定义的，从而提高了软件开发的可靠性。 程序生成技术是目前得到了较广泛应用的一种形式化开发支撑技术口1 ，主要 根据输入的断言或其他表现形式的形式化需求，自动得到满足需求的可执行代码 硕士学位论文 或某种所需语言的源代码，辅助实现了系统编码阶段的非创造性劳动，提高了程 序开发效率和质量，如p a r 方法的系列支撑平台等都属于这一类的形式化支撑工 具。 1 2 研究内容 本文以p a r 方法开发算法程序理论为基础，结合程序生成技术的实际，将 主要开展以下几方面的工作： 1 根据已有的r a d l 语言描述材料，总结r a d l 语言的特性及适用范围。 2 定义r a d l 语言的词法、语法和语义的形式化规范。为生成系统定义一个 精确的输入。 3 研究r a d l 语言和a p l a 语言两者间的语义关系，根据语义等价原则确定r a d l 语言到a p l a 语言的生成规则。 4 根据定义的r a d l 语言的词法、语法和语义信息，实现对r a d l 语言的理解， 同时根据定义的生成规则，实现生成系统。 5 探讨r a d l - - - ) a p l a 程序生成系统的可靠性。 6 开发实例，试运行生成系统。 1 3 本文组织 本文共分六章进行阐述，具体组织如下： 第一章，引言部分，阐述本文的研究背景及研究内容。 第二章，概述现有的形式化开发方法及其支撑工具，并对各种方法之间的关 系进行探讨。 第三章，详细定义r a d l 语言。采用形式化方法精确地定义r a d l 语言的词法、 语法及语义信息。 第四章，设计r a d l - - ) a p l a 程序生成系统并实现。 第五章，探讨r a d l 专a p l a 程序生成系统的可靠性。 第六章，对本文的工作进行总结，同时对接下来的工作的前景做出展望。 2 r a d l - - - ) a p l a 程序生成系统及其可靠性研究 第2 章形式化开发方法与形式化支撑工具 2 1 形式化方法概述 在软件开发的需求分析、规格说明、设计、编码、系统集成、测试、文档生 成直至维护的各阶段，凡是采用严格的数学语言、具有精确的数学语义的方法都 称为形式化方法【引。 形式化方法采用精确、严格的数学语言定义系统，从而精确描述系统的需求、 结构和处理逻辑等。现有的形式化开发方法普遍所采取的数学理论主要包括代 数、过程代数和数理逻辑等【5 j 。目前，根据所采用的数学理论，有许多相应的形 式化支撑工具可以选择【2 4 l 【2 5 j 【2 6 j 【2 7 1 。 采用形式化的方法开发系统，可以无歧义的描述系统的逻辑功能，以支持系 统设计者与实现者之间的无差异交流；可以严格的推导出程序的执行流程，以保 证编写程序的质量；可以详细的验证编写的程序正确与否，以减少系统测试人员 的工作量；甚至可以支持由设计到实现的全过程自动操作，以提高软件的开发效 率和可靠性。 形式化开发方法正在影响着、改变着原有的系统的开发方法。形式化方法贯 穿于整个软件系统的生命周期，加深了原有瀑布模型的内涵；形式化方法支持程 序的自动化，为螺旋模型( 原型法) 提供了更快捷的途径。 虽然形式化方法在软件开发过程中正在扮演着越来越重要的角色，但其自身 仍存在一些短时间内难以克服的缺陷： ( 1 ) 不能用形式化的方法将非形式化的感知事物转变成形式化的逻辑事 物。我们可以使用形式化的方法验证或推导程序满足形式化的规约，但是不能形 式化的证明或推导形式化的规约是否满足人们意识中的需求。 ( 2 ) 形式化的开发方法是基于理想的抽象机而存在，但是抽象机与具体运 行程序的实际机器之间很难一致。 ( 3 ) 形式化方法受人的理论认知水平的影响。使用形式化方法需要具有一 定的数学基础，而目前的系统开发人员大都是采用靠经念及自身理解的工作方 式，对形式化开发方法的应用将产生阻碍。 由此，系统开发过程中不能盲目的依赖形式化开发方法。需要正确的区分形 式化方法的作用领域，并根据自身的需要在系统开发过程中选择使用完全形式 化、部分形式化或不采用形式化的开发方法。 虽然形式化开发方法具有一些不足之处，但形式化方法正在将传统的程序开 3 硕士学位论文 发方法由经验转向科学理论，由手工创造转变为机械自动化。其必将影响系统开 发理论研究，将形式化方法应用于软件开发的全过程将是未来系统开发的努力方 向，也是解决“软件危机”的有效途径之一。 2 2 现有形式化开发方法 2 2 1b j - r a b r i a l 从上世纪8 0 年代开始b 方法的研究，b 方法是一种“基于模型 的软件构造方法。b 方法对软件进行严格规范描述，并提供机制实现从严格规范 到最终程序的演化( 即精化) ，以及对这一过程的自动支持。 b 方法的基本机制是抽象机( 抽象机记法形式( a m n ，a b s t r a c tm a c h i n e n o t a t i o n ) ) ，该方法所表达的软件系统由一些抽象机组成，每一个抽象机器包含 一些数据，提供一些操作。数据和操作被封装在机器里，数据通过有关机器的操 作去使用。 抽象机中的数据是使用一些数学概念，例如：集合、关系、函数、序列和树 等来表示。这些数据必须遵守通过特定条件定义的静态法则，这些条件称为不变 式。 抽象机中操作的规范用一段不能执行的伪代码表述，其中不包含任何顺序性 或者循环。在一段伪代码里，每个操作描述为一个前条件和一个原子动作。前条 件表述一种必不可少的条件，在不满足它的情况下操作就不能执行。原子动作通 过一种广义替换( 广义代换语言( g s l ，g e n e r a l i z e ds u b s t i t u t i o nl a n g u a g e ) ) 的 方式进行形式化。 b 方法的开发过程是将抽象机的初始模型( 它的规范) 精化为一个可执行的 模块( 它的实现) 。精化过程以三种不同的方式进行：删除伪代码中不可执行的 语句( 前条件和选择) ；引进程序设计的典型控制结构( 顺序性和循环) ；以及将 数学的数据结构( 集合、关系、函数、序列和树等) 变换到可能编程的其他结构 ( 简单变量、数据或文件等) 。为了控制上述精化过程，对抽象机的精化将分步 进行。在其中的每一步，初始抽象机都要整体性地重构。由此，需要控制精化的 步骤数，随着层次的增加，复杂性就会变得过高。这时就应该建议将一个精化分 解为若干更小的片段。这样，一个抽象机的最后精化将通过另外的一个或者几个 抽象机的规范实现，而那些规范本身又能进一步精化。一个抽象机的最终精化可 以很容易地变换到一种或者几种程序设计语言。 由于某些通用抽象机的实现，完全可以在精化之前就已经存在。为此，b 方 法提供了一些预定义的抽象机，它们组成了一个抽象机的库，其作用就是封装起 一些最典型的数据结构。对于一个确定的项目，可以扩充这个库，以形成一个基 4 r a d l - ) a p l a 程序生成系统及其可靠性研究 础，基于它们去实现未来更高层次的抽象机【1 们。 2 2 2d e sig n w a r e d e s i g n w a r e 是美国k e s t r e l 研究所s m i t h 教授在多年算法设计自动化研究工 作的基础上提出的系列软件开发系统之一。该系列开发系统包括：s p e c w a r e ， d e s i g n w a r e ，p l a n w a r e 。这三种方法统一于同一个形式化框架中，分别关注于软 件工程的不同方面：s p e c w a r e 主要涉及到形式化规约的构建；d e s i g n w a r e 关注 于设计知识的管理及应用；p l a n w a r e 则用于构建特定调度领域的应用系统。 用d e s i g n w a r e 开发程序时，先要借助s p e c w a r e 系统完成规约的构造，然后 由d e s i g n w a r e 对规约进行算法求精，程序优化，最后，再利用s p e c w a r e 完成代 码生成的工作。 d e s i g n w a r e 以范畴论作为数学理论基础，其中的规约由数据、运算和运算应 满足的约束组成，d e s i g n w a r e 利用范畴论中的态射解释规约变换，通过求余极限 完成规约组合。利用余极限运算基于已有的精化构造新的精化。在精化的过程中， d e s i g n w a r e 需要一个算法设计知识库的支持【7 】。 d e s i g n w a r e 的目标是给算法设计者提供一个抽象、可重用的与特定领域无关 的设计知识精化库以及一些自动化操作，帮助设计者完成算法设计。可重用设计 知识分类库中涉及算法设计、数据求精以及表达式优化技术等方面的设计知识， 并将它们表示成精化规则的形式加以存储。为了能高效地应用设计知识， d e s i g n w a r e 将抽象的可重用精化库组织成一个按类别分类形式，使得设计者能方 便地对精化库进行访问以及基于该库来构建求精。在这里涉及的关键思想是分 类，通过将设计知识分类，缩减了可选择的实现集合的范围，并且按照分类提供 的顺序进行逐步精化，将逐渐加强对设计的约束。 到目前为止，d e s i g n w a r e 中的精化规则主要集中在描述算法、数据以及优化 方面的设计知识上。 2 2 3v d m ( v i e n n ad e v e i o p m e n tm e t h o d ) v d m 是于上世纪7 0 年代由m 公司维也纳实验室的研究小组提出的。 v d m 技术的基本思想是运用抽象数据类型、数学概念和符号来定义数据及规定 操作或函数的功能，使软件系统的功能描述在抽象级上进行，完全摆脱了实现细 节，这样为软件实现者提供了很大的灵活性，此外，这种形式化规格说明还为程 序正确性证明提供了依据 5 】。 v d m 基于一个形式规约语言“v d m s l ”( v d ms p e c i f i c a t i o nl a n g u a g e ) 。 在使用v d m 的开发过程中，先定义一个抽象模型，逐步将此抽象模型转化为计 算机上的具体实现。从抽象模型到具体实现要经历多步转化，其中每一步都包含 着“数据具体化( d a t ar e i f i c a t i o n ) ”和“操作分解( o p e r a t i o nd e c o m p o s i t i o n ) 硕士学位论文 二个方面。经过多步“数据具体化 最终将抽象数据类型转换成具体的数据结构。 经过多步“操作分解”最终将抽象( 隐含) 的操作或函数的规约转换成可以直接 由具体的计算机语言实现的算法。 每一步的“数据具体化( 逐步求精( s t e p w i s er e f i n e m e n t ) ) 都是为规约中使 用的抽象数据类型找一个相对具体的表示方式。每次对一抽象数据的具体化，都 会使其表现形式发生改变，为了保证具体化后的数据与原抽象数据一致，就需要 定义一个找回函数( r e t r i e v ef u n c t i o n ) 来表示具体化前后数据间的对应关系，而 数据具体化的正确性就有赖于找回函数的正确性。 同时，随着数据表现形式的改变，必须要更改相应的操作和函数以作用于新 的数据表现形式。新的操作和函数必须保证与数据转变前的一致性。 由上述v d m 的开发过程可知，v d m 适用于基于模型系统的开发。随着面 向对象技术和并发技术的广泛应用，v d m 也派生出v d m + + 以支持这二种技术。 2 2 47 z 是在j ra b r i a l 等的开创性工作下，由英国牛滓大学的程序设计研究小组 ( p g r ，p r o g r a m m i n gr e s e a r c hg r o u p ) 于上世纪8 0 年代所开发一种形式语言。 z 语言是基于集合理论和一阶谓词逻辑的形式化规范描述语言，支持数据抽 象和过程抽象，并称之为表示抽象和操作抽象。在表示抽象中，数据从数据结构 的表示细节抽象出来，使用关系、函数、集合、序列、包等抽象的数据类型，这 些类型构成z 语言的类型系统；而操作抽象则描述了在数据抽象中所引入的数据 上的抽象算法和操作。 在z 中，表示抽象通过类型定义、全局变( 常) 量以及状态空间声明来进行 表述；操作抽象通过函数和基于一阶谓词逻辑的操作来表述。 模式( s c h e m a ) 是z 语言的基本描述单位。通过z 表示的软件系统主要由 若干个模式构成，这些模式刻画了系统的静态性质和动态行为。与之相对应，模 式分为两类：状态模式和操作模式。状态模式定义了目标软件系统某一部分的状 态空间及其约束特性，它通过相应抽象数据类型的变量以及在它们上面所定义的 一些约束关系来进行描述。操作模式描述了系统某部分的行为特征，它通过谓词 判定描述给出新的对象或操作的语义约束，来定义该部分的某种操作的特性。 每个模式都有惟一的名字，并包括一个声明部分和一个断言或谓词部分。模 式的声明部分引入了某些类型的变量，这些变量为该模式内的局部变量；断言部 分描述了在这些局部变量之间，或者局部变量与全局变量( 常量) 之间的逻辑关 系。 在z 语言中，定义了模式的运算，可以利用这些模式的运算，将旧的z 模 式说明组合成新的z 模式，新的z 模式继承其父模式的一切属性和约束。这样， 软件系统的z 模式规格说明可以按一定的层次结构给出。模式的使用为规格说明 6 r a d l - - a p l a 程序生成系统及其可靠性研究 提供了一种演算，通过这种演算，无论多么大型系统的规格说明都可以通过一个 小的部分来构成【5 】。 2 2 5p a r p a r 方法是由薛锦云教授提出的一种统一的、系统的算法程序设计和证明方 法【1 2 】。p a r 方法以谓词逻辑、f l o y d 归纳断言法、d i j k s t r a 的最弱前置谓词和h o a r e 公理语义等程序正确性证明及谓词演算理论为指导，充分运用数据抽象和功能抽 象技术，为软件开发的算法设计阶段提供形式化及自动化支持。为了支持算法设 计的形式化开发及代码自动生成，p a r 方法定义了二种支撑语言：r a d l ( 算法和 规约描述语言) ，a p l a ( 抽象程序设计语言) 。 p a r 方法将分划和递推技术结合起来，从问题的规约( 前后置断言) 出发， 通过谓词演算对规约进行变换，从而将原问题划分成一个或多个与原问题结构相 同的子问题，直到划分得到的子问题可以直接求解为止。为了刻画算法的本质， 忽略与处理逻辑无关的细节，p a r 平台提供了常用的抽象数据类型( 部件库) 。使 用p a r 方法开发算法程序的具体过程可由以下六个步骤组成【l5 】： l 、使用r a d l 语言精确描述求解问题的功能规约，即精确描述算法要完成的 工作。 2 、把问题分解成若干和原问题结构相同但规模更小的子问题，分解可一直 进行下去直至每一个子问题可直接求解。可直接求解的子问题称为最小子问题。 划分是解决复杂问题，得到快速算法的一般策略。很明显，不同的分划策略将导 致不同的算法。 3 、构造问题求解序列的递推关系s i _ f ( s i ) ，并给出递推关系中出现的变量和 函数的初始条件，然后将所有递推关系和初始化条件合并成为一个用算法描述语 言r a d l 描述的抽象算法； 通过上述三个步骤，就可以得到被求解问题使用p a r 方法开发出的递推算 法程序。为了更好的支持程序的正确性证明及程序的自动生成，还将需要进行如 下三个步骤： 4 、基于开发循环不变式的新策略2 8 1 ，开发循环不变式。即基于问题求解序 列的递推关系，确定程序中需要的所有变量，描述每个变量的变化规律或功能。 这些规律或功能就是所需要的循环不变式。 5 、基于所得的r a d l 算法和循环不变式开发由抽象程序设计语言a p l a 书写 的算法程序。在此可使用r a d l - ) a p l a 程序生成系统可以机械地、自动地将使用 r a d l 描述的规约和算法生成a p l a 程序。该生成系统的实现及可靠性研究正是本 文所进行的研究工作。 6 、用p a r 支撑平台的一系列程序生成系统将a p l a 程序变换为其他高级语 言程序，如：c + + 、j a v a 、c 、v b n e t 等f 2 4 】f 2 5 】【2 6 1 【2 7 1 。 7 硕士学位论文 通过上述开发步骤可知，p a r 方法在构造问题规范、适当选取划分方式、量 词变换规则的选用、通过形式推演得到用递推关系表示的算法等方面要求人的参 与，需要发挥人的主观创造力。但是由递推关系到循环不变式及由算法到程序的 开发都属于机械的变换，可以不需要人的干涉，完全可以采用形式化方法自动得 到，即通过构造一个自动支撑工具将这类机械变换工作交由计算机完成。由此 p a r 方法支撑平台中相应的定义r a d l 和a p l a 两种语言以划分p a r 方法开发过 程中的创造性劳动和非创造性劳动。r a d l 语言和a p l a 语言分别是本文研究的源 语言和目标语言，下面对这二种语言作一个简单介绍： ( 1 ) 、r a d l ( r e c u r r e n c e b a s e da l g o r i t h md e s i g nl a n g u a g e ) 语言 r a d l 语言既是算法描述语言，也是规约描述语言。主要用于描述问题的规 约、规约变换规则和算法等。由于r a d l 语言用于描述算法和规约，为了更好地 体现出算法的本质，在r a d l 语言中沿用了算法推导过程的数学语义，即r a d l 算 法程序中引入了传统的数学符号、数学表达式及数学特性，如各语句间的无序性 等。r a d l 语言具有非常丰富的类型系统，提供抽象数据类型机制及功能抽象机 制。 ( 2 ) 、a p l a ( a b s t r a c tp r o g r a m m i n gl a n g u a g e ) 语言 a p l a 语言是为实现算法程序形式化而定义的一种抽象程序设计语言【l l 】。a p l a 语言完全支持抽象数据类型，其中还将常用数据类型定义为预定义数据类型，使 得程序编写简单，极大的提高了程序的可靠性和开发效率。a p l a 程序易于理解 和形式化验证。同时，p a r 平台提供了许多相关的工具，可以非常方便的将由 a p l a 语言书写的程序变换成其它高级语言程序，如：c + + ，j a v a ，c ，v b n e t ， d e p h i 掣2 4 1 【2 5 】【2 6 】【2 7 1 。 由于p a r 方法用递推关系表示算法，保持了数学的透明性，使算法的形式 化推演成为可能。同时，p a r 使用基于原问题的分划原则使得算法减少了许多重 复工作。从而达到较高的效率。许多实例已经证吲2 9 】 3 0 】【3 1 】1 3 2 】【3 3 1 ，p a r 可以发 展成为一种简单实用且高效的算法程序形式化开发方法1 1 2 j 。 基于多个国家级课题的支持，p a r 目前的支撑工具极为丰富，这些支撑工具 被集中统一命名为p a r 平台，具体包括以下几个自动程序生成系统：r a d l - - ) a p l a ， a p l a 专c + + ，a p l a - - ) j a v a ，a p l a - - ) c # ，a p l a 专v b n e t ，a p l a - - ) d e l p h i 掣2 4 】【2 5 】【2 6 】【2 7 1 。 2 3 形式化开发方法分析 b 是一种覆盖了软件开发中从规约说明到编码的开发方法，b 建立在集合论、 最弱前置谓词思想和广义替换、精化、软件的层次体系结构理论的基础上。b 支 持模块化、层次化的开发思想，将整个系统的开发过程看作是一部“抽象机器 的变换过程，其可能是将一部“抽象机器”化分为几部规模较小的“抽象机器。 r a d l - ) a p l a 程序生成系统及其可靠性研究 也可能是通过抽象机的引用将若干部较小的“抽象机器”合并成较复杂的抽象机。 大大提高了系统的重用性和开发效率。b 将系统的开发过程( 即定义程序规约和 对规约的逐步求精) 处于一个统一的数学框架之下，有丰富的支撑工具对其提供 支持。然而，b 方法的本质仍然是自项向下、逐步求精的方法，难以解决复杂的 算法问题瞵j 。 d e s i g n w a r e 基于范畴论及相关数学工具，可以将软件开发过程分解为若干步 骤，这些步骤可以独立开发，最后综合集成为软件系统。采用d e s i g n w a r e 开发 软件系统，在规约描述与组合，规约的逐步精化，可执行代码生成等阶段都有范 畴论工具进行解释，这样就一定程度上保证了最终代码符合初始的规约。同时， d e s i g n w a r e 开发方法将设计知识，包括大量的可重用规约规则、算法设计规则和 表达式优化规则，表示成求精规则并分类存放于数据库中，一方面提高了软件的 重用性，一方面提高了软件开发的效率及可靠性。 d e s i g n w a r e 的算法设计系统不是完全自动化的，它依赖于与专家级用户间的 交互：作为问题求解起点的规约实际上是代数规约，要求用户具有较高的数学素 养，使用起来很不方便；并且d e s i g n w a r e 在算法和数据求精时，需使用余极限 运算，一般的软件开发人员较难掌握，在其算法设计分类库中，存放着与不同算 法设计策略对应的不同程序模式，当遇到一个待求解的实际问题时，具体选用哪 种合适的算法设计策略来解决问题并没有一个有效的标准或规则，需要具有较多 算法设计知识的用户来交互选取，这给提高算法设计自动化的程序带来了困难； 甚至于优化，用户也必须清楚程序的哪个部分可以用什么方法来进行优化，从而 选定需要优化的表达式及恰当的优化规则【8 】。 v d m 使用前置、后置条件定义规约，通过数据的具体化和操作的分解来最 终得到可执行程序，这在一定程度上保证了程序的可靠性，提供了程序正确性证 明的依据，但由于其区别对待数据和操作，使得分解前后规约或者算法的一致性 难以得到保障，同时随着求精的深入，由于要考虑更多的对应操作，使得分解将 越来越难以进行。v d m 的每一个步骤都是上一个求精步骤的具体化，由于各个 求精步骤之间并不存在着严格的推导关系，因此整个算法推导过程不够严谨；其 正确性是在算法推导完成后再回头验证其每一步求精步骤来保证的，若有错误就 必须重新推导算法，然后再对推导过程进行重新验证，这些都导致使用v d m 来 开发算法效率不够高【5 】。 z 语言基于集合理论和一阶谓词逻辑，可以用来准确地描述目标系统。利用 模式和模式演算对目标软件系统的结构和行为特征进行抽象描述，其中状态模式 对目标软件系统的结构特征进行抽象描述，操作模式对目标软件系统的行为特征 进行抽象描述，这是一种具有特色的有效的形式化方法【5 】。但由于没有明确的指 定描述公理，尽管z 提供了一种称为模式的结构，但还不能算是一种开发方法， 9 硕士学位论文 模式的层次结构形成了系统的规格说明，按照创造者的意图，模式之间的联接还 必须用一些非正式的文本加以注释。从而导致z 语言对大型系统的模块化能力不 足，因为在z 语言中，目标软件系统的结构和特征都用模式来描述，随着系统的 增大，模式也会越来越多，而z 语言中没有更加有效的机制来管理这些模式，最 终导致z 规格说明难以阅读。并且z 不支持规格说明的重用，没有提供重用机 制，更是使得开发的效率不副习。 p a r 方法是一种高效的算法设计方法，通过递推关系推导出来的算法总是使 后一步结果建立在前一步结果的基础上，避免了许多重复性的工作和计算，同时 提高了程序的运行效率。p a r 方法不仅可以用来解决一些利用传统算法设计方法 解决的问题，也可以解决部分用传统设计方法不能解决的问题。我们已经利用 p a r 方法开发了一些原来使用分治法、动态规划法和贪心法解决的问题1 2 圳。 p a r 方法为开发循环不变式提供了一种新的途径。当一个问题的递推关系得 到后，利用算法的前后置断言及得到的递推算法，对其中出现的各个变量的状态 加以分析，就可以较容易地得到算法的循环不变式，这克服了传统算法设计方法 无法提供算法程序的循环不变式的缺点，为程序的正确性证明及自动化生成提供 了理论支持。 p a r 方法是一种实用而高效的算法程序设计方法。但其只支持软件开发的算 法设计阶段。并不支持软件开发全过程。同时，对于开发过程中的子问题划分、 量词变换等工作需要人的参与，用户的个人素质决定了是否可以分划得到高效的 算法，有的问题当选择的分划策略不恰当时，甚至无法得到有效和解决方案【9 l 。 b 、z 和v d m 三者极为相似，都是基于模型的形式化规格说明方法。v d m 是b 、z 和v d m 中最早的一种语言，v d m 的数学符号建立在谓词逻辑和集合 论的基础上，在证明过程中还使用了三值逻辑( 真、假、未定义的) ，但v d m 没 能提供组装分解规格说明和精化的机制【2 】。b 不同于z 和v d m ，其提供了一个 重用库，还允许用户添加自己的重用库，以达到系统重用。同样，在d e s i g n w a r e 中，系统也提供了一个知识集，这个知识集按不同的类别提供精化规则支持用户 的求精过程。p a r 也提供了重用机制，不过其是实现级的重用，通过对数据类型 的抽象，使得用户可以重用这些预定义的抽象数据类型。 b 、z 和v d m 都是支持软件开发的全过程。而d e s i g n w a r e 和p a r 则更注重 于算法的形式化设计和开发，对于d e s i g n w a r e ，其设计者提供了其他两种方法 s p e c w a r e 和p l a n n w a r e 作为补充，以实现软件开发的全过程支持。 b 、d e s i g n w a r e 、v d m 、z 和p a r 都是通过描写出系统的规约，然后运用相 关的方法运用规约进行变换，以得到最终实现。在变换的过程中，v d m 和z 区 别对待数据和操作；而b 、d e s i g n w a r e 和p a r 则不是如此。在p a r 和d e s i g n w a r e 的算法设计过程中，都需要人的智力的支持。p a r 主要通过谓词变换来获得变化 1 0 r a d l - - ) a p l a 程序生成系统及其可靠性研究 关系，而d e s i g n w a r e 是只是通过范畴论来解释规约的变换，相比较而言，p a r 的演化过程更容易形式化且具有更高的可靠性和说服力。 2 4 形式化支撑工具简介 目前对于软件开发各个阶段的形式化开发方法，都有许多支撑工具可以选 择。本文专注于程序生成方面的研究，在此主要介绍几个程序生成领域的几个形 式化支撑工具。 1 慕尼黑大学e l b a u e r 教授主持的c i p 项目，该项目包含一个交互式程序 变换系统的研制，并保证转换过程的正确性，转换的实现只借助“保证正确性 的转换规则。但由于该系统要考虑通用性问题，需要支持一个适于描述各级程序 的广谱语言及庞大的编译系统，为了提高目标程序的效率，系统又必须提供大量 的用于各级程序之间的转换规则，所以变换系统仍然十分复杂，同时加上递归方 程表达问题的能力有限，c i p 系统仍未实现真正实用。 2 吉林大学主持的a t l a s 到c 的程序转换系统，该系统主要是运用传统的 程序编译技术对a t l a s 语言程序进行语法、语义等进行分析，并根据相应的转 换规则转换成c 语言程序。该系统在分析的过程中对a t l a s 进行了形式化的分 析，但是该系统并没有从低层的实现上来保证实现的正确性，同时因为该系统的 源语言和目标语言基本处于同一层次，即是一种横向变换，所以a t l a s 程序的 正确性与c 语言的正确性一样，难以说明。 3 江西师范大学由薛锦云教授主持的p a r 平台研究课题，p a r 平台目前主 要包含二部分，一部分为从抽象程序设计语言到高级语言的生成，主要包含： a p l a 专c + + ，a p l a - - j a v a ，a p l a - - ) c # ，a p l a - - v b n e t 等程序生成系统。该部分工 作实现了一种抽象的语言a p l a 自动生成到相应高级语言，a p l a 语言将常用数据 类型如树、图等预定义成语言中一种可扩展基本类型，在一定程序上保证了程序 的可靠性；同时a p l a 语言中独创的将数据库也定义为特定的数据类型，为数据 库定义及其操作的形式化、可靠性保证提供了一种有效的解决途径。另一部分为 算法设计语言到抽象程序设计语言的生成，即本研究项目将开展的工作。该系统 主要实现将一种较易进行正确性推导或证明的r a d l 程序到易于执行的a p l a 程序 的生成。 硕士学位论文 第3 章算法设计语言r a d i 3 1r a di 语言概述 r a d l 语言是为支持p a r 方法实现算法程序形式化和半自动开发而定义的一 种基于递推关系的算法设计语言( r e c u r r e n c eb a s e da l g o r i t h m