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
*)
header "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,LL10,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,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
(*>*)