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

摘要：

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

关键词： PAR方法 形式化推导 算法程序 递推关系 自动生成 软件转换

作者: 胡启敏 薛锦云

作者单位: 江西省高性能计算技术重点实验室,南昌,330022 江西师范大学瑶湖校区计算机信息工程学院,南昌,330022

会议类型: 国内会议

会议名称: 2007全国理论计算机科学学术年会

会议地点: 南宁

会议语种:中文

页码: 148-153

在线出版日期: 2007-11-01（万方平台首次上网日期，不代表论文的发表时间）