| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Dijkstra's Shortest Path Algorithm
| Title: | Dijkstra's Shortest Path Algorithm |
| Authors: | Benedikt Nordhoff (b_nord01 /at/ uni-muenster /dot/ de) and Peter Lammich |
| Submission date: | 2012-01-30 |
| Abstract: | 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. |
| BibTeX: |
@article{Dijkstra_Shortest_Path-AFP,
author = {Benedikt Nordhoff and Peter Lammich},
title = {Dijkstra's Shortest Path Algorithm},
journal = {Archive of Formal Proofs},
month = jan,
year = 2012,
note = {\url{http://isa-afp.org/entries/Dijkstra_Shortest_Path.shtml},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Collections |
| Used by: | Formal_SSA, Koenigsberg_Friendship, Refine_Imperative_HOL |
| Status: [skipped] | This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations. |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
Older releases:
|