|
van
Emde
Boas
Trees
Title: |
van Emde Boas Trees |
Authors:
|
Thomas Ammer and
Peter Lammich
|
Submission date: |
2021-11-23 |
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. |
BibTeX: |
@article{Van_Emde_Boas_Trees-AFP,
author = {Thomas Ammer and Peter Lammich},
title = {van Emde Boas Trees},
journal = {Archive of Formal Proofs},
month = nov,
year = 2021,
note = {\url{https://isa-afp.org/entries/Van_Emde_Boas_Trees.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Automatic_Refinement, Deriving |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|