若干算法程序的形式化推导与生成技术研究  

Research on the Formal Derivation and Generation Technique of Several Algorithmic Programs

作　　者：胡启敏[1,2,3] 薛锦云[1,2,3] 

机构地区：[1]中国科学院软件研究所计算机科学重点实验室 [2]江西师范大学瑶湖校区计算机信息工程学院,南昌330022 [3]江西省高性能计算技术重点实验室,南昌330022

出　　处：《计算机研究与发展》2008年第z1期148-153,共6页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(60273092);国家“九七三”重点基础研究发展规划基金项目(2003CCA02800);江西师范大学青年成长基金项目(1323)

摘　　要：PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于形式化证明的求解算法问题的递推关系;并在此基础上,自然地导出循环不变式.在得到简短、易于理解、高可靠性的Apla算法程序之后,通过转换工具自动生成Java,C++等可执行程序.Based on partition and recurrence, rules of quantifier transformation, new strategies for developing loop invariants, and software transforming tools, a unified formal approach called PAR method gives a new way to develop complicated algorithmic programs. Several typical algorithms are formally derived using PAR method. The derivation can achieve algorithms represented by recurrence relation which has mathmatical transpanrency and is provable. Loop invariants of those algorithms can be educed naturally using recurrence relation. Finally the derivation can obtain brief reliable Apla programs which can be translated into Java, C++ programs with correlative tools.

关 键 词：PAR方法 形式化推导 算法程序 递推关系 

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