摘要
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.
出处
《计算机研究与发展》
EI
CSCD
北大核心
2008年第z1期148-153,共6页
Journal of Computer Research and Development
基金
国家自然科学基金项目(60273092)
国家“九七三”重点基础研究发展规划基金项目(2003CCA02800)
江西师范大学青年成长基金项目(1323)
关键词
PAR方法
形式化推导
算法程序
递推关系
PAR method
formal derivation
algorithmic program
recurrence relation
