Derivation and Formal Proof of Binary Tree Depth Non-Recursive Algorithm

Zhengkang Zuo,Yue Fang,Qing Huang,Yunyan Liao,Yuan Wang,Changjing Wang

2021 5th International Conference on Communication and Information Systems (ICCIS)（2021）

引用 0|浏览0

暂无评分

摘要

The development of loop invariants for recursive problems of nonlinear data structures are always difficult problems in formal development. The paper studies the derivation and formal proof of binary tree non-recursive algorithm. The non-recursive Apla algorithm of binary tree depth and its exact and simple loop invariant are derived. Then, Dijkstra-Gries’ standard proving technique is used to pro...

查看译文

关键词

algorithm of binary tree depth,loop invariant,Dijkstra-Gries’ standard proving technique,Apla to C++ program automatic generation system,nonlinear data structure

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要