Dijkstra's Shortest Path Algorithm

Jing-Chao Chen

Donghua University, Shanghai

Summary.

The article formalizes Dijkstra's shortest path algorithm [11]. A path from a source vertex $v$ to $a$ target vertex $u$ is said to be the shortest path if its total cost is minimum among all $v$-to-$u$ paths. Dijkstra's algorithm is based on the following assumptions: \begin{itemize} \item All edge costs are non-negative. \item The number of vertices is finite. \item The source is a single vertex, but the target may be all other vertices. \end{itemize} The underlying principle of the algorithm may be described as follows: the algorithm starts with the source; it visits the vertices in order of increasing cost, and maintains a set $V$ of visited vertices (denoted by UsedVx in the article) whose cost from the source has been computed, and a tentative cost $D(u)$ to each unvisited vertex $u.$ In the article, the set of all unvisited vertices is denoted by UnusedVx. $D(u)$ is the cost of the shortest path from the source to u in the subgraph induced by $V \cup \{u\}.$ We denote the set of all unvisited vertices whose $D$-values are not infinite (i.e. in the subgraph each of which has a path from the source to itself) by OuterVx. Dijkstra's algorithm repeatedly searches OuterVx for the vertex with minimum tentative cost (this procedure is called findmin in the article), adds it to the set $V$ and modifies $D$-values by a procedure, called Relax. Suppose the unvisited vertex with minimum tentative cost is $x$, the procedure Relax replaces $D(u)$ with min$\{D(u),D(u)+cost(x,u)\}$ where $u$ is a vertex in UnusedVx, and cost$(x,u)$ is the cost of edge $(x,u).$ In the Mizar library, there are several computer models, e.g. SCMFSA and SCMPDS etc. However, it is extremely difficult to use these models to formalize the algorithm. Instead, we adopt functions in the Mizar library, which seem to be pseudo-codes, and are similar to those in the functional programming language, e.g. Lisp. To date, there is no rigorous justification with respect to the correctness of Dijkstra's algorithm. The article presents first the rigorous justification.

MML Identifier: GRAPHSP

Contents (PDF format)

1. Preliminaries
2. The Fundamental Properties of Directed Paths and Shortest Paths
3. The Basic Theorems for Dijkstra's Shortest Path Algorithm (continue)
4. The Definition of Assignment Statement
5. The Definition of Pascal--Like ``while'' - ``do" Statement
6. Defining a Weight Function for an Oriented Graph
7. Basic Operations for Dijkstra's Shortest Path Algorithm
8. Data Structure for Dijkstra's Shortest Path Algorithm
9. The Definition of Dijkstra's Shortest Path Algorithm
10. Justifying the Correctness of Dijkstra's Shortest Path Algorithm

Bibliography

[1] Grzegorz Bancerek. Cardinal numbers. Journal of Formalized Mathematics, 1, 1989.

[2] Grzegorz Bancerek. The fundamental properties of natural numbers. Journal of Formalized Mathematics, 1, 1989.

[3] Grzegorz Bancerek and Krzysztof Hryniewiecki. Segments of natural numbers and finite sequences. Journal of Formalized Mathematics, 1, 1989.

[4] Grzegorz Bancerek and Andrzej Trybulec. Miscellaneous facts about functions. Journal of Formalized Mathematics, 8, 1996.

[5] Czeslaw Bylinski. Functions and their basic properties. Journal of Formalized Mathematics, 1, 1989.

[6] Czeslaw Bylinski. Functions from a set to a set. Journal of Formalized Mathematics, 1, 1989.

[7] Czeslaw Bylinski. Partial functions. Journal of Formalized Mathematics, 1, 1989.

[8] Czeslaw Bylinski. Finite sequences and tuples of elements of a non-empty sets. Journal of Formalized Mathematics, 2, 1990.

[9] Czeslaw Bylinski. The sum and product of finite sequences of real numbers. Journal of Formalized Mathematics, 2, 1990.

[10] Agata Darmochwal. Finite sets. Journal of Formalized Mathematics, 1, 1989.

[11] E. W. Dijkstra. A note on two problems in connection with graphs. \em Numer. Math., 1:269--271, 1959.

[12] Krzysztof Hryniewiecki. Basic properties of real numbers. Journal of Formalized Mathematics, 1, 1989.

[13] Krzysztof Hryniewiecki. Graphs. Journal of Formalized Mathematics, 2, 1990.

[14] Jaroslaw Kotowicz and Yatsuka Nakamura. Introduction to Go-Board --- part I. Journal of Formalized Mathematics, 4, 1992.

[15] Yatsuka Nakamura and Piotr Rudnicki. Oriented chains. Journal of Formalized Mathematics, 10, 1998.

[16] Takaya Nishiyama and Yasuho Mizuhara. Binary arithmetics. Journal of Formalized Mathematics, 5, 1993.

[17] Andrzej Trybulec. Domains and their Cartesian products. Journal of Formalized Mathematics, 1, 1989.

[18] Andrzej Trybulec. Tarski Grothendieck set theory. Journal of Formalized Mathematics, Axiomatics, 1989.

[19] Andrzej Trybulec. Subsets of real numbers. Journal of Formalized Mathematics, Addenda, 2003.

[20] Michal J. Trybulec. Integers. Journal of Formalized Mathematics, 2, 1990.

[21] Wojciech A. Trybulec. Pigeon hole principle. Journal of Formalized Mathematics, 2, 1990.

[22] Zinaida Trybulec. Properties of subsets. Journal of Formalized Mathematics, 1, 1989.

[23] Edmund Woronowicz. Relations and their basic properties. Journal of Formalized Mathematics, 1, 1989.