课题综述
二十世纪最后二十年计算机硬件技术取得巨大进步。相形之下软件技术的发展比较缓慢，软件开发方法落后是造成这一现象的主要原因。软件自动生成和软件形式化开发技术虽然一直受到学术界和工业界的高度重视，但是由于软件本身的复杂性使得研究的难度较大，进展比较缓慢。
80 年代英国牛津大学开发的Z方法和IBM公司提出的VDM方法都是形式方法方面杰出的成果。这些方法以指称语义为基础，设计了对应的规范描述语言，用以描述软件的抽象模型。这种描述经过一系列模型的精化和验证，得到一个比较具体的软件规范，进而用于指导软件的具体实现，或者经过自动转换直接生成目标程序。
德国慕尼黑技术大学提出的CIP计划和美国康乃尔大学的POLYA语言的研究都采用程序变换系统的方式。他们以操作语义作基础，实现广谱语言的内部源到源变换。
北京大学"软件方法学"研究组从1983年起承担了"国家六五攻关"项目"软件理论"课题，在吴允曾教授的带领下率先在国内开展"形式化方法"的研究，对VDM，Z和CIP的程序变换系统进行了深入分析研究。市科委曾多次拨款，资助吴允曾教授出访西欧和北美，与国际有关科研单位（包括上述学校和厂商）建立了良好的合作关系。1998年张乃孝教授应邀赴康乃尔大学，作为客座副教授在著名计算机教授David Gries教授领导的课题组中工作，参加了美国国家自然科学基金项目，成为"POLYA"语言的设计者之一。
在跟踪国际先进水平和自己开展有关研究的过程中，本课题组也发现了上述研究中存在的一些固有缺陷。例如：借助形式系统的证明不仅非常烦琐、难以阅读，而且存在一定局限性和"陷阱"，使得正确的东西不一定都能得到证明。此外，国外工作者提出的变换系统不仅由于非常复杂，由此变换的效率低下和变换目标程序的运行缓慢，而且在变换过程的控制中还隐藏着"旋涡"，可能陷入某种循环变换而不能自拔。
基于上述背景和本课题组对问题的认识，本课题组从1990年开始了新软件方法学的研究工作。十年来本课题组围绕这一方向开展了比较深入的研究，大体上可以分为三个阶段：
第一阶段（1990-1992），方法学的提出。这期间承担了一个基金项目和一个863项目。明确提出一种的软件开发方法--"面向模型的变换型软件开发方法"（Model-Oriented Specification And Transformation）；开发了一个"程序变换实验系统"；并用所提出的方法成功地模拟了一些变换的实例。
第二个阶段（1993-1995），为理论研究阶段。主要完成了一个基金项目。对"面向模型的变换型软件开发方法"的理论基础进行了比较全面的研究，提出了支持该方法学的"语言的抽象封装机制--GARMENT"。
第三阶段（1996-1999），环境原型的开发和应用研究。承担了一个基金项目和一个国防科技预研项目。根据面向模型的变换型软件开发方法和GARMENT理论的研究成果，设计并实现一个软件开发环境的原形（称为GARADA95）。并且在这个环境中成功的开发了三个小型软件。与此同时还取得了一些理论成果。
这项研究在以下几方面取得创造性进展：
- 吸取了VDM、Z、CIP和POLYA有关工作中的精华，汇入"部分实现"和"面向对象"的思想，提出了一种"面向模型的变换型软件开发方法"，把一类软件的开发抽象成为从软件的规范说明出发，经过一系列保持正确性的变换，最终得到一个正确有效的软件的过程。这个过程可以简单地用公式表示为：
Specification + Transformation = Software
- 提出了"变换型语言族"的概念。把软件的规范抽象成软件界面语言的规范，把软件开发环境的研究从程序开发环境的研究中分离出来，为"面向模型的变换型软件开发方法"建立了一种统一的分层开发模型。
- 设计了一种语言的抽象与封装机制--"GARMENT"。一个GARMENT封装了一个语言的完整定义（包括语法和语义信息）。GARMENT的提出把数据抽象的层次从"类型"提高到"语言"，从而使语言成为软件理论研究和软件开发过程中处理的高级对象。
- 为"面向模型的变换型软件开发环境"设计了三种新的可重用部件，为建立大型语言知识库提供了灵活的手段：
- 语言的完整定义（即一个GARMENT）作为最高层的可重用部件；
- 语言的一类成分（例如语言中所有控制语句）的定义作为中层的可重用部件；
- 语言的具体成分（例如一个数据类型）的定义做成一个"变换模块"，为最低层的可重用部件。
- 探讨了"变换型语言族"和"GARMENT"的理论模型，取得以下成果：
- 为语言族中的语言建立了一个代数模型，给出了语言的继承、屏蔽和扩充的语义。此代数模型是抽象数据类型代数模型的升华。
- 通过研究Garment中的归约语义，提出了语言可归约的充分条件。
- 研究了Garment中的约束多态类型，给出了类型检查算法，证明了此算法中约束的可满足性是可判定的。
- 提出了Garment中参数化多态类型和约束多态类型的Ideal语义，并以此证明了Garment中的类型规则的语义可靠性。
- 提出循环不变式的"状态迁移理论"，并将其成功地用于不变式的开发，使得不变式的推导更加自然有效。
- 根据Garment理论设计并实现了一个以ADA95程序开发为目标的软件开发环境，称为GARADA95。用户可以使用这个环境定义具体领域的用户语言，系统能自动完成用户语言程序到ADA95语言程序的转换。
- 使用GARADA95成功的开发了三个典型的小型软件：
- 本项研究综合应用当前计算机科学的许多重要成果，并力争有所创新。主要涉及软件开发的形式方法，形式语义学，编译理论，类型理论，软件重用，面向对象技术，部分实现技术，以及程序变换等。本项研究提出的方法是软件理论与语言理论相结合的成果，也是形式化方法和面向对象方法的一种较好的结合方式。
- 本项研究吸取了VDM方法和Z方法中模型的概念。保留了模型中不变式的约束条件，但是采用了规约语义，摈弃了烦琐的模型的构造过程和难读的精化正确性证明，避免了形式系统的潜在"陷阱"问题。
- 本项研究提出的变换型语言族模型，吸收了CIP的"广谱语言"和美国康乃尔大学的"POLYA语言"中变换的思想，使得软件规范有可能直接实现，同时采用了软件（语言）分层实现的方法，克服了广谱语言过于复杂，效率低下的缺点，也避免了POLYA语言中由于控制过于灵活而产生变换漩涡的隐患。
- 与国际上近年来兴起的"具体领域语言的研究"相比，本项研究的研究工作起步要超前五年左右，并且一开始就抓住具体领域语言的生成环境的问题，而不象目前许多研究停留在个别领域语言开发的层次上。
- 本项研究从语言及其构件的定义出发，提出的三种可重用部件是目前软件重用方法中所没有的。不仅抽象层次高，而且创意新颖，为可重用部件研究开创了一条新途径。
- 本项研究提出的"状态迁移理论"，改进了D.Gries教授提出的"气球理论"，使得循环不变式的推导更加自然和有效。
- 本项研究发展面向对象的方法，研究了语言之间的继承，屏蔽和扩充的关系，把对象的概念从抽象数据类型上升到语言的高度。
|
