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

Formal Derivation and Correctness Proof of Non-Recursion Algorithm for Tower-of-Hanoi

作　　者：游珍[1,2] 薛锦云[1,2,3] 

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

出　　处：《计算机研究与发展》2008年第z1期143-147,共5页Journal of Computer Research and Development

基　　金：国家自然科学基金项目(60273092)

摘　　要：关于Hanoi塔问题的非递归算法已有大量的研究.运用薛锦云教授自创的PAR方法和循环不变式开发的新策略,形式化推导出逻辑结构清晰的Hanoi塔非递归算法及其循环不变式,并用Dijkstra最弱前置谓词法验证了该算法的正确性.充分体现了PAR方法的优越性、高效性和可靠性.There have been lots of researches on non-recursion algorithms for tower-of-Hanoi. According to professor Xue Jinyun's PAR method and new strategies for developing loop invariant, a clear logical non-recursion algorithm for tower-of-Hanoi and its loop invariant are forally deduced. Meanwhile, the correctness proof of this algorithm is given using Dijkstra's weakest precondition method. Superiority, efficiency and dependability of PAR method are also presented.

关 键 词：HANOI塔 PAR方法 循环不变式 非递归算法 Dijkstra最弱前置谓词法 

分 类 号：TP301.6[自动化与计算机技术—计算机系统结构]