[1]刘晓丹,胡 颖,左正康*.图搜索问题算法推导及形式化证明[J].江西师范大学学报(自然科学版),2021,(06):642-651.[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-651.[doi:10.16357/j.cnki.issn1000-5862.2021.06.14]
点击复制

图搜索问题算法推导及形式化证明()
分享到：

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

卷:
期数:
2021年06期
页码:
642-651
栏目:
信息科学与技术
出版日期:
2021-11-25

文章信息/Info

Title:
The Derivation and Formal Proof of Graph Search Algorithm
文章编号:
1000-5862(2021)06-0642-10
作者:
刘晓丹; 胡 颖; 左正康*
江西师范大学计算机信息工程学院,江西 南昌 330022
Author(s):
LIU Xiaodan; HU Ying; ZUO Zhengkang*
College of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China
关键词:
图搜索问题;  循环不变式;  递归定义;  形式化证明
Keywords:
graph search problem;  loop invariant;  recursive definition;  formal proof
分类号:
TP 311
DOI:
10.16357/j.cnki.issn1000-5862.2021.06.14
文献标志码:
A
摘要:
用非形式化方法解决图搜索问题规模受限,对于一些复杂问题难以保证其正确性.传统的形式化方法推导图搜索问题难以理解且不易于形式化证明,现有形式化方法对这类问题的解决方案较少,在保证可靠性和正确性方面有欠缺.该文通过对图搜索问题的深入研究,开发出一种针对解决图搜索算法的新方法.首先刻画问题的规约,利用循环不变式的递归定义技术给出了开发图搜索问题循环不变式的新策略,在此基础上得到Apla抽象算法程序,并对该算法程序进行了形式化证明,再将已验证的Apla算法程序自动生成C++可执行程序,实现了从抽象的形式规约推演出具体的面向计算机的程序代码的程序精化完整过程.以拓扑排序和广度优先遍历为例对所提方法进行实验,实验结果验证了所提方法的有效性,不仅可以推导和证明已知算法,而且对未知算法的推导也有指导性作用.
Abstract:
The scale of graph search problem solved by non-formal method is limited,and it is difficult to guarantee the correctness of some complex problems.The traditional formal methods for deriving graph search are difficult to understand and prove formally.There are few solutions to this kind of problems in existing formal methods,and they are lack of reliability and correctness.The new method is developed to solve the graph search algorithm by studying the graph search problem deeply.Firstly,the specification of the problem is described,and a new strategy for developing loop invariants of graph search problems is given by using the recursive definition technique of loop invariants.On this basis,the Apla abstract algorithm program is obtained,and the algorithm program is formally proved,and the verified algorithm program described by Apla is automatically generated as C++ executable program.The complete process of program refinement from abstract form to specific computer-oriented program code is realized.Taking topological sorting and breadth-first traversal as examples,the proposed method is introduced and proved to be effective by experiment.It can not only deduce and prove known algorithms,but also guide the derivation of unknown algorithms.

参考文献/References:

[1] Koohestani B.A graph representation for search-based approaches to graph layout problems[J].International Journal of Computational Science and Engineering,2020(3):429-436.
[2] Adrian K,Alfredo N,Cristina M,et al.Synchronous black hole search in directed graphs[J].Theoretical Computer Science,2011,412(41):5752-5759.
[3] Zhu Wei,Liu Runjie,Shen Jinyuan,et al.Formal development of non-recursive algorithm for L-system based Koch curve[EB/OL].[2020-12-11].https://dl.acm.org/doi/10.1109/IWCTFTA.2012.67.
[4] Gries D.The science of programming[M].New York:Springer,1989.
[5] Edsger W D.A discipline of programming[M].Upper Saddle River:Prentice Hall,Inc,1976.
[6] Xue Jinyun.A unified approach for developing efficient algorithmic programs[J].Journal of Computer Science and Technology,1997,12(4):314-320.
[7] 朱振元,朱承.递归算法的非递归化实现[J].小型微型计算机系统,2003,24(3):567-570.
[8] 邓觐超,佟玉凤.有关完全图的算法及实现技术[J].烟台大学学报:自然科学与工程版,1997(3):16-20.
[9] 薛锦云.复杂算法程序的规范证明和形式推导[J].江西师范大学学报:自然科学版,1992,16(3):195-202.
[10] Hu Qimin,Xue Jinyun,You Zhen.Research on formal development of non-recursive algorithms of graph search[EB/OL].[2020-12-19].https://link.springer.com/chapter/10.1007%2F978-3-319-31220-0_12.
[11] Deuerlein J,Elhay S,Simpson A R.Fast graph matrix partitioning algorithm for solving the water distribution system equations[J].Journal of Water Resources Planning and Management,2015,142(1):1-11.
[12] 古天龙.软件开发的形式化方法[M].北京:高等教育出版社,2005.
[13] 王戟,詹乃军,冯新宇,等.形式化方法概貌[J].软件学报,2019,30(1):33-61.
[14] CCF形式化方法专业委员会.形式化方法的研究进展与趋势[M].北京:机械工业出版社,2018:1-68.
[15] Xue Jinyun.PAR:a model driven engineering platform for generating algorithms and software[C]//Symposium Programming:Logics,Models,Algorithms and Concurrency to recognize Jayadev Misra's Accomplishments,2016:29-30.
[16] 胡启敏,薛锦云,游珍,等.Apla→C++自动生成系统中若干软件构件形式化验证技术研究[J].计算机工程与科学,2018,40(2):268-274.
[17] Klaus T F,Roger W.Lower and upper competitive bounds for online directed graph exploration[J].Theoretical Computer Science,2015,655:15-29.
[18] Hans L B,Michael R F,Dimitrios M T.Derivation of algorithms for cutwidth and related graph layout parameters[J].Journal of Computer and System Sciences,2008,75(4):231-244.
[19] 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.
[20] Sutton A,Maletic J I.Emulating C++0xconcepts[J].Science of Computer Programming,2013,78(9):1449-1469.
[21] Zheng Yujun,Xue Jinyun.A problem reduction based approach to discrete optimization algorithm design[J].Computing,2010,88(1/2):31-54.
[22] 杨庆红.递归问题循环不变式开发新策略的研究与应用[D].南昌:江西师范大学,2003.
[23] Xue Jinyun.Two new strategies for developing loop invariants and their applications[J].Journal of Computer Science and Technology,1993,8(3):147-154.
[24] 万松松,薛锦云,谢武平.循环不变式开发技术研究[J].计算机工程与科学,2010,32(9):84-88,94.
[25] Kondratyev D A,Maryasov I V,Nepomniaschy V A.The automation of C program verification by the symbolic method of loop invariant elimination[J].Automatic Control and Computer Sciences,2019,53(7):653-662.
[26] Zuo Zhengkang,Wang Changjing,Shi Haihe,et al.Research on a new abstract programming language for generic constraints[EB/OL].[2020-12-20].https://kns.cnki.net/KCMS/detail/detail.aspx?dbcode=IPFD&filename=LRCM201507003080.
[27] Zuo Zhengkang,Xue Jinyun,Wang Changjing.Constraint verification of generic algorithmic program for solving general network path problems[J].Journal of Networks,2013,8(5):1050-1057.
[28] Wang Hongbing,Liang Yanrui,Yao Lin,et al.Computational thinking in C++ programming language[EB/OL].[2021-02-13].https://kns.cnki.net/KCMS/detail/detail.aspx?dbcode=IPFD&filename=ZNXX201412016017.
[29] 左正康,薛锦云.Apla中泛型约束机制研究[J].软件学报,2015,26(6):1340-1355.
[30] Xue Jinyun,You Zhen,Hu Qimin.PAR:a practicable formal method and its supporting platform[EB/OL].[2021-02-15].https://doi.org/10.1007/978-3-030-02450-5_5.
[31] Hu Qimin,Xue Jinyun,You Zhen.Research on formal development of non-recursive algorithms of graph search[EB/OL].[2021-02-15].https://link.springer.com/chapter/10.1007%2F978-3-319-31220-0_12.
[32] 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.

相似文献/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].江西师范大学学报(自然科学版),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,(06):625.[doi:10.16357/j.cnki.issn1000-5862.2020.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:
收稿日期:2021-04-17
基金项目:国家自然科学基金(61862033,61762049,61902162),江西省教育厅科学技术研究(GJJ210307),江西省教育厅研究生创新基金(YC2021-S306)和江西省自然科学基金(20202BABL202026,20202BABL202025,20202BAB202015)资助项目.
通信作者:左正康(1980—),男,江西抚州人,教授,博士,主要从事泛型程序设计和可信软件的研究.E-mail:kerrykaren@126.com
更新日期/Last Update: 2021-11-25