From 6a0d337cb5bf63a2e2ceaf821168b70d4a5b85cb Mon Sep 17 00:00:00 2001
From: Robin Steiger <robin.steiger@epfl.ch>
Date: Sun, 11 Jul 2010 15:11:11 +0000
Subject: [PATCH] Moved mkInfiniteTree example to demo file.
---
testcases/BinarySearchTree.scala | 6 ++++++
testcases/UnificationTest.scala | 8 --------
2 files changed, 6 insertions(+), 8 deletions(-)
diff --git a/testcases/BinarySearchTree.scala b/testcases/BinarySearchTree.scala
index a8116240b..463ae6c02 100644
--- a/testcases/BinarySearchTree.scala
+++ b/testcases/BinarySearchTree.scala
@@ -133,6 +133,12 @@ object BinarySearchTree {
}) ensuring (contents(_) == contents(tree) -- Set(value))
*/
+ def mkInfiniteTree(x: Int): Node = {
+ Node(mkInfiniteTree(x), x, mkInfiniteTree(x))
+ } ensuring (res =>
+ res.left != Leaf() && res.right != Leaf()
+ )
+
def contains(tree: Tree, value: Int): Boolean = tree match {
case Leaf() => false
case n@Node(l, v, r) => if (v < value) {
diff --git a/testcases/UnificationTest.scala b/testcases/UnificationTest.scala
index 60f06c4e4..2202a573d 100644
--- a/testcases/UnificationTest.scala
+++ b/testcases/UnificationTest.scala
@@ -43,14 +43,6 @@ object UnificationTest {
})*/
-
- // Proved by unifier
- def mkInfiniteTree(x: Int): Node = {
- Node(mkInfiniteTree(x), x, mkInfiniteTree(x))
- } ensuring (res =>
- res.left != Leaf() && res.right != Leaf()
- )
-
// Cannot be solved yet, due to the presence of an if expression
def insert(tree: Tree, value: Int) : Node = (tree match {
case Leaf() => Node(Leaf(), value, Leaf())
--
GitLab