Derivation and Formal Proof of Floyd-Warshall Algorithm

Zhengkang Zuo, Xiaodan Liu,Qing Huang,Yunyan Liao,Yuan Wang,Changjing Wang

2021 5th International Conference on Communication and Information Systems (ICCIS)（2021）

引用 1|浏览1

暂无评分

摘要

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 algor...

查看译文

关键词

graph algorithm,Floyd-Warshall algorithm,loop invariant,Apla to C++ automatic generation system,recursive definition technique

AI 理解论文

溯源树

样例

生成溯源树，研究论文发展脉络

Chat Paper

正在生成论文摘要