From 5d8b80947727cb559e82d42242acfea260733947 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com> Date: Thu, 26 Apr 2012 16:59:50 +0200 Subject: [PATCH] Moving some tests into testcases --- mytest/Plus.scala | 13 --------- mytest/Sets2.scala | 29 ------------------- {mytest => testcases}/Add.scala | 0 {mytest => testcases}/BinarySearch.scala | 0 .../BubbleSort.scala | 0 {mytest => testcases}/LinearSearch.scala | 0 {mytest => testcases}/Mult.scala | 0 .../regression}/Epsilon1.scala | 0 .../regression}/Epsilon2.scala | 0 .../regression}/Epsilon3.scala | 0 .../regression}/Epsilon4.scala | 0 .../regression}/Epsilon5.scala | 0 .../regression}/Epsilon6.scala | 0 testcases/regression/MyTuple3.scala | 11 +++++++ testcases/regression/MyTuple4.scala | 14 +++++++++ testcases/regression/MyTuple5.scala | 10 +++++++ testcases/regression/MyTuple6.scala | 14 +++++++++ testcases/regression/MyTuple7.scala | 16 ++++++++++ {mytest => testcases/regression}/While1.scala | 0 {mytest => testcases/regression}/While2.scala | 0 20 files changed, 65 insertions(+), 42 deletions(-) delete mode 100644 mytest/Plus.scala delete mode 100644 mytest/Sets2.scala rename {mytest => testcases}/Add.scala (100%) rename {mytest => testcases}/BinarySearch.scala (100%) rename mytest/Bubble.scala => testcases/BubbleSort.scala (100%) rename {mytest => testcases}/LinearSearch.scala (100%) rename {mytest => testcases}/Mult.scala (100%) rename {mytest => testcases/regression}/Epsilon1.scala (100%) rename {mytest => testcases/regression}/Epsilon2.scala (100%) rename {mytest => testcases/regression}/Epsilon3.scala (100%) rename {mytest => testcases/regression}/Epsilon4.scala (100%) rename {mytest => testcases/regression}/Epsilon5.scala (100%) rename {mytest => testcases/regression}/Epsilon6.scala (100%) create mode 100644 testcases/regression/MyTuple3.scala create mode 100644 testcases/regression/MyTuple4.scala create mode 100644 testcases/regression/MyTuple5.scala create mode 100644 testcases/regression/MyTuple6.scala create mode 100644 testcases/regression/MyTuple7.scala rename {mytest => testcases/regression}/While1.scala (100%) rename {mytest => testcases/regression}/While2.scala (100%) diff --git a/mytest/Plus.scala b/mytest/Plus.scala deleted file mode 100644 index b0f08f168..000000000 --- a/mytest/Plus.scala +++ /dev/null @@ -1,13 +0,0 @@ -object Plus { - - def foo(): Int = ({ - - var a = 2 - var b = 1 - - a = {b = b + 2; a = a + 1; a} + {a = 5 - a; a} - a + b - }) ensuring(_ == 8) - - -} diff --git a/mytest/Sets2.scala b/mytest/Sets2.scala deleted file mode 100644 index 14e636924..000000000 --- a/mytest/Sets2.scala +++ /dev/null @@ -1,29 +0,0 @@ -import leon.Annotations._ -import leon.Utils._ - -object Sets2 { - sealed abstract class MyList - case class MyCons(head: Int, tail: MyList) extends MyList - case class MyNil() extends MyList - - def size(lst: MyList): Int = (lst match { - case MyNil() => 0 - case MyCons(_, xs) => 1 + size(xs) - }) - - def toSet(lst: MyList): Set[Int] = lst match { - case MyCons(x, xs) => toSet(xs) ++ Set(x) - case MyNil() => Set[Int]() - } - - def toList(set: Set[Int]): MyList = if(set == Set.empty[Int]) MyNil() else { - val elem = epsilon((x : Int) => set contains x) - MyCons(elem, toList(set -- Set[Int](elem))) - } - - @induct - def property(lst: MyList): Boolean = (size(toList(toSet(lst))) <= size(lst)) holds - - def wrongProperty0(lst: MyList): Boolean = (size(toList(toSet(lst))) == size(lst)) holds - def wrongProperty1(lst: MyList): Boolean = (toList(toSet(lst)) == lst) holds -} diff --git a/mytest/Add.scala b/testcases/Add.scala similarity index 100% rename from mytest/Add.scala rename to testcases/Add.scala diff --git a/mytest/BinarySearch.scala b/testcases/BinarySearch.scala similarity index 100% rename from mytest/BinarySearch.scala rename to testcases/BinarySearch.scala diff --git a/mytest/Bubble.scala b/testcases/BubbleSort.scala similarity index 100% rename from mytest/Bubble.scala rename to testcases/BubbleSort.scala diff --git a/mytest/LinearSearch.scala b/testcases/LinearSearch.scala similarity index 100% rename from mytest/LinearSearch.scala rename to testcases/LinearSearch.scala diff --git a/mytest/Mult.scala b/testcases/Mult.scala similarity index 100% rename from mytest/Mult.scala rename to testcases/Mult.scala diff --git a/mytest/Epsilon1.scala b/testcases/regression/Epsilon1.scala similarity index 100% rename from mytest/Epsilon1.scala rename to testcases/regression/Epsilon1.scala diff --git a/mytest/Epsilon2.scala b/testcases/regression/Epsilon2.scala similarity index 100% rename from mytest/Epsilon2.scala rename to testcases/regression/Epsilon2.scala diff --git a/mytest/Epsilon3.scala b/testcases/regression/Epsilon3.scala similarity index 100% rename from mytest/Epsilon3.scala rename to testcases/regression/Epsilon3.scala diff --git a/mytest/Epsilon4.scala b/testcases/regression/Epsilon4.scala similarity index 100% rename from mytest/Epsilon4.scala rename to testcases/regression/Epsilon4.scala diff --git a/mytest/Epsilon5.scala b/testcases/regression/Epsilon5.scala similarity index 100% rename from mytest/Epsilon5.scala rename to testcases/regression/Epsilon5.scala diff --git a/mytest/Epsilon6.scala b/testcases/regression/Epsilon6.scala similarity index 100% rename from mytest/Epsilon6.scala rename to testcases/regression/Epsilon6.scala diff --git a/testcases/regression/MyTuple3.scala b/testcases/regression/MyTuple3.scala new file mode 100644 index 000000000..48383898e --- /dev/null +++ b/testcases/regression/MyTuple3.scala @@ -0,0 +1,11 @@ +object MyTuple1 { + + def foo(): Int = { + val t = (1, true, 3) + val a1 = t._1 + val a2 = t._2 + val a3 = t._3 + a3 + } ensuring( _ == 3) + +} diff --git a/testcases/regression/MyTuple4.scala b/testcases/regression/MyTuple4.scala new file mode 100644 index 000000000..e928b2a9a --- /dev/null +++ b/testcases/regression/MyTuple4.scala @@ -0,0 +1,14 @@ +object MyTuple4 { + + abstract class A + case class B(i: Int) extends A + case class C(a: A) extends A + + def foo(): Int = { + val t = (B(2), C(B(3))) + t match { + case (B(x), C(y)) => x + } + } ensuring( _ > 0) + +} diff --git a/testcases/regression/MyTuple5.scala b/testcases/regression/MyTuple5.scala new file mode 100644 index 000000000..a36f3c73b --- /dev/null +++ b/testcases/regression/MyTuple5.scala @@ -0,0 +1,10 @@ +object MyTuple4 { + + def foo(): Int = { + val t = ((2, 3), true) + t._1._2 + } ensuring( _ == 3) + +} + +// vim: set ts=4 sw=4 et: diff --git a/testcases/regression/MyTuple6.scala b/testcases/regression/MyTuple6.scala new file mode 100644 index 000000000..4b87272e2 --- /dev/null +++ b/testcases/regression/MyTuple6.scala @@ -0,0 +1,14 @@ + +object MyTuple1 { + + abstract class A + case class B(i: Int) extends A + case class C(a: A) extends A + + def foo(): Int = { + val t = (1, (C(B(4)), 2), 3) + val (a1, (C(B(x)), a2), a3) = t + x + } ensuring( _ == 4) + +} diff --git a/testcases/regression/MyTuple7.scala b/testcases/regression/MyTuple7.scala new file mode 100644 index 000000000..6a55bc8c9 --- /dev/null +++ b/testcases/regression/MyTuple7.scala @@ -0,0 +1,16 @@ +object MyTuple1 { + + abstract class A + case class B(t: (Int, Int)) extends A + case class C(a: A) extends A + + def foo(): Int = { + val t: (Int, (A, Int), Int) = (1, (C(B((4, 5))), 2), 3) + t match { + case (_, (B((x, y)), _), _) => x + case (_, (C(B((_, x))), _), y) => x + case (_, _, x) => x + } + } ensuring( _ == 5) + +} diff --git a/mytest/While1.scala b/testcases/regression/While1.scala similarity index 100% rename from mytest/While1.scala rename to testcases/regression/While1.scala diff --git a/mytest/While2.scala b/testcases/regression/While2.scala similarity index 100% rename from mytest/While2.scala rename to testcases/regression/While2.scala -- GitLab