From 1c8958e421f7c86f43f93dd91d522879cd08feaa Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 20 May 2015 18:17:05 +0200
Subject: [PATCH] reorganize verification testcases
---
testcases/verification/Errors.scala | 6 -
.../verification/MutuallyRecursive.scala | 28 ----
.../{ => algorithms}/FiniteSort.scala | 0
.../{ => algorithms}/SecondsToTime.scala | 0
.../Sorting.scala | 0
.../{ => list-algorithms}/SumAndMax.scala | 0
.../TwoSizeFunctions.scala | 0
.../verification/{ => math}/Fibonacci.scala | 19 +++
.../verification/{ => math}/Naturals.scala | 0
testcases/verification/{ => math}/Prime.scala | 0
.../{ => math}/PropositionalLogic.scala | 0
testcases/verification/xlang/Arithmetic.scala | 18 +--
.../master-thesis-regis/Arithmetic.scala | 84 ----------
.../master-thesis-regis/ListOperations.scala | 146 ------------------
14 files changed, 28 insertions(+), 273 deletions(-)
delete mode 100644 testcases/verification/Errors.scala
delete mode 100644 testcases/verification/MutuallyRecursive.scala
rename testcases/verification/{ => algorithms}/FiniteSort.scala (100%)
rename testcases/verification/{ => algorithms}/SecondsToTime.scala (100%)
rename testcases/verification/{algorithms => list-algorithms}/Sorting.scala (100%)
rename testcases/verification/{ => list-algorithms}/SumAndMax.scala (100%)
rename testcases/verification/{ => list-algorithms}/TwoSizeFunctions.scala (100%)
rename testcases/verification/{ => math}/Fibonacci.scala (53%)
rename testcases/verification/{ => math}/Naturals.scala (100%)
rename testcases/verification/{ => math}/Prime.scala (100%)
rename testcases/verification/{ => math}/PropositionalLogic.scala (100%)
delete mode 100644 testcases/verification/xlang/master-thesis-regis/Arithmetic.scala
delete mode 100644 testcases/verification/xlang/master-thesis-regis/ListOperations.scala
diff --git a/testcases/verification/Errors.scala b/testcases/verification/Errors.scala
deleted file mode 100644
index 0a975695d..000000000
--- a/testcases/verification/Errors.scala
+++ /dev/null
@@ -1,6 +0,0 @@
-import leon.lang._
-
-object Errors {
- def a(a: Int): Int = error[Int]("This is an error")
-}
-
diff --git a/testcases/verification/MutuallyRecursive.scala b/testcases/verification/MutuallyRecursive.scala
deleted file mode 100644
index b39482773..000000000
--- a/testcases/verification/MutuallyRecursive.scala
+++ /dev/null
@@ -1,28 +0,0 @@
-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)
- }
-}
diff --git a/testcases/verification/FiniteSort.scala b/testcases/verification/algorithms/FiniteSort.scala
similarity index 100%
rename from testcases/verification/FiniteSort.scala
rename to testcases/verification/algorithms/FiniteSort.scala
diff --git a/testcases/verification/SecondsToTime.scala b/testcases/verification/algorithms/SecondsToTime.scala
similarity index 100%
rename from testcases/verification/SecondsToTime.scala
rename to testcases/verification/algorithms/SecondsToTime.scala
diff --git a/testcases/verification/algorithms/Sorting.scala b/testcases/verification/list-algorithms/Sorting.scala
similarity index 100%
rename from testcases/verification/algorithms/Sorting.scala
rename to testcases/verification/list-algorithms/Sorting.scala
diff --git a/testcases/verification/SumAndMax.scala b/testcases/verification/list-algorithms/SumAndMax.scala
similarity index 100%
rename from testcases/verification/SumAndMax.scala
rename to testcases/verification/list-algorithms/SumAndMax.scala
diff --git a/testcases/verification/TwoSizeFunctions.scala b/testcases/verification/list-algorithms/TwoSizeFunctions.scala
similarity index 100%
rename from testcases/verification/TwoSizeFunctions.scala
rename to testcases/verification/list-algorithms/TwoSizeFunctions.scala
diff --git a/testcases/verification/Fibonacci.scala b/testcases/verification/math/Fibonacci.scala
similarity index 53%
rename from testcases/verification/Fibonacci.scala
rename to testcases/verification/math/Fibonacci.scala
index 7c37e7ff2..df2b731c5 100644
--- a/testcases/verification/Fibonacci.scala
+++ b/testcases/verification/math/Fibonacci.scala
@@ -1,4 +1,5 @@
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))
+
}
diff --git a/testcases/verification/Naturals.scala b/testcases/verification/math/Naturals.scala
similarity index 100%
rename from testcases/verification/Naturals.scala
rename to testcases/verification/math/Naturals.scala
diff --git a/testcases/verification/Prime.scala b/testcases/verification/math/Prime.scala
similarity index 100%
rename from testcases/verification/Prime.scala
rename to testcases/verification/math/Prime.scala
diff --git a/testcases/verification/PropositionalLogic.scala b/testcases/verification/math/PropositionalLogic.scala
similarity index 100%
rename from testcases/verification/PropositionalLogic.scala
rename to testcases/verification/math/PropositionalLogic.scala
diff --git a/testcases/verification/xlang/Arithmetic.scala b/testcases/verification/xlang/Arithmetic.scala
index f3f10b892..99efb8222 100644
--- a/testcases/verification/xlang/Arithmetic.scala
+++ b/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
diff --git a/testcases/verification/xlang/master-thesis-regis/Arithmetic.scala b/testcases/verification/xlang/master-thesis-regis/Arithmetic.scala
deleted file mode 100644
index f3f10b892..000000000
--- a/testcases/verification/xlang/master-thesis-regis/Arithmetic.scala
+++ /dev/null
@@ -1,84 +0,0 @@
-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)
-
-}
diff --git a/testcases/verification/xlang/master-thesis-regis/ListOperations.scala b/testcases/verification/xlang/master-thesis-regis/ListOperations.scala
deleted file mode 100644
index 5f2844fa0..000000000
--- a/testcases/verification/xlang/master-thesis-regis/ListOperations.scala
+++ /dev/null
@@ -1,146 +0,0 @@
-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)
-
-}
--
GitLab