[1]左正康,方 越,黄志鹏,等.二叉树队列关系问题非递归算法的推导及形式化证明[J].江西师范大学学报(自然科学版),2022,(01):49-58.[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,(01):49-58.[doi:10.16357/j.cnki.issn1000-5862.2022.01.07]
点击复制

二叉树队列关系问题非递归算法的推导及形式化证明()
分享到：

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

卷:
期数:
2022年01期
页码:
49-58
栏目:
高可信与智能软件
出版日期:
2022-01-25

文章信息/Info

Title:
The Derivation and Formal Proof of Non-Recursive Algorithm for Binary Tree Queue Relation Problems
文章编号:
1000-5862(2022)01-0049-10
作者:
左正康; 方 越; 黄志鹏; 黄 箐; 王昌晶*
江西师范大学计算机信息工程学院,江西 南昌 330022
Author(s):
ZUO Zhengkang; FANG Yue; HUANG Zhipeng; HUANG Qing; WANG Changjing*
College of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China
关键词:
二叉树队列递推关系;  循环不变式;  Dijkstra-Gries标准程序证明法;  Apla到C++程序自动生成系统;  非线性数据结构
Keywords:
binary tree queue recursion relation;  loop invariant; Dijkstra-Gries standard proving technique;  Apla to C++ program automatic generation system;  nonlinear data structure
分类号:
TP 311
DOI:
10.16357/j.cnki.issn1000-5862.2022.01.07
文献标志码:
A
摘要:
该文对二叉树类问题进行分划,寻找其递推关系,并针对具有队列递推关系的一类问题,给出了其推导过程和形式化证明策略.再结合每个算法后置断言的不同,提出3种开发循环不变式的策略,并构造出该类问题的通用循环不变式模板.同时,发现该类问题是基于2个母算法的功能加以实现的,由此派生出3类问题.首先,对这3类派生问题进行推导,得到递推关系表达式和循环不变式,由此导出非递归Apla算法; 然后,使用Dijkstra-Gries标准程序证明方法证明这些算法的正确性; 最后,通过Apla到C++程序自动生成系统自动生成C++代码,实现了从抽象规约到具体的可执行程序的完整求精过程.
Abstract:
The binary tree problems are partitioned to find recursion relations in this paper.A strategy of derivation and formal proof is presented for a class of problems with queue recurrence relation.Combined with the difference of postassertion of each algorithm,three strategies for developing cycle invariant are proposed,and a general cycle invariant template for this kind of problem is constructed.At the same time,it is found that this kind of problem is implemented based on the functions of the two parent algorithms,from which three kinds of problems are derived.Firstly,the representation of the three types of derived problems is deduced,and the recursive relation expressions and loop invariant are obtained,thus the non-recursive Apla algorithm is derived.Then,the correctness of the algorithm is proved by Dijkstra-Gries standard proving technique.In the end,Apla to C++ program automatic generation system automatically generates C++ code.The complete refinement process from abstract specification to concrete executable program is realized.

参考文献/References:

[1] 朱振元,朱承.递归算法的非递归化实现 [J].小型微型计算机系统,2003,24(3):567-570.
[2] 谢武平,薛锦云.Radl算法到Apla程序的生成系统 [J].计算机研究与发展,2014,51(4):856-864.
[3] XUE Jinyun.A unified approach for developing efficient algorithmic programs [J].Journal of Computer Science and Technology,1997,12(4):314-329.
[4] YOU Zhen,XUE Jinyun,ZUO Zhengkang.Unified formal derivation and automatic verification of three binary-tree traversal non-recursive algorithms [J].Cluster Computing,2016,19(4):2145-2156.
[5] GRIES D.The science of programming [M].New York:Springer,1981.
[6] DIJKSTRA E W.A discipline of programming [M].New Jersey:Prentice Hall,1976.
[7] 赖勇.Apla到C++自动程序转换系统的研制 [D].南昌:江西师范大学,2002.
[8] 左正康,刘志豪,黄箐,等.Apla与程序设计语言泛型特性比较研究 [J].江西师范大学学报(自然科学版),2019,43(5):454-461.
[9] 李贤贞,吴茂念,杨静.循环结构的形式化推导 [J].微型机与应用,2014,33(5):82-83,86.
[10] BARNARD D T.Introducing formal methods via program derivation [J].Computing Reviews,2016,57(2):123.
[11] KOURIE D G,WATSON B W.The correctness-by-construction approach to programming [M].Berlin:Springer,2012.
[12] CHAUDHARI D L,DAMANI O.Combining top-down and bottom-up techniques in program derivation [EB/OL].[2021-03-17].https://www.doc88.com/p-7778967344901.html?r=1.
[13] SANKARANARAYANAN S,SIPMA H B,MANNA Z.Non-linear loop invariant generation using Gröbner bases [J].ACM SIGPLAN Notices,2004,39(1):318-329.
[14] COLÓN M A,SANKARANARAYANAN S,SIPMA H B.Linear invariant generation using non-linear constraint solving [M]∥HUNT W A,SOMENZI F.Computer-aided verification:lecture notes in computer science.Berlin:Springer,2003:420-432.
[15] COUST P,COUST R.Abstract interpretation:a unified lattice model for static analysis of programs by construction or approximation of fixpoints [C]∥GRAHAM R M,HARRISON M A.Proceedings of the 4th ACM SIGACT-SIGPLAN symposium on Principles of Programming Languages.New York:ACM Press,1977:238-252.
[16] 毕忠勤,曾振柄,郭远华.非线性循环不变式的自动生成 [J].计算机应用,2008,28(7):1854-1857.
[17] FURIA C A,MEYER B.Inferring loop invariants using postconditions [M]∥BLASS A,DERSHOWITZ N,REISIG W.Fields of logic and computation:lecture notes in computer science.Berlin:Springer,2010:277-300.
[18] JUNG Y,KONG S,WANG B Y,et al.Deriving invariants by algorithmic learning,decision procedures,and predicate abstraction [M]∥BARTHE G,HERMENEGILDO M.Verification,model checking and abstract interpretation:lecture notes in computer science.Berlin:Springer,2010,5944:180-196.
[19] 陈石坤,李舟军.基于QBF的循环不变式构造技术 [J].计算机工程与科学,2010,32(9):76-80.
[20] XUE Jinyun,GRIES D.Developing a linear algorithm for cubing a cyclic permutation [J].Science of Computer Programming,1988,11(2):161-165.
[21] XUE Jinyun,ZHENG Yujun,HU Qimin,et al.PAR:a practicable formal method and its supporting platform [M]∥SUN Jing,SUN Meng.Formal methods and software engineering:lecture notes in computer science.Cham:Springer,2018:70-86.
[22] 左正康,游珍,薛锦云.后序遍历二叉树非递归算法的推导及形式化证明 [J].计算机工程与科学,2010,32(3):119-123.
[23] ZUO Zhengkang,FANG Yue,HUANG Qing,et al.Non-recursive algorithm derivation and formal proof of binary tree traversal class problems [EB/OL].[2021-04-13].https://ieeexplore.ieee.org/document/9282723.

相似文献/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,(01):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,(01):378.[doi:10.16357/j.cnki.issn1000-5862.2020.04.09]
[3]左正康,方 越,黄 箐,等.二叉树排序非递归算法推导及形式化证明[J].江西师范大学学报(自然科学版),2020,(06):625.[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,(01):625.[doi:10.16357/j.cnki.issn1000-5862.2020.06.14]
[4]刘晓丹,胡 颖,左正康*.图搜索问题算法推导及形式化证明[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,(01):642.[doi:10.16357/j.cnki.issn1000-5862.2021.06.14]

备注/Memo

备注/Memo:
收稿日期:2021-09-12
基金项目:国家自然科学基金(61862033,61902162),江西省教育厅科技重点课题(GJJ210307)和江西省自然科学基金(20202BAB202015)资助项目.
作者简介:左正康(1980—),男,江西抚州人,教授,博士,主要从事可信软件和泛型程序设计的研究.E-mail:kerrykaren@126.com
通信作者:王昌晶(1977—),男,江西南昌人,教授,博士,博士生导师,主要从事软件形式化方法的研究.E-mail:wcj771006@163.com
更新日期/Last Update: 2022-01-25