版权所有：内蒙古大学图书馆 技术提供：维普资讯• 智图
内蒙古自治区呼和浩特市赛罕区大学西街235号 邮编: 010021
Hanoi塔非递归算法的形式化推导和正确性验证
Formal Derivation and Correctness Proof of Non-Recursion Algorithm for Tower-of-Hanoi作者机构：江西省高性能计算技术重点实验室南昌330022 江西师范大学计算机信息工程学院南昌330022 中国科学院软件研究所计算机科学重点实验室
出 版 物：《计算机研究与发展》 (Journal of Computer Research and Development)
年 卷 期：2008年第45卷第z1期
页 面：143-147页
核心收录：
学科分类：08[工学] 081202[工学-计算机软件与理论] 0812[工学-计算机科学与技术（可授工学、理学学位）]
主 题：Hanoi塔 PAR方法 循环不变式 非递归算法 Dijkstra最弱前置谓词法
摘 要：关于Hanoi塔问题的非递归算法已有大量的研究.运用薛锦云教授自创的PAR方法和循环不变式开发的新策略,形式化推导出逻辑结构清晰的Hanoi塔非递归算法及其循环不变式,并用Dijkstra最弱前置谓词法验证了该算法的正确性.充分体现了PAR方法的优越性、高效性和可靠性.
