Derivation and Formal Proof of Floyd-Warshall Algorithm
Zhengkang Zuo, Xiaodan Liu, Qing Yun Huang, Yunyan Liao, Yuan Wang, Changjing Wang · 2021
Graph algorithms are always complex and difficult to deduce and prove. In this paper, the Floyd-Warshall algorithm is deduced and formally proved. Firstly, the problem specification is described, and the loop invariant is detected and expressed by the recursive definition technology of loop invariant. On this basis, the Apla abstract algorithm program is obtained, and the formal proof of the algorithm program is carried out. Finally, through the Apla to C++ automatic generation system, the validated algorithm program described by Apla is automatically generated into C++ executable program. Based on the technology of developing loop invariant provided in this paper, the validity of derivation and proof of the graph structure problem are guaranteed. The correctness of the program and its development efficiency are improved. The successful experiment of this case shows that this method can not only know what the algorithm is to solve the graph structure problem, but also know how the algorithm is obtained.