diff --git a/testcases/verification/scala2013/SumAndMax.scala b/testcases/verification/SumAndMax.scala
similarity index 74%
rename from testcases/verification/scala2013/SumAndMax.scala
rename to testcases/verification/SumAndMax.scala
index a3fd5c3a50d6c56592dbd6d48b7bc90ac940d58f..0fe57b67a2101aca59a192f5392e255e2786fb12 100644
--- a/testcases/verification/scala2013/SumAndMax.scala
+++ b/testcases/verification/SumAndMax.scala
@@ -3,10 +3,10 @@ import leon.annotation._
object SumAndMax {
sealed abstract class List
- case class Cons(head : Int, tail : List) extends List
+ case class Cons(head : BigInt, tail : List) extends List
case class Nil() extends List
- def max(list : List) : Int = {
+ def max(list : List) : BigInt = {
require(list != Nil())
list match {
case Cons(x, Nil()) => x
@@ -17,14 +17,14 @@ object SumAndMax {
}
}
- def sum(list : List) : Int = list match {
- case Nil() => 0
+ def sum(list : List) : BigInt = list match {
+ case Nil() => BigInt(0)
case Cons(x, xs) => x + sum(xs)
}
- def size(list : List) : Int = (list match {
- case Nil() => 0
- case Cons(_, xs) => 1 + size(xs)
+ def size(list : List) : BigInt = (list match {
+ case Nil() => BigInt(0)
+ case Cons(_, xs) => size(xs) + 1
}) ensuring(_ >= 0)
def allPos(list : List) : Boolean = list match {
diff --git a/testcases/verification/vstte10competition/AmortizedQueue.scala b/testcases/verification/vstte10competition/AmortizedQueue.scala
deleted file mode 100644
index 4ba21d023bc9b47e26ad479b111396750829037a..0000000000000000000000000000000000000000
--- a/testcases/verification/vstte10competition/AmortizedQueue.scala
+++ /dev/null
@@ -1,123 +0,0 @@
-import leon.lang._
-import leon.annotation._
-
-object AmortizedQueue {
- sealed abstract class List
- case class Cons(head : Int, tail : List) extends List
- case class Nil() extends List
-
- sealed abstract class AbsQueue
- case class Queue(front : List, rear : List) extends AbsQueue
-
- def size(list : List) : Int = (list match {
- case Nil() => 0
- case Cons(_, xs) => 1 + size(xs)
- }) ensuring(_ >= 0)
-
- def content(l: List) : Set[Int] = l match {
- case Nil() => Set.empty[Int]
- case Cons(x, xs) => Set(x) ++ content(xs)
- }
-
- def asList(queue : AbsQueue) : List = queue match {
- case Queue(front, rear) => concat(front, reverse(rear))
- }
-
- def concat(l1 : List, l2 : List) : List = (l1 match {
- case Nil() => l2
- case Cons(x,xs) => Cons(x, concat(xs, l2))
- }) ensuring (res => size(res) == size(l1) + size(l2) && content(res) == content(l1) ++ content(l2))
-
- def isAmortized(queue : AbsQueue) : Boolean = queue match {
- case Queue(front, rear) => size(front) >= size(rear)
- }
-
- def isEmpty(queue : AbsQueue) : Boolean = queue match {
- case Queue(Nil(), Nil()) => true
- case _ => false
- }
-
- def reverse(l : List) : List = (l match {
- case Nil() => Nil()
- case Cons(x, xs) => concat(reverse(xs), Cons(x, Nil()))
- }) ensuring (content(_) == content(l))
-
- def amortizedQueue(front : List, rear : List) : AbsQueue = {
- if (size(rear) <= size(front))
- Queue(front, rear)
- else
- Queue(concat(front, reverse(rear)), Nil())
- } ensuring(isAmortized(_))
-
- def enqueue(queue : AbsQueue, elem : Int) : AbsQueue = (queue match {
- case Queue(front, rear) => amortizedQueue(front, Cons(elem, rear))
- }) ensuring(isAmortized(_))
-
- def tail(queue : AbsQueue) : AbsQueue = {
- require(isAmortized(queue) && !isEmpty(queue))
- queue match {
- case Queue(Cons(f, fs), rear) => amortizedQueue(fs, rear)
- }
- } ensuring (isAmortized(_))
-
- def front(queue : AbsQueue) : Int = {
- require(isAmortized(queue) && !isEmpty(queue))
- queue match {
- case Queue(Cons(f, _), _) => f
- }
- }
-
- @induct
- def propEnqueue(rear : List, front : List, list : List, elem : Int) : Boolean = {
- require(isAmortized(Queue(front, rear)))
- val queue = Queue(front, rear)
- if (asList(queue) == list) {
- asList(enqueue(queue, elem)) == concat(list, Cons(elem, Nil()))
- } else
- true
- } // holds
-
- @induct
- def propFront(queue : AbsQueue, list : List, elem : Int) : Boolean = {
- require(!isEmpty(queue) && isAmortized(queue))
- if (asList(queue) == list) {
- list match {
- case Cons(x, _) => front(queue) == x
- }
- } else
- true
- } holds
-
- @induct
- def propTail(rear : List, front : List, list : List, elem : Int) : Boolean = {
- require(!isEmpty(Queue(front, rear)) && isAmortized(Queue(front, rear)))
- if (asList(Queue(front, rear)) == list) {
- list match {
- case Cons(_, xs) => asList(tail(Queue(front, rear))) == xs
- }
- } else
- true
- } // holds
-
- def enqueueAndFront(queue : AbsQueue, elem : Int) : Boolean = {
- if (isEmpty(queue))
- front(enqueue(queue, elem)) == elem
- else
- true
- } holds
-
- def enqueueDequeueThrice(queue : AbsQueue, e1 : Int, e2 : Int, e3 : Int) : Boolean = {
- if (isEmpty(queue)) {
- val q1 = enqueue(queue, e1)
- val q2 = enqueue(q1, e2)
- val q3 = enqueue(q2, e3)
- val e1prime = front(q3)
- val q4 = tail(q3)
- val e2prime = front(q4)
- val q5 = tail(q4)
- val e3prime = front(q5)
- e1 == e1prime && e2 == e2prime && e3 == e3prime
- } else
- true
- } holds
-}
diff --git a/testcases/verification/vstte10competition/SumAndMax.scala b/testcases/verification/vstte10competition/SumAndMax.scala
deleted file mode 100644
index a3fd5c3a50d6c56592dbd6d48b7bc90ac940d58f..0000000000000000000000000000000000000000
--- a/testcases/verification/vstte10competition/SumAndMax.scala
+++ /dev/null
@@ -1,46 +0,0 @@
-import leon.lang._
-import leon.annotation._
-
-object SumAndMax {
- sealed abstract class List
- case class Cons(head : Int, tail : List) extends List
- case class Nil() extends List
-
- def max(list : List) : Int = {
- require(list != Nil())
- list match {
- case Cons(x, Nil()) => x
- case Cons(x, xs) => {
- val m2 = max(xs)
- if(m2 > x) m2 else x
- }
- }
- }
-
- def sum(list : List) : Int = list match {
- case Nil() => 0
- case Cons(x, xs) => x + sum(xs)
- }
-
- def size(list : List) : Int = (list match {
- case Nil() => 0
- case Cons(_, xs) => 1 + size(xs)
- }) ensuring(_ >= 0)
-
- def allPos(list : List) : Boolean = list match {
- case Nil() => true
- case Cons(x, xs) => x >= 0 && allPos(xs)
- }
-
- def prop0(list : List) : Boolean = {
- require(list != Nil())
- !allPos(list) || max(list) >= 0
- } holds
-
- @induct
- def property(list : List) : Boolean = {
- // This precondition was given in the problem but isn't actually useful :D
- // require(allPos(list))
- sum(list) <= size(list) * (if(list == Nil()) 0 else max(list))
- } holds
-}