图广度优先遍历算法的形式化推导与机械验证方法  

The Formal Derivation and Mechanical Verification Methods for Graph Breadth-First Traversal Algorithms

作　　者：余楚凌 曹中雄 王唱唱 王昌晶[1,3] YU Chuling;CAO Zhongxiong;WANG Changchang;WANG Changjing(School of Computer and Information Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China;College of Digital Industry,Jiangxi Normal University,Shangrao Jiangxi 334000,China;Research Centre of Management Science and Engineering,Jiangxi Normal University,Nanchang Jiangxi 330022,China)

机构地区：[1]江西师范大学计算机信息工程学院,江西南昌330022 [2]江西师范大学数字产业学院,江西上饶334000 [3]江西师范大学管理科学与工程研究中心,江西南昌330022

出　　处：《江西师范大学学报(自然科学版)》2024年第5期472-478,共7页Journal of Jiangxi Normal University(Natural Science Edition)

基　　金：江西省教育厅科学技术研究重点课题(GJJ220302,GJJ210307,GJJ2200303,GJJ220304)资助项目.

摘　　要：针对图广度优先遍历问题,该文提出了一种形式化推导与机械验证方法.首先,描述求解问题的形式化规约,使用分划递推得到统一的循环不变式并开发相应的Apla抽象程序;然后,在Isabelle中描述算法相关的数据类型、定义与基本函数,根据算法程序正确性证明的验证条件证明了抽象算法正确性;最后,通过Apla→C++自动生成器生成可执行代码,验证了该方法的有效性.For graph breadth-first traversal problems,a formal derivation and mechanical verification method is proposed.Firstly,a formal specification of the solution problem is provided,followed by partition recursion to produce a uniform loop invariant and the development of the Apla abstract program.Then,in Isabelle,the data types,definitions and fundamental functions associated with the algorithms are given,and the abstract algorithms are proven to be right in accordance with the verification requirements for the proof of correctness of the algorithmic programs.Finally,the Apla→C++ auto-generator generates executable code,which proves the effectiveness of the proposed method.

关 键 词：图广度优先遍历 形式化推导 定理证明 循环不变式 

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