[1]左正康,方 越,黄 箐,等.二叉树排序非递归算法推导及形式化证明[J].江西师范大学学报(自然科学版),2020,(06):625-632.[doi:10.16357/j.cnki.issn1000-5862.2020.06.14]
　ZUO Zhengkang,FANG Yue,HUANG Qing,et al.The Derivation and Formal Proof of Binary Tree Sorting Non-Recursive Algorithm[J].Journal of Jiangxi Normal University:Natural Science Edition,2020,(06):625-632.[doi:10.16357/j.cnki.issn1000-5862.2020.06.14]
点击复制

二叉树排序非递归算法推导及形式化证明()
分享到：

《江西师范大学学报》（自然科学版）[ISSN:1006-6977/CN:61-1281/TN]

卷:
期数:
2020年06期
页码:
625-632
栏目:
信息科学与技术
出版日期:
2020-12-20

文章信息/Info

Title:
The Derivation and Formal Proof of Binary Tree Sorting Non-Recursive Algorithm
文章编号:
1000-5862(2020)06-0625-08
作者:
左正康1; 方 越1; 黄 箐1; 廖云燕1; 王 渊2; 王昌晶1*
1.江西师范大学计算机信息工程学院,江西 南昌 330022; 2.江西师范大学软件学院,江西 南昌 330022
Author(s):
ZUO Zhengkang1; FANG Yue1; HUANG Qing1; LIAO Yunyan1; WANG Yuan2; WANG Changjing1*
1.College of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China; 2.College of Software,Jiangxi Normal University,Nanchang Jiangxi 330022,China
关键词:
二叉树类非递归算法;  循环不变式;  PAR 平台;  Dijkstra-Gries标准程序证明法;  非线性数据结构
Keywords:
binary tree class non-recursive algorithm;  loop invariant;  PAR platform;  Dijkstra-Gries standard proving technique;  nonlinear data structure
分类号:
TP 311
DOI:
10.16357/j.cnki.issn1000-5862.2020.06.14
文献标志码:
A
摘要:
非线性数据结构递归问题非递归算法的循环不变式的开发一直是形式化开发的难点.研究二叉树类非递归算法的推导及形式化证明方法,对二叉树排序算法进行推导,得出非递归Apla(Abstract Programming Language)算法及其精确而简单的循环不变式,然后用Dijkstra-Gries标准程序证明法证明算法的正确性,最后使用PAR平台C++程序自动生成系统自动生成C++代码.实例的实验结果简化了算法程序的推导和证明过程,对递归问题非递归算法的循环不变式的探测具有一定的借鉴意义,而且对非线性数据结构算法程序的推导及形式化证明具有指导意义.
Abstract:
The development of loop invariants for recursive problems of nonlinear data structures are always difficult problems in formal development.In this paper,an approach for the derivation and formal proof of binary tree non-recursive algorithm are researched,and the non-recursive Apla(Abstract Programming Language)algorithm of binary tree sorting algorithm and its exact and simple loop invariant are derived.Then,the correctness of the algorithm is proved by Dijkstra-Gries standard proving technique.In the end,the PAR platform C++ program automatic generation system automatically generates C++ code.The experimental results of the example simplify the derivation and proof of the algorithm program and are useful for the direction for the exploration of loop invariant of non-recursive algorithm for recursive problems,which has guiding significance for the formal proof of algorithm program for nonlinear data structure.

参考文献/References:

[1] Zhu Zhenyuan,Zhu Cheng.Non-recursive implementation of recursive algorithm[J].Journalof Chinese Computer Systems,2003,23(3):567-570.
[2] Gries D.The science of programming[M].New York:Springer,1981.
[3] Dijkstra E W.A discipline of programming[M].Upper Saddle River:Prentice Hall,1976.
[4] Xue Jinyun.Two new strategies for developing loop invariants and their applications[J].Journal of Computer Science and Technology,1993,8(3):147-154.
[5] Xue Jinyun,Zheng Yujun,Hu Qimin,et al.PAR:a practicable formal method and its supporting platform[EB/OL].[2019-05-17].https://link.springer.com/chapter/10.1007/978-3-030-02450-5_5.
[6] 左正康,游珍,薛锦云.后序遍历二叉树非递归算法的推导及形式化证明[J].计算机工程与科学,2010,32(3):119-123.
[7] Gargantini G,Riccobene A E,Scandurra P.Combining formal methods and MDE techniques for model-driven system design and analysis[J].International Journal on Advances in Software,2010,3(1/2):1-18.
[8] Brooks F P.No silver bullet:essence and accidents of software engineering[J].IEEEComputer,1987,20(4):10-19.
[9] Floyd R W.Assigning meaning to programs[EB/OL].[2019-06-12].https://link.springer.com/chapter/10.1007%2F978-94-011-1793-7_4.
[10] Hoare C A R.An axiomatic basis for computer programming[J].Communications Ofthe ACM,1969,12(10):117-126.
[11] Owicki S,Gries D.An axiomatic proof technique for parallel programs I[J].Act a Informatica,1976,6(4):319-340.
[12] Sankaranarayanan S,Sipma H B,Manna Z.Non-linear loop invariant generation using grobner bases[C]∥ACM SIGPLAN Principles of Programming Languages.NewYork: ACM Press,2004:318-329.
[13] Colon M,Sankaranarayanan S,Sipma H.Linear invariant generation using non-linearconstraint solving[C]∥Computer-Aided Verfication,LNCS 2725.Heidelberg:Springer Berleg,2003:420-433.
[14] Coust P,Coust R.Abstract interpretation:a unified lattice model for static analysis of programs by construction or approximation of fixpoints[C]∥ACM Principles of Programming Language.New York:ACMPress,1997:238-252.
[15] Cousot P,Halbwachs N.Automatic discovery of linear restraints among the variables of a program[C]∥ACM Principles of Programming Languages.New York:ACM Press,1978:84-97.
[16] 余伟.基于消元法生成非线性循环不变式[J].电子技术与软件工程,2014,16(8):264-266.
[17] Arora N,Kumar Tamta V,Kumar S.Modified non-recursive algorithm for reconstructing a binary tree[J].International Journal of Computer Applications,2012,43(10):25-28.
[18] Das V V.A new non-recursive algorithm for reconstructing a binary tree from its traversals[EB/OL].[2019-05-13].https://ieeexplore.ieee.org/document/5656782.
[19] Loginov A,Reps T,Sagiv M.Automated verification of the Deutsch-Schorr-Waitetree-traversal algorithm[M].Berlin:Static Analysis,Springer,2006:261-279.
[20] 胡启敏,薛锦云,游珍,等.PAR平台中若干软件构件形式化验证技术研究[J].计算机工程与科学,2018,40(2):268-274.
[21] Xue Jinyun.Developing the generic path algorithmic program and its instantiations using PAR method[C]∥The Second Asia Workshop on Programming Languages and Systems.Daejeon:APLAS,2001:159-169.
[22] 石海鹤,薛锦云.基于PAR的算法形式化开发[J].计算机学报,2009,32(5):982-991.
[23] 石海鹤,薛锦云.基于PAR的排序算法自动生成研究[J].软件学报,2012,23(9):2248-2260.
[24] Xue Jinyun.PAR:a model driven engineering platform for generating algorithms and software[C]∥Programming:Logics,Models,Algorithms and Concurrency to recognize Jayadev Misra's Accomplishments.Austin:University of Texas Press,2016:150-154.
[25] Xue Jinyun.A unified approach for developing efficient algorithmic programs[J].Journal of Computer Science and Technology,1997,12(4):314-320.
[26] 杨黄磊,薛锦云.一类单元赋值语句型循环不变式的开发方法研究[J].江西师范大学学报:自然科学版,2014,38(4):378-382.
[27] Gosling J,Joy W,Steele G,et al.The Java language specification[M].3rd Edition.New Jersey:Addison Wesley Press,2005.
[28] You Zhen,Xue Jinyun,Zuo Zhengkang.Unified formal derivation and automatic verificationof three binary-tree traversal non-recursive algorithms[J].Cluster Computing,2016,19:2145-2156.
[29] 谢武平,薛锦云.Radl算法到Apla程序的生成系统[J].计算机研究与发展,2014,51(4):856-864.
[30] 赖勇.APLA到C++自动程序转换系统的研制[D].南昌:江西师范大学,2002.
[31] Bryant R E,Clarke E M,Grumberg O.Research on automatic verification of finite-state concurrent systems[J].Annual Review of Computer Science,1987,2(1):269-290.
[32] Yang Qinghong,Li Yunqing.A program development method based on program correctness proof theory[J].Computer Application Research,2001,18(2):11-13.
[33] Havelund K.Pressbu rger t.Model checking programs using Java path finder[J].International Journal on Software Tools forTechnology Transfer,2000,2(4):366-381.
[34] Xue Jinyun,Gries D.Developing a line algorithm for cubing a cycle permutation[J].Science of Computer Programming,1988,11(2):161-165.
[35] 夏鲸.并发分布式事务处理机制在PAR平台中的设计与实现[D].南昌:江西师范大学,2018.
[36] 游珍.Isabelle定理证明器的剖析及其在PAR方法/PAR平台中的应用[D].南昌:江西师范大学,2009.
[37] Sutton A,Maletic J I.Emulating C++0x Concepts[J].Science of Computer Programming,2013,78(9):1449-1469.
[38] Li Mengjun.Formal characterization and verification of loop invariant based on finite difference[EB/OL].[2012-06-30].https://cs.nyu.edu/acsys/wing2012/abstracts/menghun.pdf.
[39] Furia C A,Meyer B.Inferring loop invariants using postconditions[M]∥Blass A,Dershowitz N,Peisig W.Fields of logic and computation.Berlin,Heidelberg:Springer Verlag,2010:277-300.
[40] 万松松,薛锦云,谢武平.循环不变式开发技术研究[J].计算机工程与科学,2010,32(9):84-88.
[41] CCF形式化方法专业委员会.形式化方法的研究进展与趋势[M].北京:机械工业出版社,2018:1-68.
[42] CCF软件工程专业委员会.软件分析:技术、应用与趋势[M].北京:机械工业出版社,2016:56-114.
[43] 张健,张超,玄跻峰,等.程序分析研究进展[J].软件学报,2019,30(1):80-109.
[44] 马晓星,刘譞哲,谢冰,等.软件开法方法发展回顾与展望[J].软件学报,2019,30(1):3-21.
[45] 王戟,詹乃军,冯新宇,等.形式化方法概貌[J].软件学报,2019,30(1):33-61.

相似文献/References:

[1]古素梅,杨庆红*.2类数列问题循环不变式开发策略研究与应用[J].江西师范大学学报(自然科学版),2020,(03):307.[doi:10.16357/j.cnki.issn1000-5862.2020.03.15]
　GU Sumei,YANG Qinghong*.The Research and Application of Loop Invariant Development Strategy for Two Kinds of Sequence Problems[J].Journal of Jiangxi Normal University:Natural Science Edition,2020,(06):307.[doi:10.16357/j.cnki.issn1000-5862.2020.03.15]
[2]王昌晶,贺江飞,罗海梅,等.模型驱动的Dafny程序形式化生成与自动验证[J].江西师范大学学报(自然科学版),2020,(04):378.[doi:10.16357/j.cnki.issn1000-5862.2020.04.09]
　WANG Changjing,HE Jiangfei,LUO Haimei,et al.The Model-Driven Dafny Program Generation and Automatic Verification[J].Journal of Jiangxi Normal University:Natural Science Edition,2020,(06):378.[doi:10.16357/j.cnki.issn1000-5862.2020.04.09]
[3]刘晓丹,胡 颖,左正康*.图搜索问题算法推导及形式化证明[J].江西师范大学学报(自然科学版),2021,(06):642.[doi:10.16357/j.cnki.issn1000-5862.2021.06.14]
　LIU Xiaodan,HU Ying,ZUO Zhengkang*.The Derivation and Formal Proof of Graph Search Algorithm[J].Journal of Jiangxi Normal University:Natural Science Edition,2021,(06):642.[doi:10.16357/j.cnki.issn1000-5862.2021.06.14]
[4]左正康,方 越,黄志鹏,等.二叉树队列关系问题非递归算法的推导及形式化证明[J].江西师范大学学报(自然科学版),2022,(01):49.[doi:10.16357/j.cnki.issn1000-5862.2022.01.07]
　ZUO Zhengkang,FANG Yue,HUANG Zhipeng,et al.The Derivation and Formal Proof of Non-Recursive Algorithm for Binary Tree Queue Relation Problems[J].Journal of Jiangxi Normal University:Natural Science Edition,2022,(06):49.[doi:10.16357/j.cnki.issn1000-5862.2022.01.07]

备注/Memo

备注/Memo:
收稿日期:2019-10-17
基金项目:国家自然科学基金(61862033,61762049,61902162),江西省自然科学基金(20202BABL202026,2020BABL202025,20202BAB202015)和国家留学基金(202008360094)资助项目.
作者简介:左正康(1980-),男,江西抚州人,教授,博士,主要从事软件形式化、可信软件方面的研究.E-mail:kerrykaren@126.com
通信作者:王昌晶(1977-),男,江西南昌人,教授
更新日期/Last Update: 2020-12-20