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

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

关于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.