From c6ecee57fbd3c0a2b1e9b2c35033a52d58a9631d Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <vkuncak@gmail.com>
Date: Fri, 9 Jul 2010 15:58:52 +0000
Subject: [PATCH] more better

---
 testcases/BinarySearchTree.scala | 40 ++++++++++++++++++++++++++++----
 1 file changed, 36 insertions(+), 4 deletions(-)

diff --git a/testcases/BinarySearchTree.scala b/testcases/BinarySearchTree.scala
index 617749916..09ed4c67a 100644
--- a/testcases/BinarySearchTree.scala
+++ b/testcases/BinarySearchTree.scala
@@ -14,7 +14,8 @@ object BinarySearchTree {
     sealed abstract class Triple
     case class SortedTriple(min:Int,max:Int,sorted:Boolean) extends Triple
 
-/*    def isSorted(tree: Tree): SortedTriple = tree match {
+/*
+    def isSorted(tree: Tree): SortedTriple = tree match {
       case Leaf() => SortedTriple(None(), None(), true)
       case Node(l,v,r) => sorted(l) match {
         case SortedTriple(minl,maxl,false) => SortedTriple(None(), None(), false)
@@ -52,9 +53,39 @@ object BinarySearchTree {
 	    case _ => SortedTriple(None(),None(),false)
 	  }
 	}
-      }*/
+      }
+    }
+  */
+
+    def treeMin(tree : Node) : Int = tree match {
+      case Node(left,v,_) => left match {
+	case Leaf() => v
+	case n @ Node(_,_,_) => treeMin(n)
+      }
+    }
+
+    def treeMax(tree : Node) : Int = tree match {
+      case Node(_,v,right) => right match {
+        case Leaf() => v
+	case n @ Node(_,_,_) => treeMax(n)
+      }
+    }
+
+    def insert(tree: Tree, value: Int) : Node = {
+      //require(isSorted(tree))
+      tree match {
+        case Leaf() => Node(Leaf(), value, Leaf())
+        case n @ Node(l, v, r) => if(v < value) {
+          Node(l, v, insert(r, value))
+        } else if(v > value) {
+          Node(insert(l, value), v, r)
+        } else {
+          n
+        }
+    }} ensuring (contents(_) == contents(tree) ++ Set(value))
 
-    def insert(tree: Tree, value: Int) : Node = (tree match {
+/*
+    def remove(tree: Tree, value: Int) : Node = (tree match {
         case Leaf() => Node(Leaf(), value, Leaf())
         case n @ Node(l, v, r) => if(v < value) {
           Node(l, v, insert(r, value))
@@ -63,7 +94,8 @@ object BinarySearchTree {
         } else {
           n
         }
-    }) ensuring (contents(_) == contents(tree) ++ Set(value))
+    }) ensuring (contents(_) == contents(tree) -- Set(value))
+*/
 
     def contains(tree: Tree, value: Int) : Boolean = tree match {
         case Leaf() => false
-- 
GitLab