### Abstract

The van Emde Boas tree or van Emde Boas priority queue is a data structure supporting membership test, insertion, predecessor and successor search, minimum and maximum determination and deletion in O(log log U) time, where U = 0,...,2n-1 is the overall range to be considered.

The presented formalization follows Chapter 20 of the popular Introduction to Algorithms (3rd ed.) by Cormen, Leiserson, Rivest and Stein (CLRS), extending the list of formally verified CLRS algorithms. Our current formalization is based on the first author's bachelor's thesis.

First, we prove correct a functional implementation, w.r.t. an abstract data type for sets. Apart from functional correctness, we show a resource bound, and runtime bounds w.r.t. manually defined timing functions for the operations.

Next, we refine the operations to Imperative HOL with time, and show correctness and complexity. This yields a practically more efficient implementation, and eliminates the manually defined timing functions from the trusted base of the proof.

### License

BSD License

### Topics

- Computer science/Data structures

### Session Van_Emde_Boas_Trees

- Heap_Time_Monad
- Array_Time
- Ref_Time
- Imperative_HOL_Time
- Syntax_Match
- Assertions
- Hoare_Triple
- Refine_Imp_Hol
- Automation
- Sep_Main
- Imperative_HOL_Add
- Time_Reasoning
- Simple_TBOUND_Cond
- VEBT_Example_Setup
- VEBT_Definitions
- VEBT_Member
- VEBT_Insert
- VEBT_InsertCorrectness
- VEBT_MinMax
- VEBT_Succ
- VEBT_Pred
- VEBT_Delete
- VEBT_DeleteCorrectness
- VEBT_Uniqueness
- VEBT_Height
- VEBT_Bounds
- VEBT_DeleteBounds
- VEBT_Space
- VEBT_Intf_Functional
- VEBT_List_Assn
- VEBT_BuildupMemImp
- VEBT_SuccPredImperative
- VEBT_DelImperative
- VEBT_Intf_Imperative
- VEBT_Example

### Depends on

- Automatic Data Refinement
- Deriving class instances for datatypes

### Auto-related entries

- The string search algorithm by Knuth, Morris and Pratt
- Homogeneous Linear Diophantine Equations
- Imperative Insertion Sort
- Dijkstra’s Shortest Path Algorithm

## Cite

×

Van_Emde_Boas_Trees-AFP

    @article{Van_Emde_Boas_Trees-AFP,
      author  = {Thomas Ammer and Peter Lammich},
      title   = {van Emde Boas Trees},
      journal = {Archive of Formal Proofs},
      month   = {November},
      year    = {2021},
      note    = {\url{https://isa-afp.org/entries/Van_Emde_Boas_Trees.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
- Nov 26, 2021 : Isabelle2021