图搜索问题算法推导及形式化证明  

The Derivation and Formal Proof of Graph Search Algorithm

作　　者：刘晓丹 胡颖 左正康[1] LIU Xiaodan;HU Ying;ZUO Zhengkang(College of Computer Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China)

机构地区：[1]江西师范大学计算机信息工程学院,江西南昌330022

出　　处：《江西师范大学学报（自然科学版）》2021年第6期642-651,共10页Journal of Jiangxi Normal University(Natural Science Edition)

基　　金：国家自然科学基金(61862033,61762049,61902162);江西省教育厅科学技术研究(GJJ210307);江西省教育厅研究生创新基金(YC2021-S306);江西省自然科学基金(20202BABL202026,20202BABL202025,20202BAB202015)资助项目.

摘　　要：用非形式化方法解决图搜索问题规模受限,对于一些复杂问题难以保证其正确性.传统的形式化方法推导图搜索问题难以理解且不易于形式化证明,现有形式化方法对这类问题的解决方案较少,在保证可靠性和正确性方面有欠缺.该文通过对图搜索问题的深入研究,开发出一种针对解决图搜索算法的新方法.首先刻画问题的规约,利用循环不变式的递归定义技术给出了开发图搜索问题循环不变式的新策略,在此基础上得到Apla抽象算法程序,并对该算法程序进行了形式化证明,再将已验证的Apla算法程序自动生成C++可执行程序,实现了从抽象的形式规约推演出具体的面向计算机的程序代码的程序精化完整过程.以拓扑排序和广度优先遍历为例对所提方法进行实验,实验结果验证了所提方法的有效性,不仅可以推导和证明已知算法,而且对未知算法的推导也有指导性作用.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.

关 键 词：图搜索问题 循环不变式 递归定义 形式化证明 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]