Dijkstra's Shortest Path Algorithm (Q7361202)
From MaRDI portal
!
This is the item page for this Wikibase entity, intended for internal use and editing purposes. Please use the normal view instead:
AFP entry Dijkstra_Shortest_Path
| Language | Label | Description | Also known as |
|---|---|---|---|
| default for all languages | No label defined |
||
| English | Dijkstra's Shortest Path Algorithm |
AFP entry Dijkstra_Shortest_Path |
Statements
30 January 2012
0 references
Benedikt Nordhoff
0 references
Peter Lammich
0 references
Dijkstra's Shortest Path Algorithm (English)
0 references
We implement and prove correct Dijkstra's algorithm for the single source shortest path problem, conceived in 1956 by E. Dijkstra. The algorithm is implemented using the data refinement framework for monadic, nondeterministic programs. An efficient implementation is derived using data structures from the Isabelle Collection Framework.
0 references
0 references
