Email Gateway (Nov 26 2021 at 09:50): Email Gateway (Nov 26 2021 at 09:50):From: Tobias Nipkow <nipkow@in.tum.de>
van Emde Boas Trees
Thomas Ammer and Peter Lammich
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.
https://www.isa-afp.org/entries/Van_Emde_Boas_Trees.html
Enjoy!
smime.p7s
Last updated: Apr 19 2024 at 12:27 UTC