## Red-black Tree

*March 8, 2011 – 6 years ago, by sarahgrebing*

### Short Description

The task is to implement and verify a red-black tree providing a dictionary interface, like the one below in the code Section.

### Code

class RedBlackTree { static RedBlackTree create(int defaultValue); void replace(int key, int value); void remove(int key); int lookup(int key); } void redBlackTestHarness() { RedBlackTree a = create(0), b = create(1); a.replace(1, 1); b.replace(1, 10); a.replace(2, 2); b.replace(2, 20); assert(a.lookup(1) == 1 && a.lookup(42) == 0); assert(b.lookup(1) == 10 && b.lookup(42) == 1); a.remove(1); b.remove(2); assert(a.lookup(1) == 0 && a.lookup(42) == 0); assert(b.lookup(2) == 1 && b.lookup(42) == 1); }

### Specification

### Long Description

A red-black tree [2] is a commonly used kind of binary search tree where each node,

in addition to the usual data and pointers, carries a bit of information referred to as the

color (traditionally, either red or black). Tree operations maintain approximate balance

by using rotation guided by colors of nodes. The task is to implement and verify a

red-black tree providing a dictionary interface, like the one in the code Section.

The method create(d) creates a new dictionary mapping all keys to d. replace(k, v)

replaces the current value associated with k by v. remove(k) is functionally equivalent

to replace(k, d), where d is the default value provided upon construction, but see the verification tasks below. Finally, lookup(k) returns the current value associated with k.

The following test harness should be verified without looking at the particular implementation

of red-black trees; that is, the interface above should be specified using

appropriate abstraction, e.g., a map or a set of pairs.

Verification Tasks

- Prove the correctness of the test harness and tree implementation against the specifications of the tree (it is allowed to implement remove() by a call to replace()).40 points
- Implement remove() so it really removes a node from the tree ([2], Section 13.4).20 points.
- Prove the red-black balancing invariant, that is, that a red node cannot be a parentof another red node and that every path from a leaf to the root contains the samenumber of black nodes. 20 points.

### Supplementary Materials

The paper from which this benchmark is taken was published in may 2010 by K. Rustan M. Leino and Michal Moskal. It contains some more benchmarks which are also included on this site.

Information about the scoring system and the pseudo-code description of the programs can be found here.

### Submitted by

Sarah Grebing