Red-black Tree

March 8, 2011 – 6 years, 1 month 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

  1. 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
  2. Implement remove() so it really removes a node from the tree ([2], Section 13.4).20 points.
  3. 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