形式化开发Hanoi塔问题非递归算法  

Formal development of non-recursive algorithm for Hanoi tower

作　　者：石海鹤[1] 石海鹏[2] 薛锦云[1] 

机构地区：[1]江西师范大学计算机信息工程学院 [2]江西师范大学软件学院,南昌330022

出　　处：《计算机工程与应用》2007年第11期96-99,共4页Computer Engineering and Applications

基　　金：国家自然科学基金(the National Natural Science Foundation of China under Grant No.60573080)。

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

关 键 词：HANOI塔问题 形式化方法 非递归 PAR方法 循环不变式 

分 类 号：TP311.1[自动化与计算机技术—计算机软件与理论]