Unified formal derivation and automatic verification of three binary-tree traversal non-recursive algorithms
Unified formal derivation and automatic verification of three binary-tree traversal non-recursive algorithms
复制标题
DOI：
10.1007/s10586-016-0663-9
复制
发表时间：
2016-10
期刊：
影响因子：
--
通讯作者：
左正康
中科院分区：
文献类型：
--
作者：
游珍;薛锦云;左正康
二叉树遍历算法可应用于很多方面，比如信息加密、网络、操作系统、集群计算等等。我们已经提出了一种基于……来验证算法程序正确性的有用方法。
（原句中“based on Is”似乎不完整，可能影响了更准确的翻译）
Binary tree traversal algorithm can be applied in many aspects, such as information encryption, Network, operating systems, cluster computing and so on. We have already proposed a useful method to verify the correctness of algorithmic programs based on Isabelle proof assistant and Dijkstra’s weakness precondition theory, and have manually derived and verified binary tree traversal non-recursive algorithms in our previous work. In order to ensure the security of the non-recursive algorithms, the focus of this paper is to construct a unified recurrence-relations expression about preorder, in-order, and post-order binary tree traversal non-recursive algorithms. The recurrence-relations expression make it easier to derive the loop invariants of three algorithms. Meanwhile, we automatically verify the correctness of three kinds of non-recursive algorithms by using a generic proof assistant Isabelle. This work realizes mechanically automatic-verification and overcomes the intricacies and weakness of manual verification, improves the verification efficiency, and ensures the trustworthiness and reliability of the algorithm program.
登录
查看更多内容
DOI：
10.1109/clustr.2007.4629232
发表时间：
2007-09
期刊：
2007 IEEE International Conference on Cluster Computing
影响因子：
--
作者：
Akihiro Nomura;Hiroya Matsuba;Y. Ishikawa
通讯作者：
Akihiro Nomura;Hiroya Matsuba;Y. Ishikawa
DOI：
10.1109/itap.2011.6006183
发表时间：
2011-08
期刊：
2011 International Conference on Internet Technology and Applications
影响因子：
--
作者：
Ruijun Zhang;Bichao Gong
通讯作者：
Ruijun Zhang;Bichao Gong
影响因子：
2.4
作者：
K. Ammari;D. Mercier;V. Régnier
通讯作者：
K. Ammari;D. Mercier;V. Régnier
DOI：
10.1007/978-3-642-22543-7_7
发表时间：
2011-07
期刊：
--
影响因子：
--
作者：
Rajender Dharavath;K. Bhima;Kalyanaraman Shankari;A. Jagan
通讯作者：
Rajender Dharavath;K. Bhima;Kalyanaraman Shankari;A. Jagan
DOI：
10.1109/icfem.1997.630419
发表时间：
1997-11
期刊：
First IEEE International Conference on Formal Engineering Methods
影响因子：
--
作者：
Jinyun Xue;Ruth Davis
通讯作者：
Jinyun Xue;Ruth Davis