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