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
(*>*)