Abstract: This paper develops non-recursive algorithmic program of Hanoi tower problem employing PAR method and the new strategy of developing loop invariant and verifies the program formally. This paper aims at non-recursive algorithms directly, and achieves loop invariant of Hanoi tower problem with readable, efficient and reliable non-recursive algorithm finally. The paper contributes to developing non-recursive algorithm using formal method and new strategy of developing loop invariant.

Key words: Hanoi tower problem, Formal method, Non-recursive, PAR method, Loop invariant

摘要： 使用形式化方法PAR及循环不变式开发新策略，开发了Hanoi塔问题非递归算法，并对其进行了形式化地正确性证明。本文直接面向非递归算法，在得到求解Hanoi塔问题的循环不变式的同时，直接得到易读、高效且可靠的非递归算法。对使用形式化方法及循环不变式开发新策略开发非递归算法作了较深入的实践和探讨。

关键词: Hanoi塔问题, 形式化方法, 非递归, PAR方法, 循环不变式