Up to index of Isabelle/HOL/Collections/Refine_Monadic
theory Bfs_Implheader {*\isaheader{Verified BFS Implementation in ML}*}
theory Bfs_Impl
imports
Breadth_First_Search
"../Collection_Bindings" "../Refine"
"~~/src/HOL/Library/Code_Target_Numeral"
begin
text {*
Originally, this was part of our submission to the
VSTTE 2010 Verification Competition. Some slight changes have been applied
since the submitted version.
*}
text {*
In the @{text "Breadth_First_Search"}-theory, we verified an abstract
version of the algorithm. This abstract version tried to reflect the
given pseudocode specification as precisely as possible.
However, it was not executable, as it was nondeterministic. Hence,
we now refine our algorithm to an executable specification, and use
Isabelle/HOLs code generator to generate ML-code.
The implementation uses the Isabelle Collection Framework (ICF)
(Available at \url{http://afp.sourceforge.net/entries/Collections.shtml}),
to provide efficient set implementations. We choose a hashset
(backed by a Red Black Tree) for the visited set, and lists for
all other sets. Moreover, we fix the node type to natural numbers.
*}
text {*
The following algorithm is a straightforward rewriting of the
original algorithm. We only exchanged the abstract set operations by
concrete operations on the data structures provided by the ICF.
The operations of the list-set implementation are named
@{text "ls_xxx"}, the ones of the hashset are named @{text "hs_xxx"}.
*}
definition bfs_impl :: "(nat => nat ls) => nat => nat => (nat option nres)"
where "bfs_impl succ src dst ≡ do {
(f,_,_,_,d) \<leftarrow> WHILE
(λ(f,V,C,N,d). f=False ∧ ¬ ls_isEmpty C)
(λ(f,V,C,N,d). do {
v \<leftarrow> RETURN (the (ls_sel' C (λ_. True))); let C = ls_delete v C;
if v=dst then RETURN (True,hs_empty (),ls_empty (),ls_empty (),d)
else do {
(V,N) \<leftarrow> FOREACH (ls_α (succ v)) (λw (V,N).
if (¬ hs_memb w V) then
RETURN (hs_ins w V, ls_ins_dj w N)
else RETURN (V,N)
) (V,N);
if (ls_isEmpty C) then do {
let C=N;
let N=ls_empty ();
let d=d+1;
RETURN (f,V,C,N,d)
} else RETURN (f,V,C,N,d)
}
})
(False,hs_sng src,ls_sng src, ls_empty (),0::nat);
if f then RETURN (Some d) else RETURN None
}"
text {* Auxilliary lemma to initialize the refinement prover. *}
(*lemma [refine]: "(ls_α o succ) v = ls_α (succ v)"
by auto*)
(* TODO/FIXME:
There is too much redundancy in the xx_correct - lemmas.
They do not include the automtically instantiated generic algorithms,
and they are independent of adding new operations to the interface or to
the rb-interface
*)
text {*
It is quite easy to show that the implementation respects the
specification, as most work is done by the refinement framework. *}
theorem bfs_impl_correct:
shows "bfs_impl succ src dst ≤ Graph.bfs_spec (ls_αosucc) src dst"
proof -
txt {* As list-sets are always finite, our setting satisfies the
finitely-branching assumption made about graphs *}
interpret Graph "ls_αosucc"
by unfold_locales simp
txt {* The refinement framework can prove automatically that
the implementation refines the abstract algorithm.
The notation @{text "S ≤ \<Down>R S'"} means, that the program @{text "S"}
refines the program @{text "S'"} w.r.t.\ the refinement relation
(also called coupling invariant occasionally) @{text "R"}.
In our case, the refinement relation is the identity, as
the result type was not refined.
*}
have "bfs_impl succ src dst ≤ \<Down>Id (Graph.bfs (ls_αosucc) src dst)"
unfolding bfs_impl_def bfs_def
apply (refine_rcg)
apply (refine_dref_type)
apply (rule inj_on_id | simp add: refine_hsimp
hs_correct hs.sng_correct ls_correct ls.sng_correct
split: prod.split prod.split_asm) +
done
txt {* The result then follows due to transitivity of refinement. *}
also have "… ≤ bfs_spec src dst"
by (simp add: bfs_correct)
finally show ?thesis .
qed
text {* The last step is to actually generate executable ML-code.
*}
text {*
We first use the partial-correctness code generator of our framework
to automatically turn the algorithm described in our framework into
a function that is independent from our framework. This step also
removes the last nondeterminism, that has remained in the iteration order
of the inner loop.
The result of the function is an option type, returning @{text "None"}
for nontermination. Inside this option-type, there is the option type
that encodes whether we return with failure or a distance.
*}
schematic_lemma bfs_code_refine_aux:
"nres_of ?bfs_code ≤ bfs_impl succ src dst"
unfolding bfs_impl_def
apply (refine_transfer)
done
thm bfs_code_refine_aux[no_vars]
text {* Currently, our (prototype) framework cannot yet generate the
definition itself. The following definition was copy-pasted from the
output of the above @{text "thm"} command: *}
definition
bfs_code :: "(nat => nat ls) => nat => nat => nat option dres" where
"bfs_code succ src dst ≡
(dWHILE (λ(f, V, C, N, d). f = False ∧ ¬ ls_isEmpty C)
(λ(a, b).
case b of
(aa, ab, ac, bc) =>
dRETURN (the (ls_sel' ab (λ_. True))) »=
(λxa. let xb = ls_delete xa ab
in if xa = dst
then dRETURN
(True, hs_empty (), ls_empty (), ls_empty (), bc)
else IT_tag ls_iteratei (succ xa)
(dres_case True True (λ_. True))
(λx s. s »=
(λ(ad, bd).
if ¬ hs_memb x ad
then dRETURN
(hs_ins x ad, ls_ins_dj x bd)
else dRETURN (ad, bd)))
(dRETURN (aa, ac)) »=
(λ(ad, bd).
if ls_isEmpty xb
then let xd = bd; xe = ls_empty (); xf = bc + 1
in dRETURN (a, ad, xd, xe, xf)
else dRETURN (a, ad, xb, bd, bc))))
(False, hs_sng src, ls_sng src, ls_empty (), 0) »=
(λ(a, b).
case b of
(aa, ab, ac, bc) => if a then dRETURN (Some bc) else dRETURN None))
"
text {* Finally, we get the desired lemma by folding the schematic
lemma with the definition: *}
lemma bfs_code_refine:
"nres_of (bfs_code succ src dst) ≤ bfs_impl succ src dst"
using bfs_code_refine_aux[folded bfs_code_def] .
text {*
As a last step, we make the correctness property independent of our
refinement framework. This step drastically decreases the trusted code
base, as it completely eliminates the specifications made in the
refinement framework from the trusted code base.
The following theorem solves both verification tasks, without depending
on any concepts of the refinement framework, except the deterministic result
monad.
*}
theorem bfs_code_correct:
"bfs_code succ src dst = dRETURN None
==> ¬(Graph.conn (ls_α o succ) src dst)"
"bfs_code succ src dst = dRETURN (Some d)
==> Graph.conn (ls_α o succ) src dst
∧ Graph.min_dist (ls_α o succ) src dst = d"
"bfs_code succ src dst ≠ dFAIL"
proof -
interpret Graph "ls_αosucc"
by unfold_locales simp
from order_trans[OF bfs_code_refine bfs_impl_correct, of succ src dst]
show "bfs_code succ src dst = dRETURN None
==> ¬(Graph.conn (ls_α o succ) src dst)"
"bfs_code succ src dst = dRETURN (Some d)
==> Graph.conn (ls_α o succ) src dst
∧ Graph.min_dist (ls_α o succ) src dst = d"
"bfs_code succ src dst ≠ dFAIL"
apply (unfold bfs_spec_def)
apply (auto split: option.split_asm)
done
qed
text {* Now we can use the code-generator of Isabelle/HOL to generate
code into various target languages: *}
export_code bfs_code in SML file -
export_code bfs_code in OCaml file -
export_code bfs_code in Haskell file -
export_code bfs_code in Scala file -
text {* The generated code is most conveniently executed within
Isabelle/HOL itself. We use a small test graph here: *}
definition nat_list:: "nat list => nat dlist"
where
"nat_list ≡ dlist_of_list"
definition succ :: "nat => nat dlist"
where
"succ n = nat_list (if n = 1 then [2, 3]
else if n = 2 then [4]
else if n = 4 then [5]
else if n = 5 then [2]
else if n = 3 then [6]
else [])"
definition bfs_code_succ :: "integer => integer => nat option dres"
where
"bfs_code_succ m n = bfs_code succ (nat_of_integer m) (nat_of_integer n)"
ML_val {*
(* Execute algorithm for some node pairs. *)
@{code bfs_code_succ} 1 1;
@{code bfs_code_succ} 1 2;
@{code bfs_code_succ} 1 5;
@{code bfs_code_succ} 1 7;
*}
end