@MISC{GRAPHSP.MIZ,
  AUTHOR = {Chen, Jing-Chao},
  TITLE = {Dijkstra's Shortest Path Algorithm},
  SECTION1 = {Preliminaries},
  SECTION2 = {The Fundamental Properties of Directed Paths and Shortest Paths},
  SECTION3 = {The Basic Theorems for Dijkstra's Shortest Path Algorithm (continue)},
  SECTION4 = {The Definition of Assignment Statement},
  SECTION5 = {The Definition of Pascal--Like ``while'' - ``do" Statement},
  SECTION6 = {Defining a Weight Function for an Oriented Graph},
  SECTION7 = {Basic Operations for Dijkstra's Shortest Path Algorithm},
  SECTION8 = {Data Structure for Dijkstra's Shortest Path Algorithm},
  SECTION9 = {The Definition of Dijkstra's Shortest Path Algorithm},
  SECTION10 = {Justifying the Correctness of Dijkstra's Shortest Path Algorithm},
  DAY = {17},
  MONTH = {March},
  YEAR = {2003},
  ADDRESS1 = {Donghua University\\Shanghai},
  SUMMARY = {  The article formalizes Dijkstra's shortest path algorithm
  \cite{Dijkstra59}.
  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.}}

