Radl→Apla程序生成系统及其可靠性研究

摘要

随着信息技术的发展，计算机软件已经应用到了生活的各个方面，软件的可靠性也越来越受到关注，人们不仅对安全性至关重要软件系统提出了高可靠的要求，而且对于普通的应用软件也希望尽可能不出错。众所周知，传统的软件测试手段并不能满足人们对高质量软件的要求，而形式化开发方法因其具有严格的理论基础，可以用于开发正确、高效的程序。 本文实现了由Radl算法程序到Apla程序的映射过程，其中使用Radl语言来描述由PAR方法开发的算法程序，选用Apla语言作为映射的目标语言。为了使这种映射过程具有高可靠性，本文采用形式化的描述方法分别从词法、语法和语义三个层次精确地定义Radl语言，保证了Radl语言描述的程序正确地反映了推导所得算法的逻辑思想；并且基于Radl语言属性文法，以Radl语法产生式作为最小映射单元，定义了Radl语言映射单元到Apla语言语义单元的语义等价映射规则；同时采用形式化推导方法，根据Radl语言词法、语法、语义及Radl算法程序到Apla程序的映射规则的定义，推导出Radl语言词法分析、语法分析和语义分析实现的代表性算法。基于形式化推导的语法制导翻译的方法，将Radl算法程序按映射规则映射成Apla程序，保证了所实现的系统是在相关理论的指导下进行的，并且高可靠的实现了相关理论的要求。 本文主要做了如下几方面工作，其中某些方面具有一定的创新性： 1．分别形式化的定义Radl语言的词法、语法和语义。 2．以Radl语法产生式为单元，系统定义由Radl生成Apla程序的生成规则。 3．采用形式化推导方法得到生成系统的核心代表性算法。

目录

文摘

英文文摘

声明

第1章引 言

1.1研究背景

1.2研究内容

1.3本文组织

第2章形式化开发方法与形式化支撑工具

2.1形式化方法概述

2.2现有形式化开发方法

2.2.1B

2.2.2 Designware

2.2.3 VDM(Vienna Development Method)

2.2.4 Z

2.2.5 PAR

2.3形式化开发方法分析

2.4形式化支撑工具简介

第3章算法设计语言Radl

3.1 Radl语言概述

3.2 Radl语言的定义

3.2.1 Radl语言的词法定义

3.2.2 Radl语言的语法定义

3.2.3 Radl语言的语义定义

3.3 Radl语言应用实例

3.4 Radl语言小结

第4章Radl→ Apla程序生成系统设计与实现

4.1程序生成技术

4.2 Radl→Apla程序生成系统的设计

4.2.1系统总体结构设计

4.2.2系统详细设计

4.3 Radl→Apla程序生成系统的实现

4.3.1词法分析的实现

4.3.2语法分析的实现

4.3.3语义分析的实现

4.3.4程序生成的实现

4.4 Radl→Apla程序生成系统的几个实例

第5章Radl→Apla程序生成系统可靠性研究

5.1系统设计支撑理论的可靠性研究

5.1.1词法分析的可靠性研究

5.1.2语法分析的可靠性研究

5.1.3语义分析的可靠性研究

5.1.4程序生成的可靠性研究

5.2系统实现的可靠性研究

5.2.1词法分析代表算法的可靠性研究

5.2.2语法分析代表算法的可靠性研究

5.2.3语义分析及程序生成代表算法的可靠性研究

5.3系统可靠性研究小结

第6章总结与展望

参考文献

致谢

在读期间公开发表论文(著)及科研情况