Resumen:

An Exercise in Proving Red-Black Trees Correct

Red-black trees are an efficient data structure that constitutes the basis for implementing maps, multimaps, sets and multisets, in the standard libraries of many programming languages. It achieves logarithmic costs for searching, inserting, and deleting keys, but keeping them balanced frequently requires to deal with a high number of cases. However, a variant called "Left-Leaning", due to Robert Sedgewick, reduces the number of cases to a few ones. We present here a functional version of these red-black trees and prove them correct with respect to a model-based specification, being the model of a red-black tree a set of elements. We have used the Dafny verification platform, which provides the programming language, the assertion language, and the verifier. The latter is an up-to-date SMT solver (Satisfiability Modulo Theories), which can deal with a rather large decidable fragment of the first-order logic.