more epsilon tests

mytest/Epsilon3.scala

+import leon.Utils._
+
+object Epsilon3 {
+
+  def pos(): Int = {
+    epsilon((y: Int) => y > 0)
+  } ensuring(_ >= 0)
+
+  def posWrong(): Int = {
+    epsilon((y: Int) => y >= 0)
+  } ensuring(_ > 0)
+
+}

mytest/Epsilon4.scala

+import leon.Utils._
+
+object Epsilon4 {
+
+  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)))
+  }
+
+  //timeout, but this probably means that it is valid as expected
+  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
+}

mytest/Epsilon5.scala

+import leon.Utils._
+
+object Epsilon5 {
+
+  def foo(x: Int, y: Int): Int = {
+    epsilon((z: Int) => z > x && z < y)
+  } ensuring(_ >= x)
+
+  def fooWrong(x: Int, y: Int): Int = {
+    epsilon((z: Int) => z >= x && z <= y)
+  } ensuring(_ > x)
+
+}
+
+// vim: set ts=4 sw=4 et:

mytest/Epsilon6.scala

+import leon.Utils._
+
+object Epsilon6 {
+
+  def fooWrong(): Int = {
+    epsilon((y: Int) => y > epsilon((z: Int) => z < y))
+  } ensuring(_ >= 0)
+
+  def foo(): Int = {
+    epsilon((y: Int) => y > epsilon((z: Int) => z < y))
+  } ensuring(res => res >= 0 || res < 0)
+
+}