（计算机软件与理论专业论文）aplavbnet自动程序转换系统的设计与实现.pdf

摘要 p a r 方法是薛锦云教授在国家8 6 3 和多项国家自然科学基金的资助下， 根据多年从事算法程序设计理论研究的成果，创造性地提出的一种新的形式 化软件开发方法。该方法为有效克服“软件危机”起到了重要的作用。 自动程序转换系统是整个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 d p h i ，a p l a 一甜等。随着n l 强技术的提出，v b m 汀已 经成为了一种完全面向对象的语言，具有开发效率高，开发周期短等优点， 使得对软件的开发具有了更大的灵活性和实用性，深受广大开发人员的青睐。 因此，我们有必要设计开发一个a p l a 一n l t 自动程序转换系统。 围绕转换系统的设计与实现，本研究主要进行了以下工作： 】、对a p l a 语言和n e t 语言的文法进行比较，研究两种语言之间的 关系，并得出a d l a v b n l 玎的转换规则。 2 、实现简单数据类型和组合数据类型的转换，系统可以方便使用组合数 据类型，就如同使用简单数据类型一样，很好地实现了抽象数据类型的思想。 3 、对整个自定义可重用部件库进行了完善和补充，添加了t a b l e 类库， 使转换系统更好、更自然的支持对数据库的各种操作，同时也保持了对已实 现功能的支持，极大地提高了部件库的可重用性。 4 、设计并实现自动程序转换系统，基本实现了从a p l a 抽象程序到v b n e t 可执行程序的转换。 5 、用大量由p a r 方法推导得到的典型a d l a 程序对自动程序转换系统进 行了测试。 本研究的主要创新工作：a p l a 一。n l 玎自动程序转换系统的设计与实 现、对数据库中各种操作的支持、可重用部件库的实现等。 基于以上研究，我们设计并实现的a d l a v b n 1 玎自动程序转换系统能 提高软件开发的效率和软件的可靠性，有利于高可靠软件的开发，并且能从 根本上克服“软件危机”。 关键字：p a r 方法；a p l a ；自动程序转换；可重用部件库；v b h e t a b s t r a c t f a ri san e wf o n n a lm e m o do fs o f t w a r ed e v e l o p m e n t ，w h i c hw a sp r o p o s e d c r e a t i v e l yb yp m f c s s o rx u ej i n y u nu n d e rt h es u p p o r to f8 6 3h i t b c hp r o g r a m m e a n dn a t i o n a ln a t u r a ls c i e n c ef o u n d a t i o no fc h j n a 1 1 l i sa p p m a c hp l a y s a i l i m p o n a n tr o l ei no v e r c o m i n ge 伍c i e n t l ys o f | w a r ec r i s i s a u t o m a t i ci m n s f o 玎n a t i o ns y s t e mi sa ni m p 酣a n tc o m p o n e n to ft h e 眦 a p p r o a c h n ss i g n m c a n c el i e si n ：w i t ht h ea i do fl h ep a r m e t h o d ，t h en o n c r e a t i v e w o f ks e p a r a t e d 矗啪s o f 附a r ed c v c l o p m e n tp r o c e s sw i l lb ed c v e l o p e db yf b n l l a l m e t h o d s ，w h i c hf i l n h e r 掣e a t l yr e l i c v e st h ep r o 掣锄m e r s b u r d e na i l di m p m v e st h e d c v e l o p n l e n te f f i c i 饥c yo fa 1 9 0 r i t h i i l sp m 孕a m a tt h es 锄et i m ei ti l p r o v e st h e r e l i a b i l i t yo ft h ep r 0 黟a i r i a tp r e s e n t ，w eh a v ei m p l e m e n t e dm a i i yt r a s f o 加a t i o ns y s t e m s ，s u c ha sa p l a t oj a v a ，a p l at oc + 十，a p l at od e l p h i ，a p l at o 甜a s n e tt e c h n 0 1 0 9 ye m e r g j n 舀 n e th a sa l r e a d yb e c o m e a c o m p l e t e l yo b j e c t - o r i e n t e dl a i l g u a g e w i t h a d v a n t a g e so f h j 曲e f ! f i c i e n c ya n ds h o nd e v e l o p m e n tc y d e ，w h i c hm a k e ss o 脚a r c d e v e l o p m e n tm o r en e x i b l ea n dp r a c t i c a l ，s ov b n e t i sf a v o r c db ym o s t d e v e l o p e r s 1 e r e f o r ei t i sn e c e s s a r yf o ru st od e s i g na n di m p l e m e n ta p l at o v b n e ta u t o m a t i cp r o g r a mt r 踊s f o n n a t i o ns y s t e m 7 n l ep r i m a f yw o f k sw eh a v ed o n ei nt h i sp a p e ra r el i s t e da sf b n o w s ： 1c 0 玎l p a 咖gt h es y n t a xd i s t i n c t i 彻b e 柳e e na p l a 卸dv b n e t ，如d i i l go u t t h er c l a t i o n s h i pb e t w e e nt w oo ft h e m ，i no f d e rt oo b t a i nt h et r a n s f o 咖a t i n gn 1 1 ei n t h es y s t e m 2l i n p l e m e n t i n gt r a 船f o f m a t i o n s 劬ma p l a sa b s t r a c td a t at ”e st ov b n e t s r e u s a b l ec o m p o n e n t sl i b r 哪 3e x t e d i gt h ee x i s t i n gs e l f - d e f i n e dr e u s a b l ec o m p o n e n t sl i b r a r yw i t h o p e r a t i o n so nd a t a b 弱e 4d c v e l o p j n gt h ea p l at 0v b n e ta u t op m g 舢t f a n s f o 加a t i o ns y s t e m - 5d e r i v i n gal a r g en u m b e ro fa p l ap r o 伊a m sb yi a r ，t h e nu s i n gt h e mt ot c s t t h et r a n s f 咖a t i o ns y s t e m 1 l lt h ed e v e l o p m e n to ft h es y s t e m ，s o m ei n n o v a t i o n sh a v eb e e nm a d ea s f o l l o w s ： d e s i g n a n d i m p l e m e n t a t i o n o f a p l a t ov b n e ta u t o p m g r a m t f a n s f 咖a t j o ns y s t e m ，s u p p o r tf o rt h eo p e r a t i o n so nd a t a b a s e ，i m p i e m e m a t i o no f 川- r e u s a b l ec o m p o n e n t sl i b r a r ) ra n ds oo n b a s e do nt h ea b o v es t u d i e s ，t h ea p l at ov b n e ta u t o m a t i cp r o g r a m t r a n s f o 瑚a t j o ns y s t e mh a sb e e nd e s i g n e da n di m p k m e n t e dt oi m p m v ee f f i c i e n c y a n dr e l i a b i l i t yo ft h cs o f t w a r e ，t h a ti sc o n d u c i v et ot h ed e v e i o p m e n to fh i g i l r e l i a b i l i t ys o f t w a r e ，a n df i l n d a m e t a l l yo v e r 0 0 m et h es o f t w a r ec r i s i s p k c y w o r d s ：p f 犍m e t h o d ； a p l a ； a u t o m a t i cp r o 芦a mt r a n s f o 珊a t i o n ；r e u s a b l e c o m p o n e n t sl i b f a r y ；v b n e t 1 v a p l a v b n e t 自动程序转换系统的设计与实现 研究背景 引言 长期制约软件应用及发展的瓶颈是软件开发效率低，以及软件的正确性 和可靠性得不到保证。这种现象常被称为“软件危机”。为了解决这一问题， 先后出现了z ，v d m ，c l p ，r 出s e ，b 等形式化方法，但这些方法普遍都存 在实用性差，难以推广应用等缺陷。 软件开发中存在的主要问题就在于：软件开发的自动化程度低，成本太 高。图灵奖获得者j 锄e sg r a y 认为自动化程序设计( a m t o m a t i cp r o g m m m i n g ， a p ) 是提高软件可靠性和生产效率的根本途径，但进展很缓慢。 薛锦云教授在国家8 6 3 和多项国家自然科学基金的资助下，根据多年从 事算法程序设计理论研究的成果，提出了种简单实用的设计和证明算法的 形式化方法一p a r 。这种方法结合形式化方法和非形式化方法，正确区分开 发过程中的创造性劳动和非创造性劳动。在该方法的指导下，定义了r a d l ( r e c u r r e n c c - b a s e d g o r i t l l i i l d e s i 印l a n g l l a g c ) 抽象算法设计语言来描述算法 规约和抽象算法，定义了a p l a ( a b s t r a c tp r o 擘a m m i gl a i l g u a g e ) 语言来描述 抽象程序。 a d l a 语言充分体现了数据抽象和过程抽象的思想，并且含有明显的语法 机制支持泛型程序设计、预定义泛型虹) t 类型和用户自定义泛型灿) t 类型。 这使得a p l a 语言能描述别的高级语言很难描述的问题，用a p l a 语言能编写出 比其他高级语言更简练、更清晰的算法程序，也使得a p l a 程序的正确性验证 更容易，程序的可靠性更能得到保障。但是，a 口l a 语言是一种抽象程序设计 语言，不能直接编译运行得到结果，如果单独做编译器对我们目前来说难度 较大，并且所处的地理环境以及人员条件不满足，力量不够，经济也不允许。 此外，根据p a r 方法，我们发现由递推关系到循环不变式，及由算法到程序 的丌发，属非创造性劳动，完全可以用完全形式化方法机械地变换得到。所 以，可以将非创造性劳动通过构造一个自动转换工具由计算机机械完成。这 个工具就是自动程序转换系统，将由a p l a 语言编写的抽象程序转换成一个高 级语言的可执行程序，这样就可以通过调用已有编译器编译得到运行结果。 自动程序转换系统的意义在于根据p a r 方法，将软件开发过程中分离出 来的非创造性劳动，用形式化方法进行开发，进而借助计算机机械地实现， 大大减轻了程序员的负担，提高了算法程序的开发效率，同时也提高了程序 a p l a v b n e t 自动程序转换系统的设计与实现 的可靠性。 研究现状 基于p a r 方法对算法程序进行设计和证明不仅保证了所得到的算法程序 的正确性，而且极大地提高了算法程序的开发效率。如果将其应用到实际的 软件开发中去，软件的可靠性就可以得到保证。 目前，p a r 方法开发平台提供了一系列的转换工具，如：r a d l a p l a ， a p l a c + + ，a p l a d e l p h i ，a p l a j a v a ，a p l a c # 等，这些工具支持软件开发 的不同过程。 随着n e t 技术的提出，n e t 也已经成为了一种完全面向对象的语 言，具有支持继承、派生、重载等一切面向对象的特性，是s u a ls t u d i o n e t 开发平台中的核心语言之一。它和过去的编程模式有了很大的区别，具有开 发效率高，开发周期短等优点，使得对软件的开发具有了更大的灵活性和实 用性，深受广大丌发人员的青睐。因此，我们有必要设计开发a p l a v b n l 玎 自动程序转换系统，该系统支持a p l a 程序到v b n e t 程序的自动转换和转换 后的直接运行，其内容来源于对以下课题的研究： 1 、国家自然科学基金课题：实用软件形式化方法及其开发工具研究 2 、国家自然科学基金课题：基于p a r 方法的算法设计形式化和自动化 研究 本文的主要工作与组织 1 本文的主要工作 本文是以p a r 方法、n e t 程序设计理论和关系数据库理论为基础，设计 并实现a p l a v b n e t 自动程序转换系统。 本研究主要进行了以下工作： 1 、对a p l a 语言和n e t 语言的文法进行比较，研究两种语言之间的 关系，并得出a p l a 一n e t 的转换规则。 2 、实现简单数据类型和组合数据类型的转换，系统可以方便使用组合数 据类型，就如同使用简单数据类型一样，很好地实现了抽象数掘类型的思想。 3 、对整个自定义可重用部件库进行了完善和补充，添加了t a b l e 类库， 使转换系统更好、更自然的支持对数据库的各种操作，同时也保持了对已实 现功能的支持，极大地提高了部件库的可重用性。 a p l a v b n e t 自动程序转换系统的设计与实现 4 、设计并实现自动程序转换系统，基本实现了从a p l a 抽象程序到v b n e t 可执行程序的转换。 5 、用大量由p a r 方法推导得到的典型a p l a 程序对自动程序转换系统进 行了测试。 本研究主要具有以下创新工作： 1 、设计并实现a p l a v b n e t 自动程序转换系统。 目前，在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 ，a p l a 一甜等。但是随着n e t 技术的提出，i t 语言越来越受程序员的喜爱，为此，我们创新性的设计并实现a p l a 一n e t 自动程序转换系统。通过对两种语言的文法进行比较，得出一系列转换规则。 2 、设计实现部件库，极大地提高了代码的可重用性。 我们设计实现的可重用部件库由p a r 方法推导得出，在充分保证了它的 正确性和可靠性的基础上，可将其用于n e t 平台的所有语言中，极大地提高 了部件库的可重用性。 3 、支持对数据库的各种操作。 随着计算机的广泛应用，我们对于海量数据的查找、更新、修改等操作 也越来越频繁，与数据库进行连接的频率也越来越高。在部件库的设计过程 中，我们添加了r i a b l e 类库，使转换系统支持对数据库的各种操作。1 a b l e 类 库是建立在严格的关系数据库理论的基础上，其正确性和可靠性是有理论支 持和验证的。 2 本文的组织 本论文的组织如下： 第一章形式化开发方法研究，介绍形式化方法分类及其优点，了解国内 外相关方法的研究现状和存在的问题，重点介绍一种新型软件开发方法p a r 及其支撑平台。 第二章介绍n e t 框架，n e t 框架是一个全新的跨语言软件开发平台，对 于它的体系结构和优点进行了主要介绍。 第三章重点介绍了自动程序转换系统的设计与实现，这也是本文的核心 部分。 第四章通过各种转换实例测试该自动程序转换系统的实际运行效果。 第五章结束语，对整个工作做了总结，给出了进一步的工作，并对本研 究的前景作了展望。 a p l a v b n e t 自动程序转换系统的设计与实现 1 1 形式化方法 第一章形式化开发方法研究 随着软件的广泛应用，特别是软件在尖端领域的应用，软件可靠性已经 成为一个非常重要的问题。软件的可靠性主要取决于两个方面：一个是软件 产品的测试与验证：另一个是软件开发的方法与过程。 用形式化方法开发软件，被当今计算机界誉为克服“软件危机”，提高软 件可靠性和生产效率的革命性途径。形式化方法的意义在于它能帮助发现其 它方法不容易发现的系统描述的不一致，不明确或不完整，有助于增加软件 开发人员对系统的理解，因此形式化方法是提高软件系统，特别是 s a f c t y c r i t i c a l 系统的安全性与可靠性的重要手段。尽管已经提出了各种各样的 软件形式化开发方法和开发技术，如程序计算、程序变换以及以此为基础产 生的z ，v d m ，r a i s e ，c i p 和b 方法等。但是目前这些技术还没有被软件 产业界广泛接受f 增j ，原因在于许多方法的倡导者并没有真正研究软件开发者 所面临的实际问题，算法和程序研究相脱节，缺乏系统的算法程序设计和证 明方法。事实上有些方法以及以这些方法为基础而建立的软件开发工具和自 动生成系统只能处理和生成一些玩具式程序( t o y s t y l ep r o g r a m ) 【3 】o 尚没有 一种面向实际问题、简单可行、便于广大软件开发者接受的形式化方法及与 该方法相配套的一系列辅助开发工具来切实地解决这些问题。 1 1 1 形式化方法的分类 在算法程序开发中，常用的形式化方法主要有以下两种【枷】： 一种是对于一个给定的算法程序设计问题，先用符号化的规范描述语言， 写出这个问题的形式化规范，然后采用变换方法，将问题的形式化规范变换 成可执行的程序。变换的开始、中间到结束，产物是一符号串，我们常称这 种形式化方法为完全形式化方法，使用完全形式化方法产生程序的过程可以 用计算机机械地产生。但目前用这种方法只能产生没有创造性劳动的简单程 序。 另一种形式化方法是对于给定算法程序设计问题，先写出该问题的形式 化规范，然后使用形式化和非形式化相结合的方法，开发或证明算法程序正 确，这种方法常被称为部分形式化方法，或被称为数学家的形式化方法，使 用这种类型的形式化方法常常可以设计和证明一类相当复杂的算法程序和软 件。 a p l a v bn e t 自动程序转换系统的设计与实现 使用形式化方法开发软件可以提高软件的可读性、可靠性和可维护性， 并为实现软件开发的自动化奠定基础。 1 1 2 形式化软件开发方法的优点 ( 1 ) 形式化的规范可以准确而无二义性地阐述一个问题。 ( 2 ) 形式化方法要求完整性和一致性，这样可以减少出错的机会。 ( 3 ) 形式化方法是基于数学理论的，可以使用一些定义好的规则将抽象 的规范转化成为具体的程序，通过这种方式可以实现软件开发的自动化。 ( 4 ) 形式化方法可以以一种抽象的形式定义系统，可以让一般的程序员 了解系统所做的工作。 ( 5 ) 形式化语言有利于国际之间的交流。 1 2 典型的形式化开发方法及其支持工具 目前，典型的形式化方法及其工具主要有以下几种： 一、z 方法 z 方法m 0 1 是软件工程中一种常用的规范描述语言。它是以程序公理语义 为基础的形式化开发方法，它的规范说明语言基于模式演算，提供了丰富的 操作运算，但不可执行。z 语言有模式匹配的符号，使用了具有强大功能的操 作符，还使用了一些非形式化的英语解释，给出的规范说明比较短，易于阅 读和理解。 z 语言已经成为世界最流行的形式化规约语言。现有大量的工具支持，它 们主要集中于规约的编辑和显示以及语法和类型检查方面，也有些工具支持 规约的推理和精化。比较有影响的工具有：f o 瑚a l i s e r 、p r 0 0 f p o w e r 、z o l a 、 c a d i z 、f o r m o o z 、z ，7 e v e s 等。 z 语言存在以下一些缺陷| 1 0 1 ： ( 1 ) z 语言难以用计算机直接处理。 ( 2 ) 难以识别影响某一状态模式的所有操作模式。 ( 3 ) 不能支持规格说明的重用。z 语言中没有提供重用机制。 ( 4 ) z 语言对大型系统的模块化能力不足。 为了克服z 语言这些缺陷，8 0 年代未到9 0 年代初相继提出了一些z 语 言的扩展方案，也进行了一些标准化工作，国际上在9 0 年代初提出形式化方 法和面向对象方法相结合的思想，虽然有所发展，但因缺少商品化的工具支 持等诸多原因，而不能进行大量的实际应用，因而还需要进一步完善。 二、v d m 方法 a p l a v b n e t 自动程序转换系统的设计与实现 v d m ( t h ev j e n n ad c v e l o p m e n tm e t h o d ) 方法是在1 9 6 9 年由i b m 公司维 也纳实验室研究小组提出的一种功能构造性规格说明技术。它是一种使用较 早、应用较广的基于模型的形式化方法，也是当前较为成熟的形式化开发方 法之一。v d m 是一种基于指称语义的方法，它基于离散数学的理论，包括集 合论和关系论。它具有从原始规约的高级抽象数据类型变换到目标程序设计 语言的数学类型的能力。也体现了操作分解的原则，它使指定的函数和操作 分解为更易于用目标语言来实现的形式。 v d m 包含一个称为“v d m s l ”【1 1 i ( v d ms p e c i f ：i c a t i o nl a i l g l l a g c ) 的规 约语言：一组用于在抽象的需求规约和代码级的详细设计规约间建立链接的 数据求精和操作求精规则；一套证明理论，其中可用严格的参数来操作指定 系统的属性和保证设计决策的正确性。 v d m 方法具有以下三个明显的优点【1 2 】： ( 1 ) 只告诉计算机“做什么”。 ( 2 ) 提供了程序正确性证明的依据。 ( 3 ) 规格说明的描述简练、精确。 除了这三个明显的优点外，使用m 还可以培训程序设计者牢固树立先 抽象，后具体的不断证明其正确性的逐步分解的自顶向下的开发思想，从而 在整个程序开发的全过程中用系统而严密的方法保证所开发的程序的正确 性。 但v d m 也存在不足之处：v d m 的每一步求精都是在上一求精步骤的进 一步具体化，由于各个求精步骤之间并不存在着严格的推导关系，因此整个 算法推导过程不够严谨，其正确性是在算法推导完成后再回头验证其每一求 精步骤来保证其正确性，若有错误又得重新推导算法，然后再对推导过程进 行重新验证，同时v d m 的每一求精步骤都包含“数据精化”和“操作分解” 两个不同的过程，将数据结构和算法分离，这些都导致使用v d m 来开发算法 的效率不够高。此外，尽管v d m 的规约语言已由i s o 标准化并得到很多成熟 工具的支持，但目前仍没有一个满意的工具来支持验证。 三、r 越s e 方法 r a i s e 方法( 砌g o r o u sa p p m a c ht oi n d u s t r i a ls o f t w a r ce n 舀n e e f i n g ) 是欧 洲e s p r i t 项目研发的一种适用于工业界的形式化方法。它为工业界应用形式 化方法开发软件系统，提供了有力的工具和途径。r a i s e 方法覆盖了软件丌 发的关键阶段，如需求分析和项目管理。它的目标是使建立的软件系统更加 可靠、错误更少、文档化更好、更易维护。 针对v d m 存在的两个明显的不足之处：缺乏模块性和不能处理并发的情 a p l a v bn e t 自动程序转换系统的设计与实现 况。r a i s e 使用了一种完全不同的方法：代数法。它的规范描述语言r s l 综 合了其它多种形式化方法描述应用的特点，是一种广谱的描述语言。它既能 描述高层抽象，也能够刻划底层设计。r a l s e 方法提供整套支持工具，支 持编辑和管理开发过程中涉及的多种实体，而且这些工具提供的环境可以方 便地跟踪文档化软件系统开发的全过程，支持软件系统生命周期内的维护和 改进。 但是，r a i s e 方法只是提供了开发的框架和指导方针，它不支持软件开 发的全过程。 四、b 方法 b 方法【1 3 】是一种应用范围较广且较成熟的形式化方法之一，它是在v d m 和z 的基础上发展而来的，和z 尤其相似。b 方法也是基于模型的形式化开 发方法，并且具有很高的数学抽象程度，它于8 0 年代初产生于法国，9 0 年代 中期发展成熟。 b 方法提供了一种统一的支持软件开发全过程的标示语言( 描述规范、设 计、编码及正确性证明、测试) 。这种开发方法通过一系列的数学表示( 逻辑 理论、集合理论：关系、集合、函数) ，利用谓词转换对模型进行逐步的精化， 把原始规约的高级抽象数据类型逐步交换到可执行的目标程序设计语言。 b 方法的重要组成部分是抽象机( a b s t r a c tm a c h i n e ) ，抽象机用a b s t r a c t m a c h i n en o t a t i o n ( a m n ) 语言来描述。用b 方法开发的软件系统通常由一系列 的抽象机构成。每个抽象机包括数据和操作，它实际上就是一种封装机制。 在抽象机的具体实现中，数据仍用集合理论模型来实现，操作却是用a m n 的 子集伪程序表示。 b 方法的特点【1 2 】：简单熟悉的符号表示法；模块化构造；大量实用的工 具支持，b 方法有一个b 方法工具包( b t 0 0 l k i t ) ，支持用户编写、验证和维 护软件；它还提供了一个大的数学规则库。利用这些工具，可以自动执行程 序正确性的形式化证明。但使用b 方法书写需求规范比较复杂【1 1 】。 五、c 口系统 c i p ( 计算机辅助的直观制导的程序设计) 系统1 1 4 】是德国慕尼黑大学 f r i e d r i c hl u d w i 叠b a u e r 教授主持的，在8 0 年代的时候达到顶点。c i p 是开发 可形式保证程序正确性的程序开发系统，其目标有三个：第一，设计并定义 一种广谱语言c i p l ( 计算机辅助的直观制导程序设计语言) ；第二，开发一 个交互系统；第三，建立一套完整的能指导程序开发中形式推理过程的方法 学。 c i p 的特点： a p l a v b n e t 自动程序转换系统的设计与实现 ( 1 ) 各步之间转换的实现只借助能“保证正确性”的转换规则。 ( 2 ) 开发过程完全由程序人员指导，即由程序人员选定转换规则。 目前c i p 无后续研究的原因是c i p 采取自顶向下逐步求精的开发思想， 对于大部分巧妙的算法是推导不出来的，只能实现一些简单的算法，因此仅 适用于部分领域。 1 3 新型软件开发方法p a r 及其支撑平台 1 3 1p a r 方法及p r 平台简介”即 p a r 方法是一种统一的算法程序设计和证明方法。该方法基于分划、递 推、扩充的量词变换规则、循环不变式的新技术和软件转换工具，充分利用 数据抽象、功能抽象、软件重用、多态、类属、重载、泛型等成熟的程序设 计技术，实现了复杂算法问题的形式化开发，它是一种实用的形式化方法， 并支持算法程序开发的全过程，是算法程序设计和证明方法研究方面的重要 突破。p a r 方法统一了目前普遍使用的动态规划法、贪心法、分治法等算法 设计方法，把这些只能用于特殊领域的方法实现了更广泛的应用。大量实践 证明，p a r 方法不仅开发小程序切实可行，而且开发复杂算法也十分有效。 其基本指导思想是：分离软件开发过程中的创造性劳动和非创造性劳动，通 过不断地提出新的理论、方法，尽可能多的把创造性劳动转化为非创造性劳 动，对创造性劳动采用部分形式化理论进行描述、推导、演算，对非创造性 劳动用相关工具进行机械转换。 p ：a r 方法i “】与国际上其它方法的主要区别在于：其它方法主要根据自顶 向下，逐步求精的开发思想，因此只能处理逻辑结构相对简单的问题，而对 于一些算法问题却解决不了，而p a r 方法可以解决从做什么到怎么做的问题。 p a r 方法及其支撑平台由自定义泛型算法程序设计语言r a d l 及相关规约 转换规则库；泛型抽象程序设计语言a p l a ；系列r a d l 到a p l a ，a p l a 到j a v a ， c + + ，c # ，d e l p h i ，n e t 等可执行语言程序自动转换系统和系统的算法 和程序设计方法学组成。 下面就其组成部分一一给以介绍。 一、算法程序设计语占r a d l r a d l l l 7 】( r e c u c n c e b a s e d 舢g o r i t h md e s i 印l a n g u a g e ) 的主要功能是描 述算法规约，规约变换规则和描述算法。r a d l 由算法规约语言( 舢f i t h m s p e c i f i c a t i o nl a n g i l a g c ) 和算法描述语言( a l g o r i t h md e s c r i p t j o n 山g u a g e ) 两 部分组成，用作a p l a 的前端语言，主要面向用户，适应传统的数学习惯，且 a p l a v bn e t 自动程序转换系统的设计与实现 具有引用透明性，便于算法的形式推导。r a d l 的一个重要特色是它的数据类 型系统。它提供了标准数据类型，自定义简单类型，预定义声州，自定义a d t 和泛型a d t 机制。用户可以像使用标准数据类型一样使用预定义的常见组合 数据结构的a d t 。 二、抽象程序设计语言a d l a a p l a l l 8 l ( a b s t r a c tp i o 孕a m m i n gb n g i l a g e ) 是r a d l 算法一程序转换器的目 标语言，又是a p l a 到其它可执行语言程序转换器的源语言。设计a p l a 的主要 宗旨是充分体现数据抽象、功能抽象、重载、泛型等现代程序设计思想，使 之简单实用，便于程序开发，易于转换成各种可执行程序设计语言程序。用 a p l a 语言描述的程序十分简短。 三、系列r a m 和a p l a 程序自动转换系统 p a r 方法推导出来的算法程序是抽象程序设计语言a p l a 描述的，不能直 接编译运行得到相应的结果，若为算法语言单独编写一个编译器的话，不仅 难度较大，而且难以在不同的机器间移植，编译器的正确性也很难得到保证。 因此，需要开发自动转换系统，如系列r a d l 转换器【1 9 】，将r a d l 语言描述的算 法自动转换成a p l a 语言描述的抽象程序；系列a p l a 转换器【扯2 4 1 ，用a p l a 语 言描述的抽象程序自动转换成可执行的程序( 如j a v a 、c 带、c + + 、v b n e t 等) 。 这些工具具有人性化的界面和操作方式，提供目标程序的直接执行功能，操 作者使用起来非常地方便。 1 3 2p a r 方法提出并解决的关键技术 1 、循环不变式 2 5 ，2 6 l 的新定义和新的开发策略。 2 、提出了一种统一的算法设计方法。 第1 步：尽可能形式化的构造一个问题的规范，也就是精确地描述算法 要完成的工作。形式化规范强迫算法设计者仔细精确地考虑问题，并使推导 和证明递推关系成为可能。 第2 步：把问题分解成一定数目的子问题，每一个子问题和原问题结构 相同但规模较小，再按同样的方式把子问题分划成更小的子问题，直到每一 个子问题都能直接求解。能直接求解的子问题称为最小子问题。 第3 步：构造问题求解序列的递推关系s 产f ( s 。) 并给出在递推关系中出现 的函数和变量的初始条件，再把初始条件和所有的递推关系合并成一个算法。 3 、提出一种新的算法表示法。 现有的三种算法表示法均不便于算法的形式化推导和证明。为此提出的 新的表示法是基于问题求解序列的递推关系。 4 、提出算法设计语言r a d l 及其规约变换规则。 a p l a v b n e t 自动程序转换系统的设计与实现 使用r a d l 提供的规约变换规则可以推导出快速，高效的算法。 5 、提出抽象程序设计语言a p l a 。 将传统的数学符号和数学表达式引入程序设计语言中，使得构成的程序 易于阅读理解和进行形式化验证。 6 、灵活，方便，完整的泛型程序设计机制。 7 、实用的软件形式化方法。 用p a r 方法开发算法程序的6 步骤【2 7 ，冽： 第1 步：用r a d l 语言精确地描述求解问题的功能规约。根据不同的需要， 这种描述可以是形式化的，也可以是非形式化的。 第2 步：把需求解的问题分划成若干和原问题结构相同但规模更小的子 问题，分解可一直进行下去直至每个子问题可直接求解。可直接求解的子问 题称为最小子问题。 第3 步：构造问题求解序列的递推关系s i - f ( s 。) ，并给出在递推关系中出 现的函数和变量的初始化条件，再把初始化条件和所有递推关系合并成一个 算法。 第4 步：基于循环不变式开发的新策略，开发循环不变式。 第5 步：基于所得的算法和循环不变式开发a p l a 算法程序。大多数程序 可以通过对算法进行同等变换直接得到，这种变换可以是手工的，也可以是 自动的；有些程序( 循环不变式使用了递归定义技术) 则需要通过归纳推理 获得非递归程序，然后证明程序的正确性，这项工作目前只能手工完成。 第6 步：将a p l a 算法程序转换成等价的某一可执行语言程序。 由p a r 方法的理论及上述对算法的推导，我们可以看出，眦【方法在克 服“软件危机”方面将大有作为。甜r 方法是一种能够设计快速算法的算法 程序设计方法，通过递推关系，推导出来的算法总是使后一步的结果建立在 前一步结果的基础上，避免了许多重复性的工作和计算；p a r 不仅可以用来 解决一些传统算法设计方法可以解决的问题，也可以解决用传统设计方法不 能解决的问题；循环不变式是理解和开发算法程序的关键，但产生循环不变 式的过程仍然需要创造性劳动的参与，即匮方法在此过程中起到了关键性的 指导作用。当一个问题的递推关系得到后，利用一些变量来记录递推关系中 出现的函数值，并约束变量的变化范围即成为循环不变式，这克服了传统算 法设计方法无法提供循环不变式的缺点。 1 3 3 应用前景 p a r 方法为高可靠软件的研发提供了方法学和工具方面的支持。特别适 用于急需高可靠软件的航空航天，工业过程控制和医疗机械等安全性至关重 a p l a v b n e t 自动程序转换系统的设计与实现 要领域的软件开发。此外，p a r 方法也适用于一般软件丌发。 系列算法程序自动转换工具可以替代软件企业蓝领和部分白领的工作， 减轻程序设计者的劳动。 a p l a v b n e t 自动程序转换系统的设计与实现 第二章n e t 框架简介 n e t 框架是微软n e t 平台中最关键的部分。它是在i n t e m e t 已经逐步成 为编程领域的中心时应运而生的。n e t 框架是一个全新的跨语言软件开发平 台，顺应了当今软件工业分布式计算、面向组件、企业级应用、软件服务化、 以w 曲为中心等大趋势。然而，它不仅仅是为了h l t e m e t 编程，而且还包含了 几乎所有的w i n d o w s 编程。m 玎框架为开发人员提供的技术比以前的任何微 软开发平台提供的技术都要多，比如代码重用、代码专业化、资源管理、多 语言开发、安全、部署、管理等。m i c m s 咄对n e t 的最终目标是：创造一个 全球化的分布式系统，包括个人计算机、个人数字助理、蜂窝电话以及任何 和它远程连接的设备。n e t 最终将可用于所有这些平台，并允许它们进行无 缝交互1 2 9 1 。 2 1 n e t 框架的体系结构 n e t 框架的体系结构如图2 1 所示： 图2 1 n e l 框架的体系结构 从上图中可以看出，n e t 框架是建立在w i n d o w s 操作系统之上的，它由 两部分组成：公共语言运行库( c o m m o n g u a g er u n t i m e ，c l r ) 和n l 玎 框架类库( f r a i l l e w o f kc l a s s “b r a r v ，f c l ) 。其中c l r 是n e t 框架的核心， 它为开发人员提供了一个跨语言的统一的编程环境。f c l 则提供了一个统一 的、面向对象的、可扩展的类库集( a p i ) 。通过创建一个公共的跨编程语言的 a p i 集，n l 玎框架可实现跨语言继承性。这样，开发人员可以自由选择理想 a p l a v bn e t 自动程序转换系统的设计与实现 的编程语言。 c l r 和f c l 提供的一部分服务如下i 】： 一致的编程模型 对于当前的w i n d o w s 操作系统而言，某些功能需要通过动态链接库( d l l ) 来访问，而某些功能则需要通过c 0 m 对象来访问。然而，在n 】玎框架下， 所有的应用程序服务都将以一种一致的、面向对象的编程模型提供给开发人 员。 简化的编程方式 c i 且的一个目的就是简化w i n 3 2 和c o m 环境下所需要的各种繁杂基础 构造。在c l r 下，完全抛弃了如：注册表、全局唯一标识符( g u i d ) 、i u n k n o w n 、 a d d r e 凡r e l e a s e 、h i t e s u i t 等概念。 广泛的平台支持 当编译器编译面向n e t 框架的源代码时，它实际上产生的是通用中间语 言( c c 嘲m o ni n t e r i n e d i a t cl 加g l l a g c ，简称c i l ) 。只有在运行的时候，c l r 才 会将这些c i l 翻译为c p u 指令。由于这个过程发生在运行时，所以它是面向 特定的宿主c p u 的。 无缝的语言集成 c o m 允许不同的语言之问进行互操作。而n e t 框架允许不同的语言之 间进行无缝集成。当使用一个类型时，不管它是用何种语言开发的，我们都 可以像使用自己语言开发的类型一样来使用它。例如，在v i s u a lb a s i c 中创建 一个类，然后在c # 中继承它。c u t 允许这样做是因为c l r 要求所有面向它 的语言都要遵循一种称作通用类型系统( c o m m o n1 y p es y s t e m ，简称c t s ) 的规范。而通用语言规范( c o m m o nl a n g l l a g es p e c 试c a t i o ，简称c l s ) 则描 述了一种语言与其他语言很好地集成在一起所必须遵循的规范。 简便的代码重用 使用上面所述的机制，我们可以很容易地创建一些类型来为第三方应用 程序提供服务。n e t 框架使得代码的重用变得非常简单。 强大的互操作能力 许多玎发人员有着无数现存的代码和组件，要重写所有这些代码来利 用n e t 框架平台无疑是一项艰巨的工作，其结果往往会延缓开发人员对n e t 框架平台的接受速度。因此，n e t 框架从开始就对访问现有c o m 组件， 以及调用传统d l l 中的w i n 3 2 函数提供了完全的支持。 全新的安全策略 传统操作系统的安全机制都是基于用户帐号柬提供隔离和访问控制的。 a p l a v b n e t 自