From fd9242d7caefdda6921d664ff9bb804ce4676e0b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Sun, 17 Jun 2012 04:32:08 +0200
Subject: [PATCH] testcase folder for regist master thesis results
---
.../master-thesis-regis/Arithmetic.scala | 73 ++++++
.../master-thesis-regis/ArrayOperations.scala | 207 ++++++++++++++++++
.../master-thesis-regis/Constraints.scala | 26 +++
.../master-thesis-regis/ListOperations.scala | 146 ++++++++++++
4 files changed, 452 insertions(+)
create mode 100644 testcases/master-thesis-regis/Arithmetic.scala
create mode 100644 testcases/master-thesis-regis/ArrayOperations.scala
create mode 100644 testcases/master-thesis-regis/Constraints.scala
create mode 100644 testcases/master-thesis-regis/ListOperations.scala
diff --git a/testcases/master-thesis-regis/Arithmetic.scala b/testcases/master-thesis-regis/Arithmetic.scala
new file mode 100644
index 000000000..9173132e0
--- /dev/null
+++ b/testcases/master-thesis-regis/Arithmetic.scala
@@ -0,0 +1,73 @@
+import leon.Utils._
+
+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)
+
+}
diff --git a/testcases/master-thesis-regis/ArrayOperations.scala b/testcases/master-thesis-regis/ArrayOperations.scala
new file mode 100644
index 000000000..91eb371fa
--- /dev/null
+++ b/testcases/master-thesis-regis/ArrayOperations.scala
@@ -0,0 +1,207 @@
+import leon.Utils._
+
+object ArrayOperations {
+
+ /* VSTTE 2008 - Dafny paper */
+ def binarySearch(a: Array[Int], key: Int): Int = ({
+ require(a.length > 0 && sorted(a, 0, a.length - 1))
+ var low = 0
+ var high = a.length - 1
+ var res = -1
+
+ (while(low <= high && res == -1) {
+ val i = (high + low) / 2
+ val v = a(i)
+
+ if(v == key)
+ res = i
+
+ if(v > key)
+ high = i - 1
+ else if(v < key)
+ low = i + 1
+ }) invariant(
+ res >= -1 &&
+ res < a.length &&
+ 0 <= low &&
+ low <= high + 1 &&
+ high >= -1 &&
+ high < a.length &&
+ (if (res >= 0)
+ a(res) == key else
+ (!occurs(a, 0, low, key) && !occurs(a, high + 1, a.length, key))
+ )
+ )
+ res
+ }) ensuring(res =>
+ res >= -1 &&
+ res < a.length &&
+ (if(res >= 0) a(res) == key else !occurs(a, 0, a.length, key)))
+
+
+ def occurs(a: Array[Int], from: Int, to: Int, key: Int): Boolean = {
+ require(a.length >= 0 && to <= a.length && from >= 0)
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= to)
+ false
+ else {
+ if(a(i) == key) true else rec(i+1)
+ }
+ }
+ if(from >= to)
+ false
+ else
+ rec(from)
+ }
+
+ def sorted(a: Array[Int], l: Int, u: Int): Boolean = {
+ require(a.length >= 0 && l >= 0 && u < a.length && l <= u)
+ var k = l
+ var isSorted = true
+ (while(k < u) {
+ if(a(k) > a(k+1))
+ isSorted = false
+ k = k + 1
+ }) invariant(k <= u && k >= l)
+ isSorted
+ }
+
+ /* The calculus of Computation textbook */
+ def bubbleSort(a: Array[Int]): Array[Int] = ({
+ require(a.length >= 1)
+ var i = a.length - 1
+ var j = 0
+ val sa = a.clone
+ (while(i > 0) {
+ j = 0
+ (while(j < i) {
+ if(sa(j) > sa(j+1)) {
+ val tmp = sa(j)
+ sa(j) = sa(j+1)
+ sa(j+1) = tmp
+ }
+ j = j + 1
+ }) invariant(
+ j >= 0 &&
+ j <= i &&
+ i < sa.length &&
+ sa.length >= 0 &&
+ partitioned(sa, 0, i, i+1, sa.length-1) &&
+ sorted(sa, i, sa.length-1) &&
+ partitioned(sa, 0, j-1, j, j)
+ )
+ i = i - 1
+ }) invariant(
+ i >= 0 &&
+ i < sa.length &&
+ sa.length >= 0 &&
+ partitioned(sa, 0, i, i+1, sa.length-1) &&
+ sorted(sa, i, sa.length-1)
+ )
+ sa
+ }) ensuring(res => sorted(res, 0, a.length-1))
+
+ def partitioned(a: Array[Int], l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+ require(a.length >= 0 && l1 >= 0 && u1 < l2 && u2 < a.length)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ var i = l1
+ var j = l2
+ var isPartitionned = true
+ (while(i <= u1) {
+ j = l2
+ (while(j <= u2) {
+ if(a(i) > a(j))
+ isPartitionned = false
+ j = j + 1
+ }) invariant(j >= l2 && i <= u1)
+ i = i + 1
+ }) invariant(i >= l1)
+ isPartitionned
+ }
+ }
+
+ /* The calculus of Computation textbook */
+ def linearSearch(a: Array[Int], c: Int): Boolean = ({
+ require(a.length >= 0)
+ var i = 0
+ var found = false
+ (while(i < a.length) {
+ if(a(i) == c)
+ found = true
+ i = i + 1
+ }) invariant(
+ i <= a.length &&
+ i >= 0 &&
+ (if(found) contains(a, i, c) else !contains(a, i, c))
+ )
+ found
+ }) ensuring(res => if(res) contains(a, a.length, c) else !contains(a, a.length, c))
+
+ def contains(a: Array[Int], size: Int, c: Int): Boolean = {
+ require(a.length >= 0 && size >= 0 && size <= a.length)
+ content(a, size).contains(c)
+ }
+
+ def content(a: Array[Int], size: Int): Set[Int] = {
+ require(a.length >= 0 && size >= 0 && size <= a.length)
+ var set = Set.empty[Int]
+ var i = 0
+ (while(i < size) {
+ set = set ++ Set(a(i))
+ i = i + 1
+ }) invariant(i >= 0 && i <= size)
+ set
+ }
+
+ def abs(tab: Array[Int]): Array[Int] = ({
+ require(tab.length >= 0)
+ var k = 0
+ val tabres = Array.fill(tab.length)(0)
+ (while(k < tab.length) {
+ if(tab(k) < 0)
+ tabres(k) = -tab(k)
+ else
+ tabres(k) = tab(k)
+ k = k + 1
+ }) invariant(
+ tabres.length == tab.length &&
+ k >= 0 && k <= tab.length &&
+ isPositive(tabres, k))
+ tabres
+ }) ensuring(res => isPositive(res, res.length))
+
+ def isPositive(a: Array[Int], size: Int): Boolean = {
+ require(a.length >= 0 && size <= a.length)
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= size)
+ true
+ else {
+ if(a(i) < 0)
+ false
+ else
+ rec(i+1)
+ }
+ }
+ rec(0)
+ }
+
+ /* VSTTE 2010 challenge 1 */
+ def maxSum(a: Array[Int]): (Int, Int) = ({
+ require(a.length >= 0 && isPositive(a, a.length))
+ var sum = 0
+ var max = 0
+ var i = 0
+ (while(i < a.length) {
+ if(max < a(i))
+ max = a(i)
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant (sum <= i * max && i >= 0 && i <= a.length)
+ (sum, max)
+ }) ensuring(res => res._1 <= a.length * res._2)
+
+}
diff --git a/testcases/master-thesis-regis/Constraints.scala b/testcases/master-thesis-regis/Constraints.scala
new file mode 100644
index 000000000..6fdd96392
--- /dev/null
+++ b/testcases/master-thesis-regis/Constraints.scala
@@ -0,0 +1,26 @@
+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 property(lst: MyList): Boolean = (size(toList(toSet(lst))) <= size(lst)) holds
+
+}
diff --git a/testcases/master-thesis-regis/ListOperations.scala b/testcases/master-thesis-regis/ListOperations.scala
new file mode 100644
index 000000000..4bb59c264
--- /dev/null
+++ b/testcases/master-thesis-regis/ListOperations.scala
@@ -0,0 +1,146 @@
+import leon.Utils._
+import leon.Annotations._
+
+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