From e38c4579792eaeec8c0d4f0d351f4ce6e321bed2 Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Wed, 20 May 2015 17:15:55 +0200
Subject: [PATCH] clean up more tests
---
testcases/verification/Addresses.scala | 48 +++++++++----------
.../vstte10competition/SearchLinkedList.scala | 47 ------------------
testcases/verification/xlang/Add.scala | 25 ----------
...rtionSortImp.scala => InsertionSort.scala} | 0
testcases/verification/xlang/Mult.scala | 26 ----------
5 files changed, 24 insertions(+), 122 deletions(-)
delete mode 100644 testcases/verification/vstte10competition/SearchLinkedList.scala
delete mode 100644 testcases/verification/xlang/Add.scala
rename testcases/verification/xlang/{InsertionSortImp.scala => InsertionSort.scala} (100%)
delete mode 100644 testcases/verification/xlang/Mult.scala
diff --git a/testcases/verification/Addresses.scala b/testcases/verification/Addresses.scala
index bc6ad57b8..4eebe934f 100644
--- a/testcases/verification/Addresses.scala
+++ b/testcases/verification/Addresses.scala
@@ -4,36 +4,36 @@ import leon.lang._
object Addresses {
// list of integers
sealed abstract class List
- case class Cons(a:Int,b:Int,c:Int, tail:List) extends List
+ case class Cons(a: BigInt,b: BigInt,c: BigInt, tail:List) extends List
case class Nil() extends List
- def setA(l:List) : Set[Int] = l match {
- case Nil() => Set.empty[Int]
+ def setA(l:List) : Set[BigInt] = l match {
+ case Nil() => Set.empty[BigInt]
case Cons(a,b,c,l1) => Set(a) ++ setA(l1)
}
- def containsA(x:Int,l:List) : Boolean = (l match {
+ def containsA(x:BigInt,l:List) : Boolean = (l match {
case Nil() => false
case Cons(a,b,c,t) => a==x || containsA(x,t)
}) ensuring (res => res == (setA(l) contains x))
- def theseAunique1(as:Set[Int],l:List) : Boolean = l match {
+ def theseAunique1(as:Set[BigInt],l:List) : Boolean = l match {
case Nil() => true
case Cons(a,b,c,l1) =>
theseAunique1(as,l1) && !(as contains a) && (setA(l1) contains a)
}
- def theseAunique2(as:Set[Int],l:List) : Boolean = (l match {
+ def theseAunique2(as:Set[BigInt],l:List) : Boolean = (l match {
case Nil() => true
case Cons(a,b,c,l1) =>
theseAunique2(as,l1) && !(as contains a) && containsA(a,l1)
}) ensuring (res => res==theseAunique1(as,l))
- def disjoint(x:Set[Int],y:Set[Int]):Boolean = {
- (x & y) == Set.empty[Int]
+ def disjoint(x:Set[BigInt],y:Set[BigInt]):Boolean = {
+ (x & y) == Set.empty[BigInt]
}
- def uniqueAbsentAs(unique:Set[Int],absent:Set[Int],l:List) : Boolean = (l match {
+ def uniqueAbsentAs(unique:Set[BigInt],absent:Set[BigInt],l:List) : Boolean = (l match {
case Nil() => true
case Cons(a,b,c,l1) => {
!(absent contains a) &&
@@ -47,14 +47,14 @@ object Addresses {
case Cons(a,b,c,l1) => 0 <= a && 0 <= b && 0 <= c && allPos(l1)
}
- def allEq(l:List,k:Int) : Boolean = l match {
+ def allEq(l:List,k:BigInt) : Boolean = l match {
case Nil() => true
case Cons(a,b,c,l1) => c==k && allEq(l1,k)
}
- def max(x:Int,y:Int) = if (x <= y) x else y
+ def max(x:BigInt,y:BigInt) = if (x <= y) x else y
- def collectA(x:Int,l:List) : (Int,Int,List) = (l match {
+ def collectA(x:BigInt,l:List) : (BigInt,BigInt,List) = (l match {
case Nil() => (0,0,Nil())
case Cons(a,b,c,l1) if (a==x) => {
val (b2,c2,l2) = collectA(x,l1)
@@ -70,7 +70,7 @@ object Addresses {
})
/*
- def makeUniqueA(x:Int,l:List) : List = {
+ def makeUniqueA(x:BigInt,l:List) : List = {
require(allPos(l))
val (b,c,l1) = collectA(x,l)
Cons(x,b,c,l1)
@@ -81,42 +81,42 @@ object Addresses {
def isValidAB(ab:AddressBook) : Boolean = {
allEq(ab.business,0) && allEq(ab.pers,1)
}
- def setAB(l:List) : Set[(Int,Int)] = l match {
- case Nil() => Set.empty[(Int,Int)]
+ def setAB(l:List) : Set[(BigInt,BigInt)] = l match {
+ case Nil() => Set.empty[(BigInt,BigInt)]
case Cons(a,b,c,l1) => Set((a,b)) ++ setAB(l1)
}
- def removeA(x:Int,l:List) : List = (l match {
+ def removeA(x:BigInt,l:List) : List = (l match {
case Nil() => Nil()
case Cons(a,b,c,l1) =>
if (a==x) removeA(x,l1)
else Cons(a,b,c,removeA(x,l1))
}) ensuring(res => !(setA(res) contains x))
- def removeAg(x:Int,l:List,bg:Int) : List = (l match {
+ def removeAg(x:BigInt,l:List,bg:BigInt) : List = (l match {
case Nil() => Nil()
case Cons(a,b,c,l1) =>
if (a==x) removeAg(x,l1,bg)
else Cons(a,b,c,removeAg(x,l1,bg))
}) ensuring (res => !(setAB(res) contains (x,bg)))
- def removeA1(x:Int,l:List) : List = removeAg(x,l,0)
+ def removeA1(x:BigInt,l:List) : List = removeAg(x,l,0)
@induct
- def removeAspec1(x:Int,l:List,bg:Int) : Boolean = {
+ def removeAspec1(x:BigInt,l:List,bg:BigInt) : Boolean = {
removeAg(x,l,bg) == removeA(x,l)
} holds
- def removeAspec2(x:Int,l:List,k:Int) : Boolean = {
+ def removeAspec2(x:BigInt,l:List,k:BigInt) : Boolean = {
require(allEq(l,k))
allEq(removeA(x,l),k)
} holds
- def updateABC(a:Int,b:Int,c:Int,l:List) : List = ({
+ def updateABC(a:BigInt,b:BigInt,c:BigInt,l:List) : List = ({
Cons(a,b,c,removeA(a,l))
}) ensuring (res => setAB(res) contains (a,b))
- def lookupA(x:Int,l:List) : (Int,Int,Int) = {
+ def lookupA(x:BigInt,l:List) : (BigInt,BigInt,BigInt) = {
require(setA(l) contains x)
l match {
case Cons(a,b,c,l1) => {
@@ -124,12 +124,12 @@ object Addresses {
else lookupA(x,l1)
}
}
- } ensuring((res:(Int,Int,Int)) => {
+ } ensuring((res:(BigInt,BigInt,BigInt)) => {
val (a,b,c) = res
setAB(l) contains (a,b)
})
- def makePers(ab:AddressBook, x:Int) : AddressBook = {
+ def makePers(ab:AddressBook, x:BigInt) : AddressBook = {
require(isValidAB(ab) && (setA(ab.business) contains x))
val (a,b,c) = lookupA(x,ab.business)
val business1 = removeA(x, ab.business)
diff --git a/testcases/verification/vstte10competition/SearchLinkedList.scala b/testcases/verification/vstte10competition/SearchLinkedList.scala
deleted file mode 100644
index f85d51421..000000000
--- a/testcases/verification/vstte10competition/SearchLinkedList.scala
+++ /dev/null
@@ -1,47 +0,0 @@
-import leon.lang._
-import leon.annotation._
-
-object SearchLinkedList {
- sealed abstract class List
- case class Cons(head : Int, tail : List) extends List
- case class Nil() extends List
-
- def size(list : List) : Int = (list match {
- case Nil() => 0
- case Cons(_, xs) => 1 + size(xs)
- }) ensuring(_ >= 0)
-
- def contains(list : List, elem : Int) : Boolean = (list match {
- case Nil() => false
- case Cons(x, xs) => x == elem || contains(xs, elem)
- })
-
- def firstZero(list : List) : Int = (list match {
- case Nil() => 0
- case Cons(x, xs) => if (x == 0) 0 else firstZero(xs) + 1
- }) ensuring (res =>
- res >= 0 && (if (contains(list, 0)) {
- firstZeroAtPos(list, res)
- } else {
- res == size(list)
- }))
-
- def firstZeroAtPos(list : List, pos : Int) : Boolean = {
- list match {
- case Nil() => false
- case Cons(x, xs) => if (pos == 0) x == 0 else x != 0 && firstZeroAtPos(xs, pos - 1)
- }
- }
-
- def goal(list : List, i : Int) : Boolean = {
- if(firstZero(list) == i) {
- if(contains(list, 0)) {
- firstZeroAtPos(list, i)
- } else {
- i == size(list)
- }
- } else {
- true
- }
- } holds
-}
diff --git a/testcases/verification/xlang/Add.scala b/testcases/verification/xlang/Add.scala
deleted file mode 100644
index a23ad0595..000000000
--- a/testcases/verification/xlang/Add.scala
+++ /dev/null
@@ -1,25 +0,0 @@
-import leon.lang._
-
-/* VSTTE 2008 - Dafny paper */
-
-object Add {
-
- 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)
-
-}
diff --git a/testcases/verification/xlang/InsertionSortImp.scala b/testcases/verification/xlang/InsertionSort.scala
similarity index 100%
rename from testcases/verification/xlang/InsertionSortImp.scala
rename to testcases/verification/xlang/InsertionSort.scala
diff --git a/testcases/verification/xlang/Mult.scala b/testcases/verification/xlang/Mult.scala
deleted file mode 100644
index cdacdaa61..000000000
--- a/testcases/verification/xlang/Mult.scala
+++ /dev/null
@@ -1,26 +0,0 @@
-import leon.lang._
-
-/* VSTTE 2008 - Dafny paper */
-
-object Mult {
-
- 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)
-
-}
-
--
GitLab