Hanoi塔非递归算法的形式化推导和正确性验证

摘要：

关于Hanoi塔问题的非递归算法已有大量的研究.运用薛锦云教授自创的PAR方法和循环不变式开发的新策略,形式化推导出逻辑结构清晰的Hanoi塔非递归算法及其循环不变式,并用Dijkstra最弱前置谓词法验证了该算法的正确性.充分体现了PAR方法的优越性、高效性和可靠性.

关键词： Hanoi塔 PAR方法 循环不变式 非递归算法 Dijkstra最弱前置谓词法 形式化推导

作者: 游珍 薛锦云

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

会议类型: 国内会议

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

会议地点: 南宁

会议语种:中文

页码: 143-147

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