文献类型：期刊文章

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

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

出　　处：《计算机研究与发展》

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

年　　份：2008

卷　　号：45

期　　号：z1

起止页码：148-153

语　　种：中文

收录情况：AJ、BDHX、BDHX2004、CSA-PROQEUST、CSCD、CSCD2011_2012、EI、IC、JST、RCCSE、SCOPUS、ZGKJHX、核心刊

摘　　要：PAR方法基于分划与递推、量词变换规则、循环不变式开发新策略和软件转换工具,实现了复杂算法问题的形式化开发.采用PAR方法形式化推导几个典型的算法问题.通过量词变换规则对程序规约进行形式化推导,可以得到具有数学引用透明性、易于形式化证明的求解算法问题的递推关系;并在此基础上,自然地导出循环不变式.在得到简短、易于理解、高可靠性的Apla算法程序之后,通过转换工具自动生成Java,C++等可执行程序.

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

分 类 号：TP301.6]