Theory Dijkstra_Impl
section ‹Implementation of Dijkstra's-Algorithm using the ICF›
theory Dijkstra_Impl
imports
Dijkstra
GraphSpec
HashGraphImpl
"HOL-Library.Code_Target_Numeral"
begin
text‹
In this second refinement step, we use interfaces from the
Isabelle Collection Framework (ICF) to implement the priority queue and
the result map. Moreover, we use a graph interface (that is not contained
in the ICF, but in this development) to represent the graph.
The data types of the first refinement step were designed to fit the
abstract data types of the used ICF-interfaces, which makes this refinement
quite straightforward.
Finally, we instantiate the ICF-interfaces by concrete implementations,
obtaining an executable algorithm, for that we generate code using
Isabelle/HOL's code generator.
›
locale dijkstraC =
g: StdGraph g_ops +
mr: StdMap mr_ops +
qw: StdUprio qw_ops
for g_ops :: "('V,'W::weight,'G,'moreg) graph_ops_scheme"
and mr_ops :: "('V, (('V,'W) path × 'W), 'mr,'more_mr) map_ops_scheme"
and qw_ops :: "('V ,'W infty,'qw,'more_qw) uprio_ops_scheme"
begin
definition "αsc == map_prod qw.α mr.α"
definition "dinvarC_add == λ(wl,res). qw.invar wl ∧ mr.invar res"
definition cdinit :: "'G ⇒ 'V ⇒ ('qw×'mr) nres" where
"cdinit g v0 ≡ do {
wl ← FOREACH (nodes (g.α g))
(λv wl. RETURN (qw.insert wl v Weight.Infty)) (qw.empty ());
RETURN (qw.insert wl v0 (Num 0),mr.sng v0 ([],0))
}"
definition cpop_min :: "('qw×'mr) ⇒ ('V×'W infty×('qw×'mr)) nres" where
"cpop_min σ ≡ do {
let (wl,res) = σ;
let (v,w,wl')=qw.pop wl;
RETURN (v,w,(wl',res))
}"
definition cupdate :: "'G ⇒ 'V ⇒ 'W infty ⇒ ('qw×'mr) ⇒ ('qw×'mr) nres"
where
"cupdate g v wv σ = do {
ASSERT (dinvarC_add σ);
let (wl,res)=σ;
let pv=mpath' (mr.lookup v res);
FOREACH (succ (g.α g) v) (λ(w',v') (wl,res).
if (wv + Num w' < mpath_weight' (mr.lookup v' res)) then do {
RETURN (qw.insert wl v' (wv+Num w'),
mr.update v' ((v,w',v')#the pv,val wv + w') res)
} else RETURN (wl,res)
) (wl,res)
}"
definition cdijkstra where
"cdijkstra g v0 ≡ do {
σ0 ← cdinit g v0;
(_,res) ← WHILE⇩T (λ(wl,_). ¬ qw.isEmpty wl)
(λσ. do { (v,wv,σ') ← cpop_min σ; cupdate g v wv σ' } )
σ0;
RETURN res
}"
end
locale dijkstraC_fixg = dijkstraC g_ops mr_ops qw_ops +
Dijkstra ga v0
for g_ops :: "('V,'W::weight,'G,'moreg) graph_ops_scheme"
and mr_ops :: "('V, (('V,'W) path × 'W), 'mr,'more_mr) map_ops_scheme"
and qw_ops :: "('V ,'W infty,'qw,'more_qw) uprio_ops_scheme"
and ga :: "('V,'W) graph"
and v0 :: 'V +
fixes g :: 'G
assumes g_rel: "(g,ga)∈br g.α g.invar"
begin
schematic_goal cdinit_refines:
notes [refine] = inj_on_id
shows "cdinit g v0 ≤⇓?R mdinit"
using g_rel
unfolding cdinit_def mdinit_def
apply (refine_rcg)
apply (refine_dref_type)
apply (simp_all add: αsc_def dinvarC_add_def refine_rel_defs
qw.correct mr.correct refine_hsimp)
done
schematic_goal cpop_min_refines:
"(σ,σ') ∈ build_rel αsc dinvarC_add
⟹ cpop_min σ ≤ ⇓?R (mpop_min σ')"
unfolding cpop_min_def mpop_min_def
apply (refine_rcg)
apply (refine_dref_type)
apply (simp add: αsc_def dinvarC_add_def refine_hsimp refine_rel_defs)
apply (simp add: αsc_def dinvarC_add_def refine_hsimp refine_rel_defs)
done
schematic_goal cupdate_refines:
notes [refine] = inj_on_id
shows "(σ,σ')∈build_rel αsc dinvarC_add ⟹ v=v' ⟹ wv=wv' ⟹
cupdate g v wv σ ≤ ⇓?R (mupdate v' wv' σ')"
unfolding cupdate_def mupdate_def
using g_rel
apply (refine_rcg)
apply (refine_dref_type)
apply (simp_all add: αsc_def dinvarC_add_def refine_rel_defs
qw.correct mr.correct refine_hsimp)
done
lemma cdijkstra_refines:
"cdijkstra g v0 ≤ ⇓(build_rel mr.α mr.invar) mdijkstra"
proof -
note [refine] = cdinit_refines cpop_min_refines cupdate_refines
show ?thesis
unfolding cdijkstra_def mdijkstra_def
using g_rel
apply (refine_rcg)
apply (auto
split: prod.split prod.split_asm
simp add: qw.correct mr.correct dinvarC_add_def αsc_def refine_hsimp
refine_rel_defs)
done
qed
end
context dijkstraC
begin
thm g.nodes_it_is_iterator
schematic_goal idijkstra_refines_aux:
assumes "g.invar g"
shows "RETURN ?f ≤ cdijkstra g v0"
using assms
unfolding cdijkstra_def cdinit_def cpop_min_def cupdate_def
apply (refine_transfer)
done
concrete_definition idijkstra for g ?v0.0 uses idijkstra_refines_aux
lemma idijkstra_refines:
assumes "g.invar g"
shows "RETURN (idijkstra g v0) ≤ cdijkstra g v0"
using assms
by (rule idijkstra.refine)
end
text ‹
The following theorem states correctness of the algorithm independent
from the refinement framework.
Intuitively, the first goal states that the abstraction of the returned
result is correct, the second goal states that the result
datastructure satisfies its invariant, and the third goal states
that the cached weights in the returned result are correct.
Note that this is the main theorem for a user of Dijkstra's algorithm in some
bigger context. It may also be specialized for concrete instances of the
implementation, as exemplarily done below.
›
theorem (in dijkstraC_fixg) idijkstra_correct:
shows
"weighted_graph.is_shortest_path_map ga v0 (αr (mr.α (idijkstra g v0)))"
(is ?G1)
and "mr.invar (idijkstra g v0)" (is ?G2)
and "Dijkstra.res_invarm (mr.α (idijkstra g v0))" (is ?G3)
proof -
from g_rel have I: "g.invar g" by (simp add: refine_rel_defs)
note idijkstra_refines[OF I]
also note cdijkstra_refines
also note mdijkstra_refines
finally have Z: "RETURN (idijkstra g v0) ≤
⇓(build_rel (αr ∘ mr.α) (λm. mr.invar m ∧ res_invarm (mr.α m)))
dijkstra'"
apply (subst (asm) conc_fun_chain)
apply (simp only: br_chain)
done
also note dijkstra'_refines[simplified]
also note dijkstra_correct
finally show ?G1 ?G2 ?G3
by (auto elim: RETURN_ref_SPECD simp: refine_rel_defs)
qed
theorem (in dijkstraC) idijkstra_correct:
assumes INV: "g.invar g"
assumes V0: "v0 ∈ nodes (g.α g)"
assumes nonneg_weights: "⋀v w v'. (v,w,v')∈edges (g.α g) ⟹ 0≤w"
shows
"weighted_graph.is_shortest_path_map (g.α g) v0
(Dijkstra.αr (mr.α (idijkstra g v0)))" (is ?G1)
and "Dijkstra.res_invarm (mr.α (idijkstra g v0))" (is ?G2)
proof -
interpret gv: valid_graph "g.α g" using g.valid INV .
interpret dcg: dijkstraC_fixg g_ops mr_ops qw_ops "g.α g" v0 g
apply (rule dijkstraC_fixg.intro)
apply unfold_locales
apply (simp_all add: hlg.finite INV V0 hlg_ops_def
nonneg_weights refine_rel_defs)
done
from dcg.idijkstra_correct show ?G1 ?G2 by simp_all
qed
text ‹
Example instantiation with HashSet.based graph,
red-black-tree based result map, and finger-tree based priority queue.
›
setup Locale_Code.open_block
interpretation hrf: dijkstraC hlg_ops rm_ops aluprioi_ops
by unfold_locales
setup Locale_Code.close_block
definition "hrf_dijkstra ≡ hrf.idijkstra"
lemmas hrf_dijkstra_correct = hrf.idijkstra_correct[folded hrf_dijkstra_def]
export_code hrf_dijkstra checking SML
export_code hrf_dijkstra in OCaml
export_code hrf_dijkstra in Haskell
export_code hrf_dijkstra checking Scala
definition hrfn_dijkstra :: "(nat,nat) hlg ⇒ _"
where "hrfn_dijkstra ≡ hrf_dijkstra"
export_code hrfn_dijkstra in SML
lemmas hrfn_dijkstra_correct =
hrf_dijkstra_correct[where ?'a = nat and ?'b = nat, folded hrfn_dijkstra_def]
term hrfn_dijkstra
term hlg.from_list
definition "test_hrfn_dijkstra
≡ rm.to_list
(hrfn_dijkstra (hlg.from_list ([0..<4],[(0,3,1),(0,4,2),(2,1,3),(1,4,3)])) 0)"
ML_val ‹
@{code test_hrfn_dijkstra}
›
end