Skip to content
Snippets Groups Projects
Commit 8c91bcc4 authored by Etienne Kneuss's avatar Etienne Kneuss
Browse files

Remove unused ad-hoc test files

parent a3cab185
Branches
Tags
No related merge requests found
Showing
with 0 additions and 223 deletions
object Array1 {
def foo(): Int = {
val a = Array.fill(5)(0)
a(2) = 3
a(2)
} ensuring(_ == 0)
}
object Array2 {
def foo(): Int = {
val a = Array.fill(5)(0)
a(2) = 3
a.length
} ensuring(_ == 4)
}
import leon.Utils._
object Array3 {
def foo(): Int = {
val a = Array.fill(5)(3)
var i = 0
var sum = 0
(while(i <= a.length) {
sum = sum + a(i)
i = i + 1
}) invariant(i >= 0)
sum
} ensuring(_ == 15)
}
import leon.Utils._
object Array4 {
def foo(a: Array[Int]): Int = {
a(2)
}
}
import leon.Utils._
object Array4 {
def foo(a: Array[Int]): Int = {
require(a.length > 2)
a(2)
} ensuring(_ == 0)
}
import leon.Utils._
object Epsilon1 {
def rand2(x: Int): Int = epsilon((y: Int) => true)
//this should not hold
def property2(x: Int): Boolean = {
rand2(x) == rand2(x+1)
} holds
}
import leon.Utils._
object Epsilon1 {
def rand3(x: Int): Int = epsilon((y: Int) => x == x)
//this should not hold
def property3(x: Int): Boolean = {
rand3(x) == rand3(x+1)
} holds
}
import leon.Utils._
object Epsilon3 {
def posWrong(): Int = {
epsilon((y: Int) => y >= 0)
} ensuring(_ > 0)
}
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)))
}
def wrongProperty0(lst: MyList): Boolean = (size(toList(toSet(lst))) == size(lst)) holds
//def wrongProperty1(lst: MyList): Boolean = (toList(toSet(lst)) == lst) holds
}
import leon.Utils._
object Epsilon5 {
def fooWrong(x: Int, y: Int): Int = {
epsilon((z: Int) => z >= x && z <= y)
} ensuring(_ > x)
}
import leon.Utils._
object Epsilon6 {
def greaterWrong(x: Int): Int = {
epsilon((y: Int) => y >= x)
} ensuring(_ > x)
}
object IfExpr1 {
def foo(): Int = {
var a = 1
var b = 2
if({a = a + 1; a != b})
a = a + 3
else
b = a + b
a
} ensuring(_ == 3)
}
object IfExpr2 {
def foo(): Int = {
var a = 1
var b = 2
if(a < b) {
a = a + 3
b = b + 2
a = a + b
}
a
} ensuring(_ == 0)
}
object MyTuple1 {
def foo(): Int = {
val t = (1, true, 3)
val a1 = t._1
val a2 = t._2
val a3 = t._3
a3
} ensuring( _ == 1)
}
object MyTuple2 {
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( _ == 3)
}
object MyTuple3 {
def foo(t: (Int, Int)): (Int, Int) = {
t
} ensuring(res => res._1 > 0 && res._2 > 1)
}
object Unit1 {
def foo(u: Unit): Unit = ({
u
}) ensuring(_ != ())
}
object Array1 {
def foo(): Int = {
val a = Array.fill(5)(0)
a(2) = 3
a(2)
} ensuring(_ == 3)
}
object Array10 {
def foo(a: Array[Int]): Int = {
require(a.length > 0)
val b = a.clone
b(0)
} ensuring(res => res == a(0))
}
object Array2 {
def foo(): Int = {
val a = Array.fill(5)(0)
a(2) = 3
a.length
} ensuring(_ == 5)
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment