Automatic verification of non-recursive algorithm of Hanoi Tower by using Isabelle Theorem Prover
Huazhen Xu, Zhen You, Jinyun Xue · 2016
Hanoi Tower problem is an ancient and interesting puzzle and Isabelle is one of famous proof assistants. We have put forward a method to verify the correctness of algorithmic programs based on Isabelle, and have presented formal derivation and proof about the non-recursive algorithm of Hanoi Tower problem in our previous work. The focus of this paper is to turn the former manual verification to automatic verification by using Isabelle Theorem Prover. On the other hand, we originally find a boundary function, which used to proof termination of our non-recursive algorithm of Hanoi Tower problem. This work realizes mechanically automatic-verifying the complete correctness of our non-recursive algorithm of Hanoi Tower Problem, and overcomes the intricacies of manual verification, improves the verification efficiency, and ensures the trustworthiness and reliability of the algorithm program.