Add BinarySearchTree with isSorted and buggyMerge

testcases/datastructures/BinarySearchTreeSorted.scala

+import leon.lang._
+import leon.annotation._
+import leon._
+
+object BinaryTree {
+  sealed abstract class Tree
+  case class Node(left: Tree, value: Int, right: Tree) extends Tree
+  case class Leaf() extends Tree
+
+  case class SortedTriple(min: Option[Int], max: Option[Int], sorted: Boolean)
+
+  def isSortedTriple(tree: Tree) : SortedTriple = (tree match {
+    case Leaf() => SortedTriple(None(), None(), true)
+    case Node(l, v, r) =>
+      (isSortedTriple(l), isSortedTriple(r)) match {
+        case (SortedTriple(minl, maxl, sortedl), SortedTriple(minr, maxr, sortedr)) =>
+          val sorted = sortedl && sortedr && (v > maxl.getOrElse(v-1)) && (v < minr.getOrElse(v+1))
+          SortedTriple(minl.orElse(Some(v)), maxr.orElse(Some(v)), sorted)
+      }
+  }) ensuring { res => res match {
+    case SortedTriple(Some(min), Some(max), res) => !res || (min <= max)
+    case SortedTriple(None(), None(), res) => res
+    case _ => false
+  }}
+
+  def isSorted(tree: Tree): Boolean = isSortedTriple(tree).sorted
+
+  def insert(tree: Tree, value: Int): Tree = ({
+    require(isSorted(tree))
+    tree match {
+      case Leaf() => Node(Leaf(), value, Leaf())
+      case Node(l, v, r) => if (v < value) {
+        Node(l, v, insert(r, value))
+      } else if (v > value) {
+        Node(insert(l, value), v, r)
+      } else {
+        Node(l,v,r)
+      }
+    }
+  }) ensuring (res => isSorted(res))
+
+  def buggyMerge(t1 : Tree, t2 : Tree) : Tree = ({
+    require(isSorted(t1) && isSorted(t2))
+    (t1, t2) match {
+      case (Leaf(), _) => t2
+      case (_, Leaf()) => t1
+      case (t1 @ Node(l1, v1, r1), t2 @ Node(l2, v2, r2)) =>
+        if (v1 < v2) {
+          Node(buggyMerge(t1, l2), v2, r2)
+        } else if (v2 < v1) {
+          Node(buggyMerge(l1, t2), v1, r1)
+        } else {
+          Node(buggyMerge(l1, l2), v1, buggyMerge(r1, r2))
+        }
+    }
+  }) ensuring (res => isSorted(res))
+}