典型文献
A Unified Strategy for Formal Derivation and Proof of Binary Tree Nonrecursive Algorithms
文献摘要：
In the formal derivation and proof of binary tree al-gorithms,Dijkstra's weakest predicate method is commonly used.However,the method has some drawbacks,including a time-consuming derivation process,complicated loop invariants,and the inability to generate executable programs from the specification.This paper proposes a unified strategy for the for-mal derivation and proof of binary tree non-recursive algorithms to address these issues.First,binary tree problem solving se-quences are decomposed into two types of recursive relations based on queue and stack,and two corresponding loop invariant templates are constructed.Second,high-reliability Apla(abstract programming language)programs are derived using recursive re-lations and loop invariants.Finally,Apla programs are con-verted automatically into C++executable programs.Two types of problems with binary tree queue and stack recursive relations are used as examples,and their formal derivation and proof are performed to validate the proposed strategy's effectiveness.This strategy improves the efficiency and correctness of binary tree algorithm derivation.
文献关键词：
中图分类号：
作者姓名：
ZUO Zhengkang;HUANG Zhipeng;FANG Yue;HUANG Qing;WANG Yuan;WANG Changjing
作者机构：
College of Computer Information Engineering,Jiangxi Normal University,Nanchang 330022,Jiangxi,China;College of Software,Jiangxi Normal University,Nanchang 330022,Jiangxi,China
文献出处：
引用格式：
[1]ZUO Zhengkang;HUANG Zhipeng;FANG Yue;HUANG Qing;WANG Yuan;WANG Changjing-.A Unified Strategy for Formal Derivation and Proof of Binary Tree Nonrecursive Algorithms)[J].武汉大学自然科学学报（英文版）,2022(05):415-423
A类：
executable,C++executable
B类：
Unified,Strategy,Formal,Derivation,Proof,Binary,Tree,Nonrecursive,Algorithms,In,formal,derivation,proof,binary,tree,Dijkstra,weakest,predicate,method,commonly,used,However,has,some,drawbacks,including,consuming,process,complicated,loop,invariants,inability,generate,programs,from,specification,This,paper,proposes,unified,strategy,algorithms,address,these,issues,First,solving,quences,are,decomposed,into,two,types,relations,queue,stack,corresponding,templates,constructed,Second,high,reliability,Apla,abstract,programming,language,derived,using,Finally,verted,automatically,Two,problems,examples,their,performed,validate,proposed,effectiveness,improves,efficiency,correctness
AB值：
0.542269
相似文献
机标中图分类号，由域田数据科技根据网络公开资料自动分析生成，仅供学习研究参考。
