Navegación

Búsqueda

Búsqueda avanzada

An Exercise in Proving Red-Black Trees Correct (Trabajo en progreso)

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.

A Generic Intermediate Representation for Verification Condition Generation, Work in Progress

As part of a platform for computer-assisted verification, we present an intermediate representation of programs that is both language independent and appropriate for the generation of verification conditions. We show how many imperative and functional languages can be translated to this generic internal representation, and how the generated conditions faithfully reflect the semantics of the original program. At this representation level, loop invariants and preconditions of recursive functions belonging to the original program are represented by assertions placed at certain edges of a directed graph. The paper defines the generic representation, sketches the transformation algorithms, and describes how the places where the invariants should be placed are computed. Assuming that, either manually or assisted by the platform, the invariants have been settled, it is shown how the verification conditions are generated. A running example illustrates the process.