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

• 作者: 游珍 薛锦云
• 来源期刊: 计算机研究与发展
• 学科: 工学
• 关键词: Hanoi塔 PAR方法 循环不变式 非递归算法 Dijkstra最弱前置谓词法
• 年，卷（期）: 2008,（z1）
• 所属期刊栏目: 数据、程序及其理论
• 页码范围: 143-147
• 页数: 5页
• 分类号: TP301.6
• 字数: 3233字
• 语种: 中文

摘要

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

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	薛锦云		8	47	5.0	6.0
5	游珍		5	45	5.0	5.0