Email Gateway (Aug 22 2022 at 15:27): Email Gateway (Aug 22 2022 at 15:27):From: Tobias Nipkow <nipkow@in.tum.de>
The Floyd-Warshall Algorithm for Shortest Paths
Simon Wimmer and Peter Lammich
The Floyd-Warshall algorithm [Flo62, Roy59, War62] is a classic dynamic
programming algorithm to compute the length of all shortest paths between any
two vertices in a graph (i.e. to solve the all-pairs shortest path problem, or
APSP for short). Given a representation of the graph as a matrix of weights M,
it computes another matrix M' which represents a graph with the same path
lengths and contains the length of the shortest path between any two vertices i
and j. This is only possible if the graph does not contain any negative cycles.
However, in this case the Floyd-Warshall algorithm will detect the situation by
calculating a negative diagonal entry. This entry includes a formalization of
the algorithm and of these key properties. The algorithm is refined to an
efficient imperative version using the Imperative Refinement Framework.
https://www.isa-afp.org/entries/Floyd_Warshall.shtml
Enjoy!
smime.p7s
Last updated: Apr 25 2024 at 08:20 UTC