Skip to content
Snippets Groups Projects
Commit 5d8b8094 authored by Régis Blanc's avatar Régis Blanc
Browse files

Moving some tests into testcases

parent c219c26a
Branches
Tags
No related merge requests found
Showing
with 65 additions and 42 deletions
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)
}
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
}
File moved
File moved
File moved
File moved
File moved
File moved
File moved
File moved
File moved
File moved
File moved
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)
}
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)
}
object MyTuple4 {
def foo(): Int = {
val t = ((2, 3), true)
t._1._2
} ensuring( _ == 3)
}
// vim: set ts=4 sw=4 et:
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)
}
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)
}
File moved
File moved
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment