From fddd97ca76c95b9be4e0cea0a608a878d3f656d8 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Fri, 25 Apr 2014 14:22:42 +0200
Subject: [PATCH] Add BinarySearchTree with isSorted and buggyMerge
---
.../BinarySearchTreeSorted.scala | 57 +++++++++++++++++++
1 file changed, 57 insertions(+)
create mode 100644 testcases/datastructures/BinarySearchTreeSorted.scala
diff --git a/testcases/datastructures/BinarySearchTreeSorted.scala b/testcases/datastructures/BinarySearchTreeSorted.scala
new file mode 100644
index 000000000..464335f62
--- /dev/null
+++ b/testcases/datastructures/BinarySearchTreeSorted.scala
@@ -0,0 +1,57 @@
+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))
+}
--
GitLab