Test or verify properties of red-black tree

1
votes

I have based this code on the Wikipedia article about red-black trees and on the part about red-black trees in the CLRS book "Introduction to Algorithms". This program displays the expected results if I run it. Now I would like to verify that it is good. How can one verify the properties and not just simply test it for certain cases? I would like to verify that the code fulfills the specification. I suppose that I could write a test case building up a large red-black tree and then deallocating it but that is still only a test and not a complete verification. 

#include <stdio.h>
#include <assert.h>
#include <stdlib.h>


static char BLACK = 'b';
static char RED = 'r';

struct node {
    int key;
    char color;
    struct node *left, *right, *parent;
};

void insert_repair_tree(struct node* n);
void delete_case1(struct node* n);
void delete_case2(struct node* n);
void delete_case3(struct node* n);
void delete_case4(struct node* n);
void delete_case5(struct node* n);
struct node *LEAF;

struct node *parent(struct node *n) {
    return n->parent; // NULL for root node
}

struct node *grandparent(struct node *n) {
    struct node *p = parent(n);
    if (p == NULL)
        return NULL; // No parent means no grandparent
    return parent(p); // NULL if parent is root
}

struct node *sibling(struct node *n) {
    struct node *p = parent(n);
    if (p == NULL)
        return NULL; // No parent means no sibling
    if (n == p->left)
        return p->right;
    else
        return p->left;
}

struct node *uncle(struct node *n) {
    struct node *p = parent(n);
    struct node *g = grandparent(n);
    if (g == NULL)
        return NULL; // No grandparent means no uncle
    return sibling(p);
}

void rotate_left(struct node *n) {
    struct node *nnew = n->right;
    struct node *p = parent(n);
    assert(nnew != NULL); // since the leaves of a red-black tree are empty, they cannot become internal nodes
    n->right = nnew->left;
    nnew->left = n;
    n->parent = nnew;
    // handle other child/parent pointers
    if (n->right != NULL)
        n->right->parent = n;
    if (p != NULL) // initially n could be the root
    {
        if (n == p->left)
            p->left = nnew;
        else if (n == p->right) // if (...) is excessive
            p->right = nnew;
    }
    nnew->parent = p;
}

void rotate_right(struct node *n) {
    struct node *nnew = n->left;
    struct node *p = parent(n);
    assert(nnew != NULL); // since the leaves of a red-black tree are empty, they cannot become internal nodes
    n->left = nnew->right;
    nnew->right = n;
    n->parent = nnew;
    // handle other child/parent pointers
    if (n->left != NULL)
        n->left->parent = n;
    if (p != NULL) // initially n could be the root
    {
        if (n == p->left)
            p->left = nnew;
        else if (n == p->right) // if (...) is excessive
            p->right = nnew;
    }
    nnew->parent = p;
}

void insert_recurse(struct node* root, struct node* n) {
    // recursively descend the tree until a leaf is found
    if (root != NULL && n->key < root->key) {
        if (root->left != LEAF) {
            insert_recurse(root->left, n);
            return;
        }
        else
            root->left = n;
    } else if (root != NULL) {
        if (root->right != LEAF){
            insert_recurse(root->right, n);
            return;
        }
        else
            root->right = n;
    }

    // insert new node n
    n->parent = root;
    n->left = LEAF;
    n->right = LEAF;
    n->color = RED;
}


void insert_case1(struct node* n)
{
    if (parent(n) == NULL)
        n->color = BLACK;
}

void insert_case2(struct node* n)
{
    return; /* Do nothing since tree is still valid */
}
void insert_case3(struct node* n)
{
    parent(n)->color = BLACK;
    uncle(n)->color = BLACK;
    grandparent(n)->color = RED;
    insert_repair_tree(grandparent(n));
}
void insert_case4step2(struct node* n)
{
    struct node* p = parent(n);
    struct node* g = grandparent(n);

    if (n == p->left)
        rotate_right(g);
    else
        rotate_left(g);
    p->color = BLACK;
    g->color = RED;
}


void insert_case4(struct node* n)
{
    struct node* p = parent(n);
    struct node* g = grandparent(n);

    if (n == g->left->right) {
        rotate_left(p);
        n = n->left;
    } else if (n == g->right->left) {
        rotate_right(p);
        n = n->right;
    }

    insert_case4step2(n);
}



void insert_repair_tree(struct node* n) {
    if (parent(n) == NULL) {
        insert_case1(n);
    } else if (parent(n)->color == BLACK) {
        insert_case2(n);
    } else if (uncle(n)->color == RED) {
        insert_case3(n);
    } else {
        insert_case4(n);
    }
}
struct node *insert(struct node* root, struct node* n) {
    // insert new node into the current tree
    insert_recurse(root, n);

    // repair the tree in case any of the red-black properties have been violated
    insert_repair_tree(n);

    // find the new root to return
    root = n;
    while (parent(root) != NULL)
        root = parent(root);
    return root;
}



void replace_node(struct node* n, struct node* child){
    child->parent = n->parent;
    if (n == n->parent->left)
        n->parent->left = child;
    else
        n->parent->right = child;
}

int is_leaf(struct node* n){
    if(n->right ==NULL && n->left == NULL)
        return 1;
    else return 0;
}

void delete_one_child(struct node* n)
{
    /*
     * Precondition: n has at most one non-leaf child.
     */
    struct node* child = is_leaf(n->right) ? n->left : n->right;

    replace_node(n, child);
    if (n->color == BLACK) {
        if (child->color == RED)
            child->color = BLACK;
        else
            delete_case1(child);
    }
    free(n);
}

void delete_case1(struct node* n)
{
    if (n->parent != NULL)
        delete_case2(n);
}

void delete_case2(struct node* n)
{
    struct node* s = sibling(n);

    if (s->color == RED) {
        n->parent->color = RED;
        s->color = BLACK;
        if (n == n->parent->left)
            rotate_left(n->parent);
        else
            rotate_right(n->parent);
    }
    delete_case3(n);
}

void delete_case3(struct node* n)
{
    struct node* s = sibling(n);

    if ((n->parent->color == BLACK) &&
        (s->color == BLACK) &&
        (s->left->color == BLACK) &&
        (s->right->color == BLACK)) {
        s->color = RED;
        delete_case1(n->parent);
    } else
        delete_case4(n);
}

void delete_case4(struct node* n)
{
    struct node* s = sibling(n);

    if ((n->parent->color == RED) &&
        (s->color == BLACK) &&
        (s->left->color == BLACK) &&
        (s->right->color == BLACK)) {
        s->color = RED;
        n->parent->color = BLACK;
    } else
        delete_case5(n);
}

void delete_case6(struct node* n)
{
    struct node* s = sibling(n);

    s->color = n->parent->color;
    n->parent->color = BLACK;

    if (n == n->parent->left) {
        s->right->color = BLACK;
        rotate_left(n->parent);
    } else {
        s->left->color = BLACK;
        rotate_right(n->parent);
    }
}

void delete_case5(struct node* n)
{
    struct node* s = sibling(n);

    if  (s->color == BLACK) { /* this if statement is trivial,
due to case 2 (even though case 2 changed the sibling to a sibling's child,
the sibling's child can't be red, since no red parent can have a red child). */
/* the following statements just force the red to be on the left of the left of the parent,
   or right of the right, so case six will rotate correctly. */
        if ((n == n->parent->left) &&
            (s->right->color == BLACK) &&
            (s->left->color == RED)) { /* this last test is trivial too due to cases 2-4. */
            s->color = RED;
            s->left->color = BLACK;
            rotate_right(s);
        } else if ((n == n->parent->right) &&
                   (s->left->color == BLACK) &&
                   (s->right->color == RED)) {/* this last test is trivial too due to cases 2-4. */
            s->color = RED;
            s->right->color = BLACK;
            rotate_left(s);
        }
    }
    delete_case6(n);
}

struct node* search(struct node *temp, int val) {
    int diff;
    while (!is_leaf(temp)) {
        diff = val - temp->key;
        if (diff > 0) {
            temp = temp->right;
        } else if (diff < 0) {
            temp = temp->left;
        } else {
            printf("Search Element Found!!\n");
            return temp;
        }
    }
    printf("Given Data Not Found in the tree!!\n");
    return 0;
}
void inorderTree(struct node *root) {
    struct node *temp = root;

    if (temp != NULL) {
        inorderTree(temp->left);

        printf(" %d--%c ", temp->key, temp->color);

        inorderTree(temp->right);

    }
}

void postorderTree(struct node *root) {
    struct node *temp = root;

    if (temp != NULL) {
        postorderTree(temp->left);
        postorderTree(temp->right);
        printf(" %d--%c ", temp->key, temp->color);
    }
}

void traversal(struct node *root) {
    if (root != NULL) {
        printf("root is %d-- %c", root->key, root->color);
        printf("\nInorder tree traversal\n");
        inorderTree(root);
        printf("\npostorder tree traversal\n");
        postorderTree(root);
    }
}
int main() {
    printf("Hello!\n");
    struct node *root = NULL;//malloc(sizeof(struct node));
    LEAF = malloc(sizeof(struct node));
    LEAF->color=BLACK;
    LEAF->left=NULL;
    LEAF->right=NULL;
    LEAF->key=0;
    int choice, val, var, fl = 0;
    while (1) {
        setbuf(stdout, 0); // Bugfix for debugging mode on Windows
        printf("\nEnter your choice :1:Add  2:Delete  3:Find  4:Traverse 5: Test  6:Exit\n");
        scanf("%d", &choice);
        switch (choice) {
            case 1:
                setbuf(stdout, 0);
                printf("Enter the integer you want to add : ");
                scanf("%d", &val);
                struct node *z = malloc(sizeof(struct node));
                z->key = val;
                z->left = NULL;
                z->right = NULL;
                z->parent = NULL;
                z->color = RED;
                root = insert(root, z);
                printf("The root is now %d: ", root->key);

                break;
            case 2:
                printf("Enter the integer you want to delete : ");
                scanf("%d", &var);
                delete_one_child(search(root, var));
                break;
            case 3:
                printf("Enter search element \n");
                scanf("%d", &val);
                search(root, val);
                break;
            case 4: 
                traversal(root);
                break;
            case 5: // TODO
                //test();
                break;
            case 6:
                fl = 1;
                break;
            default:
                printf("\nInvalid Choice\n");
        }
        if (fl == 1) { break; }
    }
    return 0;
}
2
cred-black-treeformal-verification
I've looked at the wikipedia explanation and I think this one: eternallyconfuzzled.com/tuts/datastructures/jsw_tut_rbtree.aspx is much better. If you navigate around there, it actually has public domain working source code. Some RB trees do "top down" and jsw's does "bottom up" [or vice versa], so a good alternative to look at. Also, checks for null pointers [vs. using a sentinel node]. – Craig Estey
Well, you're basically asking "How can I be certain that my code is absolutely correct?" – eesiraed

2 Answers

3
votes

There is verification, and there is proof. Perhaps by "complete verification" you mean formal proof of code correctness. However, in many places verification means:

  • functions that test properties of the data structure
  • applied repeatedly after several rounds of insertions and/or deletions
  • combined with code coverage metrics ensuring that all of your code is exercised

With map-like data structures I like to keep a simple parallel data structure, such as a hashtable of all keys in the tree. Then among the tests executed after each round of insertions and/or deletions, you can verify that all the expected keys are in the tree, as well as that the tree has correct size. Of course, this is in addition to the basic tests that the red-black invariant holds, and that the tree is sufficiently balanced, and that the tree is ordered.

It's wise to use a random key generator, with parameters for the range of key sizes, to avoid biasing your tests. Add a random selection of insert, lookup, or delete operations, with a ratio dynamically biased to grow the tree to a sufficiently large size. Run it for a few hours and see if you can get 100% code coverage; extra credit for MC/DC coverage.

1
votes

A theoretical examination of the implementation is discussed in the Wikipedia article you reference.

If you want to test your particular implementation, then write the tests for each feature you want to test. Using the Wikipedia case studies would be a good start.

There are full formal proofs of red-black trees available online but it would be up to you to generate a formal proof of your particular implementation. Most people feel that formal proofs of programming programs are not worthwhile or useful.