### 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.

### License

BSD License

### Topics

- Computer science/Algorithms/Graph

### Session Dijkstra_Shortest_Path

- Introduction
- Dijkstra_Misc
- Graph
- Weight
- Dijkstra
- GraphSpec
- GraphGA
- GraphByMap
- HashGraphImpl
- Dijkstra_Impl
- Dijkstra_Impl_Adet
- Test

### Depends on

- Collections Framework

### Used by

- The Imperative Refinement Framework
- Verified Construction of Static Single Assignment Form
- The Königsberg Bridge Problem and the Friendship Theorem

### Auto-related entries

- van Emde Boas Trees
- Homogeneous Linear Diophantine Equations
- Automatic Data Refinement
- Generating linear orders for datatypes

## Cite

×

Dijkstra_Shortest_Path-AFP

    @article{Dijkstra_Shortest_Path-AFP,
      author  = {Benedikt Nordhoff and Peter Lammich},
      title   = {Dijkstra's Shortest Path Algorithm},
      journal = {Archive of Formal Proofs},
      month   = {January},
      year    = {2012},
      note    = {\url{https://isa-afp.org/entries/Dijkstra_Shortest_Path.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Mar 8, 2013 : Isabelle2013
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Mar 15, 2012 : Isabelle2011-1
- Feb 10, 2012 : Isabelle2011-1