主页

科研

M O S A T

  分层模型
  理论基础
  GARMENT
  GARADA
  相关论文
  课题综述

面向模型的变换型软件开发方法

面向模型的变换型软件开发方法把数据抽象的思想提高到语言抽象层次；把一类专用软件的规范抽象为语言的规范；把这类软件的实现抽象为语言的归约变换；用“规范+变换”抽象软件开发过程。

为支持这种方法，提出了语言的一种抽象与封装机制Garment，以此定义语言中各成分的语法和语义，描述语言间的继承、屏蔽和扩充关系。

设计并实现了一个支持Garment的软件开发环境"GARADA"，目标语言是 Ada95 。

分层模型

"面向模型的变换型软件开发方法"把程序开发、软件开发和软件开发环境的开发视为三种不同层次上的活动，它们之间的关系可以用下图来表示：

理论基础

为语言族中的语言建立了一个代数模型，给出了语言的继承、屏蔽和扩充的语义。此代数模型是抽象数据类型代数模型的升华。

通过研究Garment中的归约语义，提出了语言可归约的充分条件。

研究了Garment中的约束多态类型，给出了类型检查算法，证明了此算法中约束的可满足性是可判定的。

提出了Garment中参数化多态类型和约束多态类型的Ideal语义，并以此证明了Garment中的类型规则的语义可靠性。

提出循环不变式的"状态迁移理论"，并将其成功地用于不变式的开发，使得不变式的推导更加自然有效。

GARMENT

要实现面向模型的变换型软件开发方法，首先要提供一种语言的描述机制，用于描述专用软件所需实现的专用语言，我们称这种语言描述机制为Garment。 一个Garment规范就是一个语言的抽象与封装。Garment 定义语言中各成分的语法和语义，描述语言间的继承、屏蔽和扩充关系。

Garment机制中还融入了组件化的设计思想，语言可以按照其语法结构被分解为词法、表达式、语句等组件。通过重用，实现了对语言定义的继承和扩充功能。Garment给出了三种层次上的重用方法，为建立大型语言知识库提供了灵活的手段。这三种方法分别是：

• 语言的完整定义（即一个Garment）作为最高层的可重用部件。
• 语言的一类语法成分（例如语言中所有表达式）的定义作为中层的可重用部件。
• 语言的具体语法成分（例如一个具体语句）的定义作成为一个变换模块为低层的可重用部件。

GARADA

GARADA95是以Ada95为目标语言的Garment程序综合开发环境（GIDE）。它集成了Garment程序编译器、生成的用户语言解释器、Ada95语言排版工具（pretty printer）、Ada95语言编译器等一系列工具，极大的方便了Garment程序和用户语言应用程序的开发。GARADA95系统的结构如下图所示。

我们已经使用GARADA95成功的开发了三个典型的小型软件：

• 顺序语言PL0及其程序到Ada95语言程序的转换系统；
• 并行语言UNITY-BD及其程序到Ada95语言程序的转换系统；
• 控制决策语言VERT及其程序到Ada95语言程序的转换系统。

GARADA95系统（包括文档说明、示例、源程序等）可以由此下载

相关论文

在本课题十余年的研究过程中，发表论文近二十篇，具体可见相关论文列表。

课题综述

关于面向模型的变换型软件开发方法的背景、发展阶段、取得的进展和特色可以参见课题综述。