reorganize verification testcases

testcases/verification/Errors.scala

-import leon.lang._
-
-object Errors {
-  def a(a: Int): Int = error[Int]("This is an error")
-}
-

testcases/verification/MutuallyRecursive.scala

-import scala.collection.immutable.Set
-import leon.lang._
-import leon.annotation._
-
-object MutuallyRecursive {
-    def f(n : Int) : Int = {
-        if(n <= 0){
-            1
-        }
-        else{
-            f(n-1) + g(n-1)
-        }
-    }
-
-    def g(n : Int) : Int = {
-        if(n <= 0)
-            1
-        else
-            f(n-1) 
-    }ensuring(_ == fib(n + 1))
-
-    def fib(n : Int ) : Int = {
-                    if(n <= 2)
-                                    1
-                    else
-                                    fib(n-1) + fib (n-2)
-    }
-}

testcases/verification/Fibonacci.scala → testcases/verification/math/Fibonacci.scala

 object Fibonacci {
+
   def fib(x: BigInt) : BigInt = {
     require(x >= 0)
     if(x < 2) {
@@ -12,4 +13,22 @@ object Fibonacci {
   def check() : Boolean = {
     fib(5) == 5
   } ensuring(_ == true)
+
+
+  def f(n : BigInt) : BigInt = {
+    require(n >= 0)
+    if(n <= 0)
+      1
+    else
+      f(n-1) + g(n-1)
+  }
+
+  def g(n : BigInt) : BigInt = {
+    require(n >= 0)
+    if(n <= 0)
+      1
+    else
+      f(n-1) 
+  } ensuring(_ == fib(n + 1))
+
 }

testcases/verification/xlang/Arithmetic.scala

@@ -3,8 +3,8 @@ import leon.lang._
 object Arithmetic {
 
   /* VSTTE 2008 - Dafny paper */
-  def mult(x : Int, y : Int): Int = ({
-    var r = 0
+  def mult(x : BigInt, y : BigInt): BigInt = ({
+    var r: BigInt = 0
     if(y < 0) {
       var n = y
       (while(n != 0) {
@@ -22,7 +22,7 @@ object Arithmetic {
   }) ensuring(_ == x*y)
 
   /* VSTTE 2008 - Dafny paper */
-  def add(x : Int, y : Int): Int = ({
+  def add(x : BigInt, y : BigInt): BigInt = ({
     var r = x
     if(y < 0) {
       var n = y
@@ -41,7 +41,7 @@ object Arithmetic {
   }) ensuring(_ == x+y)
 
   /* VSTTE 2008 - Dafny paper */
-  def addBuggy(x : Int, y : Int): Int = ({
+  def addBuggy(x : BigInt, y : BigInt): BigInt = ({
     var r = x
     if(y < 0) {
       var n = y
@@ -59,10 +59,10 @@ object Arithmetic {
     r
   }) ensuring(_ == x+y)
 
-  def sum(n: Int): Int = {
+  def sum(n: BigInt): BigInt = {
     require(n >= 0)
-    var r = 0
-    var i = 0
+    var r: BigInt = 0
+    var i: BigInt = 0
     (while(i < n) {
       i = i + 1
       r = r + i
@@ -70,10 +70,10 @@ object Arithmetic {
     r
   } ensuring(_ >= n)
 
-  def divide(x: Int, y: Int): (Int, Int) = {
+  def divide(x: BigInt, y: BigInt): (BigInt, BigInt) = {
     require(x >= 0 && y > 0)
     var r = x
-    var q = 0
+    var q = BigInt(0)
     (while(r >= y) {
       r = r - y
       q = q + 1

testcases/verification/xlang/master-thesis-regis/Arithmetic.scala

-import leon.lang._
-
-object Arithmetic {
-
-  /* VSTTE 2008 - Dafny paper */
-  def mult(x : Int, y : Int): Int = ({
-    var r = 0
-    if(y < 0) {
-      var n = y
-      (while(n != 0) {
-        r = r - x
-        n = n + 1
-      }) invariant(r == x * (y - n) && 0 <= -n)
-    } else {
-      var n = y
-      (while(n != 0) {
-        r = r + x
-        n = n - 1
-      }) invariant(r == x * (y - n) && 0 <= n)
-    }
-    r
-  }) ensuring(_ == x*y)
-
-  /* VSTTE 2008 - Dafny paper */
-  def add(x : Int, y : Int): Int = ({
-    var r = x
-    if(y < 0) {
-      var n = y
-      (while(n != 0) {
-        r = r - 1
-        n = n + 1
-      }) invariant(r == x + y - n && 0 <= -n)
-    } else {
-      var n = y
-      (while(n != 0) {
-        r = r + 1
-        n = n - 1
-      }) invariant(r == x + y - n && 0 <= n)
-    }
-    r
-  }) ensuring(_ == x+y)
-
-  /* VSTTE 2008 - Dafny paper */
-  def addBuggy(x : Int, y : Int): Int = ({
-    var r = x
-    if(y < 0) {
-      var n = y
-      (while(n != 0) {
-        r = r + 1
-        n = n + 1
-      }) invariant(r == x + y - n && 0 <= -n)
-    } else {
-      var n = y
-      (while(n != 0) {
-        r = r + 1
-        n = n - 1
-      }) invariant(r == x + y - n && 0 <= n)
-    }
-    r
-  }) ensuring(_ == x+y)
-
-  def sum(n: Int): Int = {
-    require(n >= 0)
-    var r = 0
-    var i = 0
-    (while(i < n) {
-      i = i + 1
-      r = r + i
-    }) invariant(r >= i && i >= 0 && r >= 0)
-    r
-  } ensuring(_ >= n)
-
-  def divide(x: Int, y: Int): (Int, Int) = {
-    require(x >= 0 && y > 0)
-    var r = x
-    var q = 0
-    (while(r >= y) {
-      r = r - y
-      q = q + 1
-    }) invariant(x == y*q + r && r >= 0)
-    (q, r)
-  } ensuring(res => x == y*res._1 + res._2 && res._2 >= 0 && res._2 < y)
-
-}

testcases/verification/xlang/master-thesis-regis/ListOperations.scala

-import leon.lang._
-import leon.annotation._
-
-object ListOperations {
-
-  sealed abstract class List
-  case class Cons(head: Int, tail: List) extends List
-  case class Nil() extends List
-
-  sealed abstract class IPList
-  case class IPCons(head: (Int, Int), tail: IPList) extends IPList
-  case class IPNil() extends IPList
-
-  def content(l: List) : Set[Int] = l match {
-    case Nil() => Set.empty[Int]
-    case Cons(x, xs) => Set(x) ++ content(xs)
-  }
-
-  def iplContent(l: IPList) : Set[(Int, Int)] = l match {
-    case IPNil() => Set.empty[(Int, Int)]
-    case IPCons(x, xs) => Set(x) ++ iplContent(xs)
-  }
-
-  def size(l: List) : Int = {
-    var r = 0
-    var l2 = l
-    (while(!l2.isInstanceOf[Nil]) {
-      val Cons(_, tail) = l2
-      l2 = tail
-      r = r+1
-    }) invariant(r >= 0)
-    r
-  } ensuring(res => res >= 0)
-
-  def sizeBuggy(l: List) : Int = {
-    var r = -1
-    var l2 = l
-    (while(!l2.isInstanceOf[Nil]) {
-      val Cons(_, tail) = l2
-      l2 = tail
-      r = r+1
-    }) invariant(r >= 0)
-    r
-  } ensuring(res => res >= 0)
-
-  def sizeFun(l: List) : Int = l match {
-    case Nil() => 0
-    case Cons(_, t) => 1 + sizeFun(t)
-  } 
-
-  def iplSizeFun(l: IPList) : Int = l match {
-    case IPNil() => 0
-    case IPCons(_, t) => 1 + iplSizeFun(t)
-  }
-
-  def iplSize(l: IPList) : Int = {
-    var r = 0
-    var l2 = l
-    (while(!l2.isInstanceOf[IPNil]) {
-      val IPCons(_, tail) = l2
-      l2 = tail
-      r = r+1
-    }) invariant(r >= 0)
-    r
-  } ensuring(_ >= 0)
-
-  def sizeImpEqFun(l: List): Boolean = (size(l) == sizeFun(l)) ensuring(_ == true)
-
-  def zip(l1: List, l2: List) : IPList = ({
-    require(sizeFun(l1) == sizeFun(l2))
-    var  r: IPList = IPNil()
-    var ll1: List = l1
-    var ll2 = l2
-
-    (while(!ll1.isInstanceOf[Nil]) {
-      val Cons(l1head, l1tail) = ll1
-      val Cons(l2head, l2tail) = if(!ll2.isInstanceOf[Nil]) ll2 else Cons(0, Nil())
-      r = IPCons((l1head, l2head), r)
-      ll1 = l1tail
-      ll2 = l2tail
-    }) invariant(iplSizeFun(r) + sizeFun(ll1) == sizeFun(l1))
-
-    iplReverse(r)
-  }) ensuring(res => iplSizeFun(res) == sizeFun(l1))
-
-  def iplReverse(l: IPList): IPList = {
-    var r: IPList = IPNil()
-    var l2: IPList = l
-
-    (while(!l2.isInstanceOf[IPNil]) {
-      val IPCons(head, tail) = l2
-      l2 = tail
-      r = IPCons(head, r)
-    }) invariant(iplContent(r) ++ iplContent(l2) == iplContent(l) && iplSizeFun(r) + iplSizeFun(l2) == iplSizeFun(l))
-
-    r
-  } ensuring(res => iplContent(res) == iplContent(l) && iplSizeFun(res) == iplSizeFun(l))
-
-  def reverse(l: List): List = {
-    var r: List = Nil()
-    var l2: List = l
-
-    (while(!l2.isInstanceOf[Nil]) {
-      val Cons(head, tail) = l2
-      l2 = tail
-      r = Cons(head, r)
-    }) invariant(content(r) ++ content(l2) == content(l) && sizeFun(r) + sizeFun(l2) == sizeFun(l))
-
-    r
-  } ensuring(res => content(res) == content(l) && sizeFun(res) == sizeFun(l))
-
-  def listEqReverse(l: List): Boolean = {
-    l == reverse(l)
-  } ensuring(_ == true)
-
-  def append(l1 : List, l2 : List) : List = {
-    var r: List = l2
-    var tmp: List = reverse(l1)
-
-    (while(!tmp.isInstanceOf[Nil]) {
-      val Cons(head, tail) = tmp
-      tmp = tail
-      r = Cons(head, r)
-    }) invariant(content(r) ++ content(tmp) == content(l1) ++ content(l2))
-
-    r
-  } ensuring(content(_) == content(l1) ++ content(l2))
-
-  def appendBuggy(l1 : List, l2 : List) : List = {
-    var r: List = l2
-    var tmp: List = l1
-
-    while(!tmp.isInstanceOf[Nil]) {
-      val Cons(head, tail) = tmp
-      tmp = tail
-      r = Cons(head, r)
-    }
-
-    r
-  }
-
-  def appendEqAppendBuggy(l1: List, l2: List): Boolean = {
-    append(l1, l2) == appendBuggy(l1, l2)
-  } ensuring(_ == true)
-
-}