diff --git a/mytest/Plus.scala b/mytest/Plus.scala deleted file mode 100644 index b0f08f1686c15b7126231fcf0f94e194cf7eb248..0000000000000000000000000000000000000000 --- 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 14e636924d9c44a660a6d168b0a7a6badc5c8307..0000000000000000000000000000000000000000 --- 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 0000000000000000000000000000000000000000..48383898e203c723751a7a53869ac6c8c69ae3b5 --- /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 0000000000000000000000000000000000000000..e928b2a9aec650923f5a0f6f980a3c6fe03c7695 --- /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 0000000000000000000000000000000000000000..a36f3c73b7893563371bbb15302a5923bc85b3e9 --- /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 0000000000000000000000000000000000000000..4b87272e23f7d9f2a3c33c29b5d455b88f234ddb --- /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 0000000000000000000000000000000000000000..6a55bc8c9cdbc4f70be7a6b79c8d11137ecb0d71 --- /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