Commit 7445e476 authored by Niels Mündler's avatar Niels Mündler
Browse files

Add imperative deletion operation and OCaml code export to BTree entry

parent 1edcb594d89c
......@@ -10349,7 +10349,7 @@ abstract =
In this work, we use the interactive theorem prover Isabelle/HOL to
verify an imperative implementation of the classical B-tree data
structure invented by Bayer and McCreight [ACM 1970]. The
implementation supports set membership and insertion queries with
implementation supports set membership, insertion and deletion queries with
efficient binary search for intra-node navigation. This is
accomplished by first specifying the structure abstractly in the
functional modeling language HOL and proving functional correctness.
......@@ -10358,12 +10358,18 @@ abstract =
separation logic utilities from the <a
href="https://www.isa-afp.org/entries/Refine_Imperative_HOL.html">
Isabelle Refinement Framework </a> . The code can be exported to
the programming languages SML and Scala. We examine the runtime of all
the programming languages SML, OCaml and Scala. We examine the runtime of all
operations indirectly by reproducing results of the logarithmic
relationship between height and the number of nodes. The results are
discussed in greater detail in the corresponding <a
href="https://mediatum.ub.tum.de/1596550">Bachelor's
Thesis</a>.
extra-history =
Change history:
[2021-05-02]:
Add implementation and proof of correctness of imperative deletion operations.
Further add the option to export code to OCaml.
<br>
 
[Sunflowers]
title = The Sunflower Lemma of Erdős and Rado
......
......@@ -2,6 +2,26 @@ theory Array_SBlit
imports "Separation_Logic_Imperative_HOL.Array_Blit"
begin
(* Resolves TODO by Peter Lammich *)
(* OCaml handles the case of len=0 correctly (i.e.
as specified by the Hoare Triple in Array_Blit
not generating an exception if si+len \<le> array length and such) *)
code_printing code_module "array_blit" \<rightharpoonup> (OCaml)
\<open>
let array_blit src si dst di len = (
if src=dst then
raise (Invalid_argument "array_blit: Same arrays")
else
Array.blit src (Z.to_int si) dst (Z.to_int di) (Z.to_int len)
)
\<close>
code_printing constant blit' \<rightharpoonup>
(OCaml) "(fun () -> /array'_blit _ _ _ _ _)"
export_code blit checking OCaml
section "Same array Blit"
text "The standard framework already provides a function to copy array
......@@ -117,7 +137,6 @@ next
have[simp]: "take len (drop si (lsrc[di + len := lsrc ! (si + len)]))
= take len (drop si lsrc)"
sledgehammer
by (metis Suc.prems(2) ab_semigroup_add_class.add.commute add_le_cancel_right take_drop take_update_cancel)
have [simp]: "drop (di + len) (lsrc[di + len := lsrc ! (si + len)])
= lsrc ! (si+len) # drop (Suc di + len) lsrc"
......@@ -173,8 +192,10 @@ thm safe_sblit_rule
subsection "Code Generator Setup"
text "Note that the requirement for correctness
is even weaker here than in SML.
We therefore manually handle the case where length is 0 (in which case nothing happens at all)."
is even weaker here than in SML/OCaml.
In particular, if the length of the slice to copy is equal to 0,
we will never throw an exception.
We therefore manually handle this case, where nothing happens at all."
code_printing code_module "array_sblit" \<rightharpoonup> (SML)
\<open>
......@@ -188,6 +209,15 @@ code_printing code_module "array_sblit" \<rightharpoonup> (SML)
)
\<close>
code_printing code_module "array_sblit" \<rightharpoonup> (OCaml)
\<open>
let array_sblit src si di len = (
if len > Z.zero then
(Array.blit src (Z.to_int si) src (Z.to_int di) (Z.to_int len))
else ()
)
\<close>
definition safe_sblit' where
[code del]: "safe_sblit' src si di len
= safe_sblit src (nat_of_integer si) (nat_of_integer di)
......@@ -198,7 +228,7 @@ lemma [code]:
= safe_sblit' src (integer_of_nat si) (integer_of_nat di)
(integer_of_nat len)" by (simp add: safe_sblit'_def)
(* TODO: Export to other languages: OCaml, Haskell *)
(* TODO: Export to other languages: Haskell *)
code_printing constant safe_sblit' \<rightharpoonup>
(SML) "(fn/ ()/ => /array'_sblit _ _ _ _)"
and (Scala) "{ ('_: Unit)/=>/
......@@ -211,7 +241,13 @@ code_printing constant safe_sblit' \<rightharpoonup>
safescopy(_.array,_.toInt,_.toInt,_.toInt)
}"
export_code safe_sblit checking SML Scala
code_printing constant safe_sblit' \<rightharpoonup>
(OCaml) "(fun () -> /array'_sblit _ _ _ _)"
export_code safe_sblit checking SML Scala OCaml
subsection "Derived operations"
......
This diff is collapsed.
......@@ -403,17 +403,22 @@ global_interpretation btree_imp_binary_split: imp_split_smeq bin_split
defines btree_isin = btree_imp_binary_split.isin
and btree_ins = btree_imp_binary_split.ins
and btree_insert = btree_imp_binary_split.insert
and btree_del = btree_imp_binary_split.del
and btree_split_max = btree_imp_binary_split.split_max
and btree_delete = btree_imp_binary_split.delete
and btree_empty = btree_imp_binary_split.empty
apply unfold_locales
apply(sep_auto heap: bin_split_rule)
done
thm btree_imp_binary_split.ins.simps
declare btree_imp_binary_split.ins.simps[code] btree_imp_binary_split.isin.simps[code]
declare btree_imp_binary_split.ins.simps[code]
declare btree_imp_binary_split.isin.simps[code]
declare btree_imp_binary_split.del.simps[code] btree_imp_binary_split.split_max.simps[code]
export_code btree_empty btree_isin btree_insert checking SML Scala
export_code btree_empty btree_isin btree_insert in SML module_name BTreeInsert
export_code btree_empty btree_isin btree_insert in Scala module_name BTreeInsert
export_code btree_empty btree_isin btree_insert btree_delete checking OCaml SML Scala
export_code btree_empty btree_isin btree_insert btree_delete in OCaml module_name BTree
export_code btree_empty btree_isin btree_insert btree_delete in SML module_name BTree
export_code btree_empty btree_isin btree_insert btree_delete in Scala module_name BTree
end
theory BTree_Map
imports BTree_Set "HOL-Data_Structures.Map_Specs"
begin
term "(1,2)"
term int
fun eq_kv where
"eq_kv (k1, v1) (k2,v2) = (k1 = k2)"
datatype ('a, 'b) ukv = KV 'a 'b
quotient_type ('a,'b) kv = "('a, 'b) prod" / eq_kv
apply(rule equivpI)
apply (auto simp add: reflp_def symp_def transp_def)
done
type_notation (ASCII)
kv (infixr "\<mapsto>" 20)
instantiation kv :: (linorder, type) linorder
begin
fun less_eq_ukv::"'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
where "less_eq_ukv (k1, v1) (k2, v2) = (k1 \<le> k2)"
lift_definition less_eq_kv :: "'a \<mapsto> 'b \<Rightarrow> 'a \<mapsto> 'b \<Rightarrow> bool" is less_eq_ukv
by auto
definition less_kv:: "'a \<mapsto> 'b \<Rightarrow> 'a \<mapsto> 'b \<Rightarrow> bool"
where "less_kv a b = (a \<le> b \<and> \<not>b \<le> a)"
instance
proof(standard, goal_cases)
case (1 x y)
then show ?case by (simp add: less_kv_def)
next
case (2 x)
then show ?case
by (transfer; clarsimp)
next
case (3 x y z)
then show ?case
by (transfer; auto)
next
case (4 x y)
then show ?case
by (transfer; auto)
next
case (5 x y)
then show ?case
by (transfer; auto)
qed
end
locale split_default = abs_split: BTree_Set.split split
for split::
"(('a \<mapsto> 'b) btree \<times> ('a::{linorder} \<mapsto> 'b::{default})) list \<Rightarrow> ('a \<mapsto> 'b)
\<Rightarrow> (('a \<mapsto> 'b) btree \<times> ('a \<mapsto> 'b)) list \<times> (('a \<mapsto> 'b) btree \<times> ('a \<mapsto> 'b)) list"
begin
lift_definition lift :: "'a \<Rightarrow> ('a \<mapsto> 'b)" is
"\<lambda>a. (a, default)" .
lift_definition val :: "('a \<mapsto> 'b) \<Rightarrow> 'b" is
"\<lambda>(a,b). b"
apply auto
sorry
fun find where
"find (Leaf) y = None" |
"find (Node ts t) y = (
case split ts y of (_,(sub,sep)#rs) \<Rightarrow> (
if y = sep then
Some sep
else
find sub y
)
| (_,[]) \<Rightarrow> find t y
)"
fun lookup :: "('a \<mapsto> 'b option) btree \<Rightarrow> 'a \<Rightarrow> 'a option"
where "lookup t x = (case find t (x,None) of Some (a,b) \<Rightarrow> Some b | None \<Rightarrow> None)"
interpretation btree_map: Map_by_Ordered
empty_btree
end
end
\ No newline at end of file
......@@ -106,6 +106,11 @@ fun node\<^sub>i:: "nat \<Rightarrow> ('a btree \<times> 'a) list \<Rightarrow>
)
)"
lemma nodei_ti_simp: "node\<^sub>i k ts t = T\<^sub>i x \<Longrightarrow> x = Node ts t"
apply (cases "length ts \<le> 2*k")
apply (auto split!: list.splits)
done
fun ins:: "nat \<Rightarrow> 'a \<Rightarrow> 'a btree \<Rightarrow> 'a up\<^sub>i" where
"ins k x Leaf = (Up\<^sub>i Leaf x Leaf)" |
......@@ -140,7 +145,7 @@ fun insert::"nat \<Rightarrow> 'a \<Rightarrow> 'a btree \<Rightarrow> 'a btree"
subsection "Deletion"
text "The following deletion method is inspired by Bayer (70) and Fielding (??).
text "The following deletion method is inspired by Bauer (70) and Fielding (??).
Rather than stealing only a single node from the neighbour,
the neighbour is fully merged with the potentially underflowing node.
If the resulting node is still larger than allowed, the merged node is split
......
......@@ -146,10 +146,10 @@ definition pfa_shrink :: "nat \<Rightarrow> 'a::heap pfarray \<Rightarrow> 'a pf
lemma pfa_shrink_rule[sep_heap_rules]: "
k \<le> length l \<Longrightarrow>
< is_pfa c l (a,n) >
k \<le> length xs \<Longrightarrow>
< is_pfa c xs (a,n) >
pfa_shrink k (a,n)
<\<lambda>(a',n'). is_pfa c (take k l) (a',n') * \<up>(n' = k \<and> a'=a) >"
<\<lambda>(a',n'). is_pfa c (take k xs) (a',n') * \<up>(n' = k \<and> a'=a) >"
by (sep_auto
simp: pfa_shrink_def is_pfa_def min.absorb1
split: prod.splits nat.split)
......@@ -354,7 +354,7 @@ definition pfa_insert_grow :: "'a::{heap,default} pfarray \<Rightarrow> nat \<R
return a''
}"
lemma pfa_insert_grow_rule:
lemma pfa_insert_grow_rule[sep_heap_rules]:
"i \<le> n \<Longrightarrow>
<is_pfa c l (a,n)>
pfa_insert_grow (a,n) i x
......@@ -369,7 +369,7 @@ definition pfa_extend where
return (a,n+m)
}"
lemma pfa_extend_rule:
lemma pfa_extend_rule[sep_heap_rules]:
"n+m \<le> c \<Longrightarrow>
<is_pfa c l1 (a,n) * is_pfa d l2 (b,m)>
pfa_extend (a,n) (b,m)
......@@ -385,7 +385,7 @@ definition pfa_extend_grow where
return (a',n+m)
}"
lemma pfa_extend_grow_rule:
lemma pfa_extend_grow_rule[sep_heap_rules]:
"<is_pfa c l1 (a,n) * is_pfa d l2 (b,m)>
pfa_extend_grow (a,n) (b,m)
<\<lambda>(a',n'). is_pfa (max c (n+m)) (l1@l2) (a',n') * \<up>(n'=n+m \<and> c \<ge> n) * is_pfa d l2 (b,m)>\<^sub>t"
......@@ -400,7 +400,7 @@ definition pfa_append_extend_grow where
return (a'',n+m+1)
}"
lemma pfa_append_extend_grow_rule:
lemma pfa_append_extend_grow_rule[sep_heap_rules]:
"<is_pfa c l1 (a,n) * is_pfa d l2 (b,m)>
pfa_append_extend_grow (a,n) x (b,m)
<\<lambda>(a',n'). is_pfa (max c (n+m+1)) (l1@x#l2) (a',n') * \<up>(n'=n+m+1 \<and> c \<ge> n) * is_pfa d l2 (b,m)>\<^sub>t"
......
......@@ -27,11 +27,11 @@ All above mentioned files contain definitions as well as proofs of functional co
## Usage
These theories have been tested with [Isabelle2020](https://isabelle.in.tum.de/website-Isabelle2020/index.html), although it should be compatible to newer versions of the tool.
These theories have been tested with [Isabelle2021](https://isabelle.in.tum.de/website-Isabelle2021/index.html).
The files `BTree*.thy` that do not contain `Imp` only need a regular Isabelle2020 setup.
The files `BTree*.thy` that do not contain `Imp` only need a regular Isabelle setup.
The rest of the theories build upon [Refine_Imperative_HOL](https://www.isa-afp.org/entries/Refine_Imperative_HOL.html), you will need to succesfully set up that project first as described in the [rArchive of Formal Proofs](https://www.isa-afp.org/using.html).
The rest of the theories build upon [Refine_Imperative_HOL](https://www.isa-afp.org/entries/Refine_Imperative_HOL.html), you will need to succesfully set up that project first as described in the [Archive of Formal Proofs](https://www.isa-afp.org/using.html).
The script `start_isabelle.sh` uses and if not available compiles a session
containing the content of the Refinement Framework which significantly enhances
working with the files provided in this project.
chapter AFP
session "BTree" (AFP) = Refine_Imperative_HOL +
options [timeout = 600]
session "BTree" (AFP) = "Refine_Imperative_HOL" +
options [timeout = 600, document = pdf]
sessions
"HOL-Data_Structures"
theories
......
\documentclass[11pt,a4paper]{article}
\usepackage[T1]{fontenc}
\usepackage{isabelle,isabellesym}
\usepackage[T1]{fontenc}
\usepackage{mathtools}
\usepackage{amssymb}
\usepackage{stmaryrd}
......@@ -26,7 +26,7 @@
\begin{abstract}
In this work, we use the interactive theorem prover Isabelle/HOL
to verify an imperative implementation of the classical B-tree data structure \cite{DBLP:journals/acta/BayerM72}.
The implementation supports set membership and insertion queries
The implementation supports set membership, insertion and deletion queries
with efficient binary search for intra-node navigation.
This is accomplished by first specifying the structure abstractly
in the functional modeling language HOL and proving functional correctness.
......@@ -35,7 +35,7 @@ in Imperative/HOL.
We show the validity of this refinement using
the separation logic utilities from the
Isabelle Refinement Framework \cite{Refine_Imperative_HOL-AFP}.
The code can be exported to the programming languages SML and Scala.
The code can be exported to the programming languages SML, Scala and OCaml.
We examine the runtime of all operations indirectly by reproducing results
of the logarithmic relationship between height and the number of nodes.
The results are discussed in greater detail in the related Bachelor's Thesis
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment