Red-Black Trees in SPARK
This example features a minimalist library of trees providing only membership test and insertion. The complexity of this example lies in the invariants that are maintained on the data-structure. Namely, it implements a balanced binary search tree, balancing being enforced by red black coloring.
The implementation is divided in three layers, each concerned with only a part of the global data structure invariant. The first package, named Binary_Trees, is only concerned with the tree structure, whereas Search_Trees imposes ordering properties and Red_Black_Trees enforces balancing. At each level, the relevant properties are expressed using a Type Invariant. It allows to show each independent invariant at the boundary of its layer, assuming that it holds when working on upper layers.
The example features several particularities which make it complex beyond purely automated reasoning. First, the tree structure is encoded using references in an array, which makes it difficult to reason about disjointness of different branches of a tree. Then, reasoning about reachability in the tree structure requires induction, which is often out of the reach of automatic solvers. Finally, reasoning about value ordering is also a pain point for automatic solvers, as it requires coming up with intermediate values on which to apply transitivity.
To achieve full functional verification of this example, it resorts to manually helping automatic solvers using auto-active techniques. For example, ghost procedures are used to introduce intermediate lemmas, loop invariants are written to achieve inductive proofs, and assertions are introduced to provide new values to be used for transitivity relations.
This program and the verification activities associated to it are described in Auto-Active Proof of Red-Black Trees in SPARK, presented at NFM 2017.
Authors: Claire Dross
Topics: Ghost code / Data Structures / Trees / Type invariant
Tools: SPARK 2014
References: ProofInUse joint laboratory
See also: Red-black trees
see also the index (by topic, by tool, by reference, by year)
download ZIP archive
The full code is in the ZIP archive above. The proofs can be replayed using SPARK Community 2018 and invoking the test.cmd script from the archive.