--- a/src/insert_verification/akashaLLRBContext.c	Tue Mar 22 15:26:22 2016 +0900
+++ b/src/insert_verification/akashaLLRBContext.c	Tue Mar 22 15:39:31 2016 +0900
@@ -5,6 +5,7 @@
 extern __code showTree_stub(struct Context*);
 extern __code iterateInsertion_stub(struct Context*);
 extern __code putAndGoToNextDepth_stub (struct Context*);
+extern __code verifySpecification_stub (struct Context*);
 extern __code duplicateIterator_stub(struct Context*);
 extern __code duplicateIteratorElem_stub(struct Context*);
 extern __code duplicateTree_stub(struct Context*);
@@ -65,6 +66,7 @@
     context->code[ShowTree]              = showTree_stub;
     context->code[IterateInsertion]      = iterateInsertion_stub;
     context->code[PutAndGoToNextDepth]   = putAndGoToNextDepth_stub;
+    context->code[VerifySpecification]   = verifySpecification_stub;;
     context->code[DuplicateIterator]     = duplicateIterator_stub;
     context->code[DuplicateIteratorElem] = duplicateIteratorElem_stub;
     context->code[DuplicateTree]         = duplicateTree_stub;

--- a/src/insert_verification/include/akashaLLRBContext.h	Tue Mar 22 15:26:22 2016 +0900
+++ b/src/insert_verification/include/akashaLLRBContext.h	Tue Mar 22 15:39:31 2016 +0900
@@ -2,12 +2,13 @@
 #include "stack.h"
 
 #define ALLOCATE_SIZE 10000000
-#define LIMIT_OF_VERIFICATION_SIZE 4
+#define LIMIT_OF_VERIFICATION_SIZE 7
 
 enum Code {
     ShowTree,
     IterateInsertion,
     PutAndGoToNextDepth,
+    VerifySpecification,
     DuplicateIterator,
     DuplicateIteratorElem,
     DuplicateTree,

--- a/src/insert_verification/main.c	Tue Mar 22 15:26:22 2016 +0900
+++ b/src/insert_verification/main.c	Tue Mar 22 15:39:31 2016 +0900
@@ -6,6 +6,38 @@
 extern void allocator(struct Context* context);
 void showTrace(struct Iterator* iter); //FIXME
 
+/* C functions (TODO: convert to code segment) */
+
+unsigned int min_height(struct Node* node, unsigned int height) {
+    if ((node->left == NULL) && (node->right == NULL)) return height;
+    if (node->left  == NULL) return min_height(node->right, height+1);
+    if (node->right == NULL) return min_height(node->left, height+1);
+
+    unsigned int left_min  = min_height(node->left, height+1);
+    unsigned int right_min = min_height(node->right, height+1);
+
+    if (left_min < right_min) {
+        return left_min;
+    } else {
+        return right_min;
+    }
+}
+
+unsigned int max_height(struct Node* node, unsigned int height) {
+    if ((node->left == NULL) && (node->right == NULL)) return height;
+    if (node->left  == NULL) return max_height(node->right, height+1);
+    if (node->right == NULL) return max_height(node->left, height+1);
+
+    unsigned int left_max  = max_height(node->left, height+1);
+    unsigned int right_max = max_height(node->right, height+1);
+
+    if (left_max > right_max) {
+        return left_max;
+    } else {
+        return right_max;
+    }
+}
+
 void printTree(struct Node* node, int n) {
     if (node != 0) {
         printTree(node->left, n+1);
@@ -16,6 +48,18 @@
     }
 }
 
+void showTrace(struct Iterator* iter) {
+    printf("show trace(reversed):");
+
+    for (; iter != NULL; iter = iter->previousDepth) {
+        printf("%u ", iter->iteratedValue);
+    }
+    printf("\n");
+}
+
+
+/* Code Segments */
+
 __code showTree_stub(struct Context* context) {
     goto showTree(context, &context->data[Tree]->tree);
 }
@@ -27,9 +71,6 @@
     goto meta(context, Exit);
 }
 
-__code verifySpecification(struct Context* context) {
-}
-
 __code iterateInsertion_stub(struct Context* context) {
     goto iterateInsertion(context, &context->data[Iter]->iterator, &context->data[Node]->node);
 }
@@ -61,11 +102,30 @@
     if (iter->head == iter->head->next) {
         context->next = GoToPreviousDepth;
     } else {
-        context->next = DuplicateIterator;
+        context->next = VerifySpecification;
     }
     goto meta(context, Put);
 }
 
+__code verifySpecification_stub(struct Context* context) {
+    goto verifySpecification(context, &context->data[Tree]->tree, &context->data[Iter]->iterator);
+}
+
+__code verifySpecification(struct Context* context, struct Tree* tree, struct Iterator* iter) {
+    unsigned const int min_h = min_height(tree->root, 1);
+    unsigned const int max_h = max_height(tree->root, 1);
+
+    if (max_h > 2*min_h) {
+        printf("llrb-condition violated.\n");
+        printf("\tmin-height %u\n", min_h);
+        printf("\tmax-height %u\n", max_h);
+        showTrace(iter);
+        exit(1);
+    }
+
+    goto meta(context, DuplicateIterator);
+}
+
 __code duplicateIterator_stub(struct Context* context) {
     goto duplicateIterator(context, &context->data[Allocate]->allocate, &context->data[Iter]->iterator);
 }
@@ -150,15 +210,6 @@
     goto meta(context, PutAndGoToNextDepth);
 }
 
-void showTrace(struct Iterator* iter) {
-    printf("show trace(reversed):");
-
-    for (; iter != NULL; iter = iter->previousDepth) {
-        printf("%u ", iter->iteratedValue);
-    }
-    printf("\n");
-}
-
 int main(int argc, char const* argv[]) {
     goto startCode(PutAndGoToNextDepth);
 }