title: Test or verify properties of red-black tree
body: <p>I have based this code on the <a href="https://en.wikipedia.org/wiki/Red%E2%80%93black_tree" rel="nofollow noreferrer">Wikipedia article</a> 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.  </p>
  
  <pre><code>#include &lt;stdio.h&gt;
  #include &lt;assert.h&gt;
  #include &lt;stdlib.h&gt;
  
  
  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-&gt;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-&gt;left)
          return p-&gt;right;
      else
          return p-&gt;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-&gt;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-&gt;right = nnew-&gt;left;
      nnew-&gt;left = n;
      n-&gt;parent = nnew;
      // handle other child/parent pointers
      if (n-&gt;right != NULL)
          n-&gt;right-&gt;parent = n;
      if (p != NULL) // initially n could be the root
      {
          if (n == p-&gt;left)
              p-&gt;left = nnew;
          else if (n == p-&gt;right) // if (...) is excessive
              p-&gt;right = nnew;
      }
      nnew-&gt;parent = p;
  }
  
  void rotate_right(struct node *n) {
      struct node *nnew = n-&gt;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-&gt;left = nnew-&gt;right;
      nnew-&gt;right = n;
      n-&gt;parent = nnew;
      // handle other child/parent pointers
      if (n-&gt;left != NULL)
          n-&gt;left-&gt;parent = n;
      if (p != NULL) // initially n could be the root
      {
          if (n == p-&gt;left)
              p-&gt;left = nnew;
          else if (n == p-&gt;right) // if (...) is excessive
              p-&gt;right = nnew;
      }
      nnew-&gt;parent = p;
  }
  
  void insert_recurse(struct node* root, struct node* n) {
      // recursively descend the tree until a leaf is found
      if (root != NULL &amp;&amp; n-&gt;key &lt; root-&gt;key) {
          if (root-&gt;left != LEAF) {
              insert_recurse(root-&gt;left, n);
              return;
          }
          else
              root-&gt;left = n;
      } else if (root != NULL) {
          if (root-&gt;right != LEAF){
              insert_recurse(root-&gt;right, n);
              return;
          }
          else
              root-&gt;right = n;
      }
  
      // insert new node n
      n-&gt;parent = root;
      n-&gt;left = LEAF;
      n-&gt;right = LEAF;
      n-&gt;color = RED;
  }
  
  
  void insert_case1(struct node* n)
  {
      if (parent(n) == NULL)
          n-&gt;color = BLACK;
  }
  
  void insert_case2(struct node* n)
  {
      return; /* Do nothing since tree is still valid */
  }
  void insert_case3(struct node* n)
  {
      parent(n)-&gt;color = BLACK;
      uncle(n)-&gt;color = BLACK;
      grandparent(n)-&gt;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-&gt;left)
          rotate_right(g);
      else
          rotate_left(g);
      p-&gt;color = BLACK;
      g-&gt;color = RED;
  }
  
  
  void insert_case4(struct node* n)
  {
      struct node* p = parent(n);
      struct node* g = grandparent(n);
  
      if (n == g-&gt;left-&gt;right) {
          rotate_left(p);
          n = n-&gt;left;
      } else if (n == g-&gt;right-&gt;left) {
          rotate_right(p);
          n = n-&gt;right;
      }
  
      insert_case4step2(n);
  }
  
  
  
  void insert_repair_tree(struct node* n) {
      if (parent(n) == NULL) {
          insert_case1(n);
      } else if (parent(n)-&gt;color == BLACK) {
          insert_case2(n);
      } else if (uncle(n)-&gt;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-&gt;parent = n-&gt;parent;
      if (n == n-&gt;parent-&gt;left)
          n-&gt;parent-&gt;left = child;
      else
          n-&gt;parent-&gt;right = child;
  }
  
  int is_leaf(struct node* n){
      if(n-&gt;right ==NULL &amp;&amp; n-&gt;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-&gt;right) ? n-&gt;left : n-&gt;right;
  
      replace_node(n, child);
      if (n-&gt;color == BLACK) {
          if (child-&gt;color == RED)
              child-&gt;color = BLACK;
          else
              delete_case1(child);
      }
      free(n);
  }
  
  void delete_case1(struct node* n)
  {
      if (n-&gt;parent != NULL)
          delete_case2(n);
  }
  
  void delete_case2(struct node* n)
  {
      struct node* s = sibling(n);
  
      if (s-&gt;color == RED) {
          n-&gt;parent-&gt;color = RED;
          s-&gt;color = BLACK;
          if (n == n-&gt;parent-&gt;left)
              rotate_left(n-&gt;parent);
          else
              rotate_right(n-&gt;parent);
      }
      delete_case3(n);
  }
  
  void delete_case3(struct node* n)
  {
      struct node* s = sibling(n);
  
      if ((n-&gt;parent-&gt;color == BLACK) &amp;&amp;
          (s-&gt;color == BLACK) &amp;&amp;
          (s-&gt;left-&gt;color == BLACK) &amp;&amp;
          (s-&gt;right-&gt;color == BLACK)) {
          s-&gt;color = RED;
          delete_case1(n-&gt;parent);
      } else
          delete_case4(n);
  }
  
  void delete_case4(struct node* n)
  {
      struct node* s = sibling(n);
  
      if ((n-&gt;parent-&gt;color == RED) &amp;&amp;
          (s-&gt;color == BLACK) &amp;&amp;
          (s-&gt;left-&gt;color == BLACK) &amp;&amp;
          (s-&gt;right-&gt;color == BLACK)) {
          s-&gt;color = RED;
          n-&gt;parent-&gt;color = BLACK;
      } else
          delete_case5(n);
  }
  
  void delete_case6(struct node* n)
  {
      struct node* s = sibling(n);
  
      s-&gt;color = n-&gt;parent-&gt;color;
      n-&gt;parent-&gt;color = BLACK;
  
      if (n == n-&gt;parent-&gt;left) {
          s-&gt;right-&gt;color = BLACK;
          rotate_left(n-&gt;parent);
      } else {
          s-&gt;left-&gt;color = BLACK;
          rotate_right(n-&gt;parent);
      }
  }
  
  void delete_case5(struct node* n)
  {
      struct node* s = sibling(n);
  
      if  (s-&gt;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-&gt;parent-&gt;left) &amp;&amp;
              (s-&gt;right-&gt;color == BLACK) &amp;&amp;
              (s-&gt;left-&gt;color == RED)) { /* this last test is trivial too due to cases 2-4. */
              s-&gt;color = RED;
              s-&gt;left-&gt;color = BLACK;
              rotate_right(s);
          } else if ((n == n-&gt;parent-&gt;right) &amp;&amp;
                     (s-&gt;left-&gt;color == BLACK) &amp;&amp;
                     (s-&gt;right-&gt;color == RED)) {/* this last test is trivial too due to cases 2-4. */
              s-&gt;color = RED;
              s-&gt;right-&gt;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-&gt;key;
          if (diff &gt; 0) {
              temp = temp-&gt;right;
          } else if (diff &lt; 0) {
              temp = temp-&gt;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-&gt;left);
  
          printf(" %d--%c ", temp-&gt;key, temp-&gt;color);
  
          inorderTree(temp-&gt;right);
  
      }
  }
  
  void postorderTree(struct node *root) {
      struct node *temp = root;
  
      if (temp != NULL) {
          postorderTree(temp-&gt;left);
          postorderTree(temp-&gt;right);
          printf(" %d--%c ", temp-&gt;key, temp-&gt;color);
      }
  }
  
  void traversal(struct node *root) {
      if (root != NULL) {
          printf("root is %d-- %c", root-&gt;key, root-&gt;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-&gt;color=BLACK;
      LEAF-&gt;left=NULL;
      LEAF-&gt;right=NULL;
      LEAF-&gt;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", &amp;choice);
          switch (choice) {
              case 1:
                  setbuf(stdout, 0);
                  printf("Enter the integer you want to add : ");
                  scanf("%d", &amp;val);
                  struct node *z = malloc(sizeof(struct node));
                  z-&gt;key = val;
                  z-&gt;left = NULL;
                  z-&gt;right = NULL;
                  z-&gt;parent = NULL;
                  z-&gt;color = RED;
                  root = insert(root, z);
                  printf("The root is now %d: ", root-&gt;key);
  
                  break;
              case 2:
                  printf("Enter the integer you want to delete : ");
                  scanf("%d", &amp;var);
                  delete_one_child(search(root, var));
                  break;
              case 3:
                  printf("Enter search element \n");
                  scanf("%d", &amp;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;
  }
  </code></pre>