Buggy balancing method in RBT, a precondition in insertion sort.

demo/InsertionSort.scala

@@ -29,24 +29,24 @@ object InsertionSort {
     }
   }
 
-  def minProp0(l : List) : Boolean = (l match {
-    case Nil() => true
-    case c @ Cons(x, xs) => min(c) match {
-      case None() => false
-      case Some(m) => x >= m
-    }
-  }) holds
+  // def minProp0(l : List) : Boolean = (l match {
+  //   case Nil() => true
+  //   case c @ Cons(x, xs) => min(c) match {
+  //     case None() => false
+  //     case Some(m) => x >= m
+  //   }
+  // }) holds
 
-  def minProp1(l : List) : Boolean = {
-    require(isSorted(l) && size(l) <= 5)
-    l match {
-      case Nil() => true
-      case c @ Cons(x, xs) => min(c) match {
-        case None() => false
-        case Some(m) => x == m
-      }
-    }
-  } holds
+  // def minProp1(l : List) : Boolean = {
+  //   require(isSorted(l) && size(l) <= 5)
+  //   l match {
+  //     case Nil() => true
+  //     case c @ Cons(x, xs) => min(c) match {
+  //       case None() => false
+  //       case Some(m) => x == m
+  //     }
+  //   }
+  // } holds
 
   def isSorted(l: List): Boolean = l match {
     case Nil() => true
@@ -70,7 +70,7 @@ object InsertionSort {
   /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
    * the expected content and size */
   def buggySortedIns(e: Int, l: List): List = {
-    // require(isSorted(l))
+    require(isSorted(l))
     l match {
       case Nil() => Cons(e,Nil())
       case Cons(x,xs) => if (x <= e) Cons(x,buggySortedIns(e, xs)) else Cons(e, l)

demo/RedBlackTree.scala

@@ -84,7 +84,7 @@ object RedBlackTree {
   
   def buggyAdd(x: Int, t: Tree): Tree = {
     require(redNodesHaveBlackChildren(t))
-    makeBlack(ins(x, t))
+    ins(x, t)
   } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
   
   def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
@@ -100,4 +100,18 @@ object RedBlackTree {
       case Node(c,a,xV,b) => Node(c,a,xV,b)
     }
   } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
+
+  def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+    Node(c,a,x,b) match {
+      case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) => 
+        Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+      case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) => 
+        Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+      case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) => 
+        Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+      case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) => 
+        Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+      // case Node(c,a,xV,b) => Node(c,a,xV,b)
+    }
+  } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
 }