| Hanoi塔非递归算法的形式化推导和正确性验证 |
| |
| 引用本文： | 游珍,薛锦云.Hanoi塔非递归算法的形式化推导和正确性验证[J].计算机研究与发展,2008,45(Z1):143-147. |
| |
| 作者姓名： | 游珍 薛锦云 |
| |
| 作者单位： | 江西省高性能计算技术重点实验室,南昌,330022;江西师范大学计算机信息工程学院,南昌,330022 |
| |
| 摘 要： | 关于Hanoi塔问题的非递归算法已有大量的研究.运用薛锦云教授自创的PAR方法和循环不变式开发的新策略,形式化推导出逻辑结构清晰的Hanoi塔非递归算法及其循环不变式,并用Dijkstra最弱前置谓词法验证了该算法的正确性.充分体现了PAR方法的优越性、高效性和可靠性.
|
| 关 键 词： | Hanoi塔 PAR方法 循环不变式 非递归算法 Dijkstra最弱前置谓词法 |
| 修稿时间： | 2007年7月10日 |
Formal Derivation and Correctness Proof of Non-Recursion Algorithm for Tower-of-Hanoi |
| |
| You Zhen,Xue Jinyun.Formal Derivation and Correctness Proof of Non-Recursion Algorithm for Tower-of-Hanoi[J].Journal of Computer Research and Development,2008,45(Z1):143-147. |
| |
| Authors: | You Zhen Xue Jinyun |
| |
| Affiliation: | You Zhen1,2 , Xue Jinyun1,2,31(Provincial Key Laboratory for High Performance Computing Techology,Nanchang 330022)2(College of Computer Information , Engineering,Jiangxi Normal University,Nanchang 330022)3(Key Laboratory for Computer Science,Institute of Software,Chinese Academy of Sciences,Beijing 100080) |
| |
| Abstract: | 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. |
| |
| Keywords: | tower-of-Hanoi PAR method loop invariant non-recursion algorithm Dijkstra's weakest precondition method |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
