东篱科研大数据发现系统（DRDS）

位置：成果数据库 > 期刊 > 期刊详情页

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

ISSN号：1000-1239
期刊名称：计算机研究与发展
时间：2014.4.15
页码：856-864
分类：TP301[自动化与计算机技术—计算机系统结构;自动化与计算机技术—计算机科学与技术]
作者机构：[1]软件工程国家重点实验室(武汉大学),武汉430072, [2]江西省高性能计算技术重点实验室(江西师范大学),南昌330022, [3]武汉大学计算机学院,武汉430072
相关基金：国家自然科学基金项目（60573080,60273092）;国家自然科学基金重大国际（地区）合作研究项目（61020106009）
相关项目：若干软件新技术及其在PAR平台中的实验研究

关键词： PAR方法, Radl算法, 程序生成, 算法推导, 生成规则, PAR method, Radl algorithms, program generation, algorithm derivation, generation rule

中文摘要：

算法设计是一项创造性工作,传统的设计与描述方法难以保证算法的正确性.在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.

同期刊论文项目