Radl算法到Apla程序的生成系统  

Research on Generation System from Radl Algorithm to Apla Program

作　　者：谢武平[1,2,3] 薛锦云[1,2,3] 

机构地区：[1]软件工程国家重点实验室(武汉大学),武汉430072 [2]江西省高性能计算技术重点实验室(江西师范大学),南昌330022 [3]武汉大学计算机学院,武汉430072

出　　处：《计算机研究与发展》2014年第4期856-864,共9页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(60573080;60273092);国家自然科学基金重大国际(地区)合作研究项目(61020106009)

摘　　要：算法设计是一项创造性工作,传统的设计与描述方法难以保证算法的正确性.在PAR方法中通过定义具有数学引用透明性的算法描述语言Radl,可实现对问题规约进行形式化推导得到用递推关系描述的算法.Radl算法的核心就是递推关系组,从而易于进行形式化推导和证明.通过深入剖析Radl算法特性,揭示Radl算法与抽象顺序程序Apla(abstract programming language)间本质关系,定义基于Radl语法产生式的Apla程序生成规则,实现了Apla程序自动生成系统,并对其可靠性进行系统研究,着重形式化验证了实现系统的核心算法.使用PAR方法开发的算法是正确的,采用形式化证明的生成系统具有可靠性保证,从而保证了算法从设计到实现的高可靠性,并通过实现自动化开发工具提高了程序的开发效率.Designing algorithm is a creative activity.The traditional design and description methods are difficult to ensure the correctness of algorithm.By defining algorithm description language Radl with mathematical referential transparency in the PAR method,the algorithm described by recursive relation can be obtained from deriving problem specification formally.The core of the algorithm is the recursive relation group,and therefore,it is easy to deduce and prove Radl algorithm formally.By deeply analyzing Radl language and Radl algorithm characteristics,the essential relationship between the Radl algorithm and abstract sequential program Apla is revealed,and Apla program generation rules based on Radl grammar productions are defined.Then Apla program automatic generation system is achieved and the system＇s reliability is studied.Finally the core algorithm of the system is verified formally.The algorithm developed by PAR method is correct,and the generation system which is proved formally can be assured reliably.So the high reliability of algorithm is ensured,and the automation development tools improve the development efficiency of program.

关 键 词：PAR方法 Radl算法 程序生成 算法推导 生成规则 

分 类 号：TP301[自动化与计算机技术—计算机系统结构]