# Theory Introduction

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