# Theory Introduction

(*  Title: A efficiently computable formalisation of Dijkstra's algorithm
Author: Benedikt Nordhoff <bnord01 at gmail.com>,
Peter Lammich <lammich at in.tum.de>
Maintainer: lammich@in.tum.de
*)
section "Introduction and Overview"

(*<*)
theory Introduction
imports Main
begin
(*>*)

text_raw ‹\label{thy:Introduction}›
text ‹

Dijkstra's algorithm \<^cite>‹"Dijk59"› is an algorithm used to
find shortest paths from one given vertex to all other vertices in a
non-negatively weighted graph.

The implementation of the algorithm is meant to be an application
of our extensions to the Isabelle Collections Framework (ICF)
\<^cite>‹"L09_collections" and "LL10" and "NKP10"›. Moreover, it serves as a test case
for our data refinement framework \<^cite>‹"refinement_framework"›.
We use ICF-Maps to efficiently represent the graph and
result and the newly introduced unique priority queues for the work
list.

For a documentation of the refinement framework see \<^cite>‹"refinement_framework"›,
that also contains a userguide and some simpler examples.

The development utilizes a stepwise refinement approach. Starting from an
abstract algorithm that has a nice correctness proof, we stepwise refine
the algorithm until we end up with an efficient implementation, for that
we generate code using Isabelle/HOL's code generator\<^cite>‹"Haft09" and "HaNi10"›.

\paragraph{Structure of the Submission.}
The abstract version of the algorithm with the correctness proof, as well
as the main refinement steps are contained in the theory \texttt{Dijkstra}.
The refinement steps involving the ICF and code generation are contained in
\texttt{Dijkstra-Impl}.
The theory \texttt{Infty} contains an extension of numbers with an infinity
element.
The theory \texttt{Graph} contains a formalization of graphs, paths, and
related concepts.
The theories \texttt{GraphSpec,GraphGA,GraphByMap,HashGraphImpl} contain an
ICF-style specification of graphs.
The theory \texttt{Test} contains a small performance test on random graphs.
It uses the ML-code generated by the code generator.
›

(*<*)
end
(*>*)