• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>Companion of the IEEE International Conference on Software Quality, Reliability, and Security >Non-recursive Algorithm Derivation and Formal Proof of Binary Tree Traversal Class Problems
【24h】

Non-recursive Algorithm Derivation and Formal Proof of Binary Tree Traversal Class Problems

机译：非递归算法衍生和二叉树遍历类问题的正式证明

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

The development of loop invariants for recursive problems of nonlinear data structures is always difficult problem in formal development. The paper studies the derivation and formal proof of binary tree traversal class non-recursive algorithm. The non-recursive Apla (Abstract Programming Language) algorithms of binary tree traversal class problems and their exact and simple loop invariants are derived. Then, the correctness of the algorithm is proved by Dijkstra-Gries standard proving technique. Finally, the PAR platform is used to automatically generate C++ code, which realizes the complete refinement process from abstract specification to concrete executable program. The results of this study point out the direction for the exploration of the loop invariant of the nonrecursive algorithm for recursive problems and have guiding significance for the derivation and formal proof of the algorithm program of the nonlinear data structure.
机译：非线性数据结构递归问题的循环不变的开发始终是正式发展中的难题。本文研究了二叉树遍历类非递归算法的衍生和正式证明。派生了二叉树遍历类问题的非递归APLA（抽象编程语言）算法及其精确和简单的循环不变。然后，Dijkstra-Gries标准证明技术证明了算法的正确性。最后，PAR平台用于自动生成C ++代码，从而实现了从抽象规范到具体可执行程序的完整细化过程。本研究的结果指出了探索递归问题的非持久性算法的循环不变的方向，并且对非线性数据结构的算法程序的推导和正式证明具有指导意义。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号