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

作者：谢武平; 薛锦云

来源：计算机研究与发展, 2014, 51(04): 856-864.

DOI：10.7544/issn1000-1239.2014.20121058

• PAR方法
• Radl算法
• 程序生成
• 算法推导
• 生成规则

算法设计是一项创造性工作,传统的设计与描述方法难以保证算法的正确性.在PAR方法中通过定义具有数学引用透明性的算法描述语言Radl,可实现对问题规约进行形式化推导得到用递推关系描述的算法.Radl算法的核心就是递推关系组,从而易于进行形式化推导和证明.通过深入剖析Radl算法特性,揭示Radl算法与抽象顺序程序Apla(abstract programming language)间本质关系,定义基于Radl语法产生式的Apla程序生成规则,实现了Apla程序自动生成系统,并对其可靠性进行系统研究,着重形式化验证了实现系统的核心算法.使用PAR方法开发的算法是正确的,采用形式化证明的生成系统具有可靠性保证,从而保证了算法从设计到实现的高可靠性,并通过实现自动化开发工具提高了程序的开发效率.

• 单位
  江西省高性能计算技术重点实验室; 江西师范大学; 软件工程国家重点实验室; 武汉大学