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, insertion, deletion, iteration and range 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.
Using manual refinement, we derive an imperative implementation in
Imperative/HOL. We show the validity of this refinement using the
separation logic utilities from the
Isabelle Refinement Framework . The code can be exported to
the programming languages SML, OCaml and Scala.
This entry contains two developments:
- B-Trees
- This formalisation is discussed in greater detail in the corresponding Bachelor's Thesis.
- B+-Trees:
- This formalisation also supports range queries and is discussed in a paper published at ICTAC 2022.
License
History
- May 2, 2021
- Add implementation and proof of correctness of imperative deletion operations.
Further add the option to export code to OCaml.
Topics
Session BTree
- BTree
- BTree_Height
- BTree_Set
- BTree_Split
- BPlusTree
- BPlusTree_Split
- BPlusTree_Set
- BPlusTree_Range
- BPlusTree_SplitCE
- Array_SBlit
- Partially_Filled_Array
- Basic_Assn
- BTree_Imp
- BTree_ImpSet
- Imperative_Loops
- BTree_ImpSplit
- Flatten_Iter_Spec
- Flatten_Iter
- Inst_Ex_Assn
- BPlusTree_Imp
- BPlusTree_ImpSplit
- BPlusTree_ImpSet
- Partially_Filled_Array_Iter
- BPlusTree_Iter_OneWay
- Subst_Mod_Mult_AC
- BPlusTree_Iter
- BPlusTree_ImpRange
- BPlusTree_ImpSplitCE