Verifying Balanced Trees
Zohar Manna,
Henny B. Sipma,
Ting Zhang
Abstract
Balanced search trees provide guaranteed worst-case time performance
and hence they form a very important class of data structures.
However, the self-balancing ability comes at a price; balanced trees
are more complex than their unbalanced counterparts both in terms of
data structure themselves and related manipulation operations. In
this paper we present a framework to model balanced trees in decidable
first-order theories of term algebras with Presburger arithmetic. In
this framework, a theory of term algebras (i.e., a theory of finite
trees) is extended with Presburger arithmetic and with certain
connecting functions that map terms (trees) to integers. Our
framework is flexible in the sense that we can obtain a variety of
decidable theories by tuning the connecting functions. By adding
maximal path and minimal path functions, we obtain a
theory of red-black trees in which the transition relation of tree
self-balancing (rotation) operations is expressible. We then show
how to reduce the verification problem of the red-black tree algorithm
to constraint satisfiability problems in the extended theory.
