From 7ba98f5b95d3fc7fa9038bbb39cdc889937dea9e Mon Sep 17 00:00:00 2001
From: Robin Steiger <robin.steiger@epfl.ch>
Date: Mon, 12 Jul 2010 22:28:31 +0000
Subject: [PATCH] Regression tests, they were working at rev 1137 but they
break now..
---
testcases/regression/README | 29 ++++++++++++
testcases/regression/unifier_valid.scala | 60 ++++++++++++++++++++++++
2 files changed, 89 insertions(+)
create mode 100644 testcases/regression/README
create mode 100644 testcases/regression/unifier_valid.scala
diff --git a/testcases/regression/README b/testcases/regression/README
new file mode 100644
index 000000000..f9d40ee46
--- /dev/null
+++ b/testcases/regression/README
@@ -0,0 +1,29 @@
+Revision 1137, this morning 11:20, everything worked:
+====================================================
+mkInfiniteTree postcondition valid Unifier
+dumbInsert postcondition valid Unifier
+insert postcondition valid Unifier
+createRoot postcondition valid Unifier
+dumbInsertWithOrder postcondition valid Unifier
+====================================================
+
+Revision 1147, this evening 19:32, already broken:
+====================================================
+mkInfiniteTree postcondition valid Unifier
+dumbInsert postcondition unknown ---
+insert postcondition unknown ---
+createRoot postcondition valid Unifier
+dumbInsertWithOrder postcondition unknown ---
+====================================================
+
+Revision 1157, now, even worse
+====================================================
+dumbInsertWithOrder postcondition unknown ---
+createRoot postcondition unknown ---
+mkInfiniteTree postcondition valid Unifier
+insert postcondition unknown ---
+dumbInsert postcondition unknown ---
+====================================================
+
+Would be great if we could this working again...
+
diff --git a/testcases/regression/unifier_valid.scala b/testcases/regression/unifier_valid.scala
new file mode 100644
index 000000000..d201527ce
--- /dev/null
+++ b/testcases/regression/unifier_valid.scala
@@ -0,0 +1,60 @@
+import scala.collection.immutable.Set
+
+object BinarySearchTree {
+
+ /* Data types and the catamorphism */
+
+ sealed abstract class Tree
+ case class Node(left: Tree, value: Int, right: Tree) extends Tree
+ case class Leaf() extends Tree
+
+ def contents(tree: Tree): Set[Int] = tree match {
+ case Leaf() => Set.empty[Int]
+ case Node(l, v, r) => contents(l) ++ Set(v) ++ contents(r)
+ }
+
+ /* Tests */
+
+ def insert(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))
+ } else if (v > value) {
+ Node(insert(l, value), v, r)
+ } else {
+ n
+ }
+ }
+ } ensuring (contents(_) == contents(tree) ++ Set(value))
+
+
+ def dumbInsert(tree: Tree): Node = {
+ tree match {
+ case Leaf() => Node(Leaf(), 0, Leaf())
+ case Node(l, e, r) => Node(dumbInsert(l), e, r)
+ }
+ } ensuring (contents(_) == contents(tree) ++ Set(0))
+
+
+ def dumbInsertWithOrder(tree: Tree): Node = {
+ tree match {
+ case Leaf() => Node(Leaf(), 0, Leaf())
+ case Node(l, e, r) => Node(dumbInsert(l), e, r)
+ }
+ } ensuring (res => {val S = contents(res); S == contents(tree) ++ Set(0) && S.min <= 0 && S.max >= 0})
+
+
+ def createRoot(v: Int): Node = {
+ Node(Leaf(), v, Leaf())
+ } ensuring (contents(_) == Set(v))
+
+
+ def mkInfiniteTree(x: Int): Node = {
+ Node(mkInfiniteTree(x), x, mkInfiniteTree(x))
+ } ensuring (res =>
+ res.left != Leaf() && res.right != Leaf()
+ )
+
+}
+
--
GitLab