### 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.

Change history: [2022-08-16]: Added formalisations of B+-Trees

### License

BSD 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

- Computer science/Data management systems
- Computer science/Data structures

### 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

### Depends on

- The Imperative Refinement Framework

### Auto-related entries

- Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL
- Flow Networks and the Min-Cut-Max-Flow Theorem
- Formalizing Push-Relabel Algorithms
- Formalizing the Edmonds-Karp Algorithm
- Pop-Refinement

## Cite

×

BTree-AFP

    @article{BTree-AFP,
      author  = {Niels Mündler},
      title   = {A Verified Imperative Implementation of B-Trees},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/BTree.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 26, 2021 : Isabelle2021