diff --git a/testcases/BinaryTreeImp.scala b/testcases/BinaryTreeImp.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3005d199122e373e29cdc3ce19f932be29eb4c3d
--- /dev/null
+++ b/testcases/BinaryTreeImp.scala
@@ -0,0 +1,101 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object BinaryTree {
+
+ sealed abstract class Tree
+ case class Leaf() extends Tree
+ case class Node(left: Tree, value: Int, right: Tree) extends Tree
+
+ sealed abstract class OptionInt
+ case class Some(v : Int) extends OptionInt
+ case class None() extends OptionInt
+
+ def content(t: Tree) : Set[Int] = t match {
+ case Leaf() => Set.empty
+ case Node(l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : Int = (t match {
+ case Leaf() => 0
+ case Node(l, v, r) => size(l) + 1 + size(r)
+ }) ensuring(_ >= 0)
+
+ def binaryTreeProp(t: Tree): Boolean = t match {
+ case Leaf() => true
+ case Node(left, value, right) => {
+ val b1 = left match {
+ case Leaf() => true
+ case Node(a,b,c) => value >= treeMax(Node(a,b,c))
+ }
+ val b2 = right match {
+ case Leaf() => true
+ case Node(a,b,c) => value <= treeMin(Node(a,b,c))
+ }
+ binaryTreeProp(left) && binaryTreeProp(right) && b1 && b2
+ }
+ }
+
+ def treeMin(tree: Node): Int = {
+ require(binaryTreeProp(tree))
+ tree match {
+ case Node(left, value, _) => left match {
+ case Leaf() => value
+ case Node(l, v, r) => treeMin(Node(l, v, r))
+ }
+ }
+ } ensuring(content(tree).contains(_))
+
+ //def treeMin(tree: Node): Int = {
+ // require(binaryTreeProp(tree))
+ // val Node(left, value, _) = tree
+ // var res = value
+ // var tmpLeft = left
+ // (while(!tmpLeft.isInstanceOf[Leaf]) {
+ // val Node(left, value, _) = tmpLeft
+ // res = value
+ // tmpLeft = left
+ // }) invariant(content(tmpLeft).contains(res))
+ // res
+ //} ensuring(content(tree).contains(_))
+
+ def treeMax(tree: Node): Int = {
+ require(binaryTreeProp(tree))
+ tree match {
+ case Node(_, v, right) => right match {
+ case Leaf() => v
+ case Node(l, v, r) => treeMax(Node(l, v, r))
+ }
+ }
+ } ensuring(content(tree).contains(_))
+
+
+ def search(t: Tree, x: Int): Boolean = {
+ require(binaryTreeProp(t))
+ t match {
+ case Leaf() => false
+ case Node(left, value, right) =>
+ if(value == x) true
+ else if(value < x) search(right, x)
+ else search(left, x)
+ }
+ } ensuring(res => res == content(t).contains(x))
+
+ def searchImp(t: Tree, x: Int): Boolean = {
+ require(binaryTreeProp(t))
+ var res = false
+ var t2: Tree = t
+ (while(!t2.isInstanceOf[Leaf]) {
+ val Node(left, value, right) = t2
+ if(value == x)
+ res = true
+ else if(value < x)
+ t2 = right
+ else
+ t2 = left
+ })
+ res
+ } ensuring(res => res == content(t).contains(x))
+
+}
diff --git a/testcases/InsertionSortImp.scala b/testcases/InsertionSortImp.scala
new file mode 100644
index 0000000000000000000000000000000000000000..266905b26329d3cb3c4bd09d45a9356f805c6005
--- /dev/null
+++ b/testcases/InsertionSortImp.scala
@@ -0,0 +1,107 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object InsertionSort {
+ sealed abstract class List
+ case class Cons(head:Int,tail:List) extends List
+ case class Nil() extends List
+
+ sealed abstract class OptInt
+ case class Some(value: Int) extends OptInt
+ case class None() extends OptInt
+
+ def size(l : List) : Int = (l match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def contents(l: List): Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def min(l : List) : OptInt = l match {
+ case Nil() => None()
+ case Cons(x, xs) => min(xs) match {
+ case None() => Some(x)
+ case Some(x2) => if(x < x2) Some(x) else Some(x2)
+ }
+ }
+
+ def isSorted(l: List): Boolean = l match {
+ case Nil() => true
+ case Cons(x, Nil()) => true
+ case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
+ }
+ def isReversedSorted(l: List): Boolean = l match {
+ case Nil() => true
+ case Cons(x, Nil()) => true
+ case Cons(x, Cons(y, ys)) => x >= y && isReversedSorted(Cons(y, ys))
+ }
+
+ 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(contents(r) ++ contents(l2) == contents(l) && size(r) + size(l2) == size(l) &&
+ (if(isSorted(l)) isReversedSorted(r) else true))
+
+ r
+ } ensuring(res => contents(res) == contents(l) && size(res) == size(l) &&
+ (if(isSorted(l)) isReversedSorted(res) else true))
+
+ def reverseSortedSpec(l: List): List = {
+ require(isSorted(l))
+ reverse(l)
+ } ensuring(res => isReversedSorted(res))
+
+ /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+ * the expected content and size */
+ def sortedIns(e: Int, l: List): List = {
+ require(isSorted(l))
+ l match {
+ case Nil() => Cons(e,Nil())
+ case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ && isSorted(res)
+ && size(res) == size(l) + 1
+ )
+
+ /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+ * the expected content and size */
+ def buggySortedIns(e: Int, l: List): List = {
+ // require(isSorted(l))
+ l match {
+ case Nil() => Cons(e,Nil())
+ case Cons(x,xs) => if (x <= e) Cons(x,buggySortedIns(e, xs)) else Cons(e, l)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ && isSorted(res)
+ && size(res) == size(l) + 1
+ )
+
+ /* Insertion sort yields a sorted list of same size and content as the input
+ * list */
+ def sort(l: List): List = (l match {
+ case Nil() => Nil()
+ case Cons(x,xs) => sortedIns(x, sort(xs))
+ }) ensuring(res => contents(res) == contents(l)
+ && isSorted(res)
+ && size(res) == size(l)
+ )
+
+ def main(args: Array[String]): Unit = {
+ val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
+
+ println(ls)
+ println(sort(ls))
+ }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/QuickSortImp.scala b/testcases/QuickSortImp.scala
new file mode 100644
index 0000000000000000000000000000000000000000..dd8e34b32c8262ee804e072872796050ed03d28a
--- /dev/null
+++ b/testcases/QuickSortImp.scala
@@ -0,0 +1,79 @@
+import leon.Utils._
+
+object QuickSortImp {
+
+
+ def quicksort(array: Array[Int]): Array[Int] = {
+ require(array.length > 0)
+
+ def quicksort0(array: Array[Int], left: Int, right: Int): Array[Int] = {
+ require(array.length > 0 && left >= 0 && right < array.length)
+
+ def partition(array: Array[Int], left: Int, right: Int, pivotIndex: Int): (Array[Int], Int) = {
+ require(array.length > 0 && left >= 0 && left < right && right < array.length &&
+ pivotIndex >= left && pivotIndex <= right)
+ val pivotValue = array(pivotIndex)
+ val sa: Array[Int] = array.clone
+ val tmp = array(pivotIndex)
+ sa(pivotIndex) = sa(right)
+ sa(right) = tmp
+ var storeIndex = left
+ var i = left
+ (while(i < right) {
+ if(sa(i) < pivotValue) {
+ val tmp = sa(i)
+ sa(i) = sa(storeIndex)
+ sa(storeIndex) = tmp
+ storeIndex = storeIndex + 1
+ }
+ i += 1
+ }) invariant(
+ sa.length >= 0 && right < sa.length && sa.length == array.length &&
+ storeIndex >= left &&
+ i >= left &&
+ storeIndex <= i &&
+ storeIndex <= right &&
+ i <= right
+ )
+
+ val tmp2 = array(storeIndex)
+ //sa(storeIndex) = sa(right)
+ sa(pivotIndex) = sa(right)
+ sa(right) = tmp2
+
+ (sa, storeIndex)
+ } ensuring(res => res._2 >= left && res._2 <= right &&
+ res._1.length == array.length && res._1.length >= 0)
+
+
+ // If the list has 2 or more items
+ if(left < right) {
+ val pivotIndex = left
+
+ val (as1, pivotNewIndex) = partition(array, left, right, pivotIndex)
+
+ // Recursively sort elements smaller than the pivot
+ val as2 = quicksort0(as1, left, pivotNewIndex - 1)
+
+ // Recursively sort elements at least as big as the pivot
+ quicksort0(as2, pivotNewIndex + 1, right)
+ } else array
+ } ensuring(res => res.length == array.length && res.length >= 0)
+
+ quicksort0(array, 0, array.length-1)
+ } ensuring(res => sorted(res, 0, res.length-1))
+
+ 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
+ }
+
+
+}
diff --git a/testcases/scala-workshop/AmortizedQueue.scala b/testcases/scala-workshop/AmortizedQueue.scala
new file mode 100644
index 0000000000000000000000000000000000000000..dd5a75f89735805a74612665e487aa8fa99ec397
--- /dev/null
+++ b/testcases/scala-workshop/AmortizedQueue.scala
@@ -0,0 +1,124 @@
+import scala.collection.immutable.Set
+import leon.Utils._
+import leon.Annotations._
+
+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/scala-workshop/AmortizedQueueImp.scala b/testcases/scala-workshop/AmortizedQueueImp.scala
new file mode 100644
index 0000000000000000000000000000000000000000..71d199ea9d1152f708268f073e5cb57fde549100
--- /dev/null
+++ b/testcases/scala-workshop/AmortizedQueueImp.scala
@@ -0,0 +1,138 @@
+import scala.collection.immutable.Set
+import leon.Utils._
+import leon.Annotations._
+
+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 = {
+ 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) && size(r) + size(tmp) == size(l1) + size(l2))
+
+ r
+ } ensuring(res => content(res) == content(l1) ++ content(l2) && size(res) == size(l1) + size(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 = {
+ 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) && size(r) + size(l2) == size(l))
+
+ r
+ } ensuring(res => content(res) == content(l) && size(res) == size(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 enqueueDequeueTwice(queue : AbsQueue, e1 : Int, e2 : Int, e3 : Int) : Boolean = {
+ if (isEmpty(queue)) {
+ val q1 = enqueue(queue, e1)
+ val q2 = enqueue(q1, e2)
+ val e1prime = front(q2)
+ val q3 = tail(q2)
+ val e2prime = front(q3)
+ val q4 = tail(q3)
+ e1 == e1prime && e2 == e2prime
+ } else
+ true
+ } holds
+}
diff --git a/testcases/scala-workshop/Arithmetic.scala b/testcases/scala-workshop/Arithmetic.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2b90bda91805791950d4c9129196b0ebb30bb3e2
--- /dev/null
+++ b/testcases/scala-workshop/Arithmetic.scala
@@ -0,0 +1,84 @@
+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)
+
+ 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/scala-workshop/AssociativeList.scala b/testcases/scala-workshop/AssociativeList.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f5a2fc0415a2cf6023f9ae1f3620e99f9fdc27cb
--- /dev/null
+++ b/testcases/scala-workshop/AssociativeList.scala
@@ -0,0 +1,50 @@
+import scala.collection.immutable.Set
+import leon.Utils._
+import leon.Annotations._
+
+object AssociativeList {
+ sealed abstract class KeyValuePairAbs
+ case class KeyValuePair(key: Int, value: Int) extends KeyValuePairAbs
+
+ sealed abstract class List
+ case class Cons(head: KeyValuePairAbs, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class OptionInt
+ case class Some(i: Int) extends OptionInt
+ case class None() extends OptionInt
+
+ def domain(l: List): Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(KeyValuePair(k,_), xs) => Set(k) ++ domain(xs)
+ }
+
+ def find(l: List, e: Int): OptionInt = l match {
+ case Nil() => None()
+ case Cons(KeyValuePair(k, v), xs) => if (k == e) Some(v) else find(xs, e)
+ }
+
+ def noDuplicates(l: List): Boolean = l match {
+ case Nil() => true
+ case Cons(KeyValuePair(k, v), xs) => find(xs, k) == None() && noDuplicates(xs)
+ }
+
+ def update(l1: List, l2: List): List = (l2 match {
+ case Nil() => l1
+ case Cons(x, xs) => update(updateElem(l1, x), xs)
+ }) ensuring(domain(_) == domain(l1) ++ domain(l2))
+
+ def updateElem(l: List, e: KeyValuePairAbs): List = (l match {
+ case Nil() => Cons(e, Nil())
+ case Cons(KeyValuePair(k, v), xs) => e match {
+ case KeyValuePair(ek, ev) => if (ek == k) Cons(KeyValuePair(ek, ev), xs) else Cons(KeyValuePair(k, v), updateElem(xs, e))
+ }
+ }) ensuring(res => e match {
+ case KeyValuePair(k, v) => domain(res) == domain(l) ++ Set[Int](k)
+ })
+
+ @induct
+ def readOverWrite(l: List, k1: Int, k2: Int, e: Int) : Boolean = {
+ find(updateElem(l, KeyValuePair(k2,e)), k1) == (if (k1 == k2) Some(e) else find(l, k1))
+ } holds
+}
diff --git a/testcases/scala-workshop/AssociativeListImp.scala b/testcases/scala-workshop/AssociativeListImp.scala
new file mode 100644
index 0000000000000000000000000000000000000000..dabf9c994336fb3ddd74b18d5cc170aa7586d995
--- /dev/null
+++ b/testcases/scala-workshop/AssociativeListImp.scala
@@ -0,0 +1,98 @@
+import scala.collection.immutable.Set
+import leon.Utils._
+import leon.Annotations._
+
+object AssociativeListImp {
+ sealed abstract class KeyValuePairAbs
+ case class KeyValuePair(key: Int, value: Int) extends KeyValuePairAbs
+
+ sealed abstract class List
+ case class Cons(head: KeyValuePairAbs, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class OptionInt
+ case class Some(i: Int) extends OptionInt
+ case class None() extends OptionInt
+
+ def domain(l: List): Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(KeyValuePair(k,_), xs) => Set(k) ++ domain(xs)
+ }
+
+ def findSpec(l: List, e: Int): OptionInt = l match {
+ case Nil() => None()
+ case Cons(KeyValuePair(k, v), xs) => if (k == e) Some(v) else find(xs, e)
+ }
+
+ def findLast(l: List, e: Int): OptionInt = {
+ var res: OptionInt = None()
+ var l2 = l
+ while(!l2.isInstanceOf[Nil]) {
+ val Cons(KeyValuePair(k, v), tail) = l2
+ l2 = tail
+ if(k == e)
+ res = Some(v)
+ }
+ res
+ } ensuring(res => findSpec(l, e) == res)
+
+ def find(l: List, e: Int): OptionInt = {
+ var res: OptionInt = None()
+ var l2 = l
+ var seen: List = Nil()
+ (while(!l2.isInstanceOf[Nil]) {
+ val Cons(head@KeyValuePair(k, v), tail) = l2
+ seen = Cons(head, seen)
+ l2 = tail
+ if(res == None() && k == e)
+ res = Some(v)
+ }) invariant((res match {
+ case Some(_) => domain(seen).contains(e)
+ case None() => !domain(seen).contains(e)
+ }) && domain(seen) ++ domain(l2) == domain(l))
+
+ res
+ } ensuring(res => res match {
+ case Some(_) => domain(l).contains(e)
+ case None() => !domain(l).contains(e)
+ })
+
+ def noDuplicates(l: List): Boolean = l match {
+ case Nil() => true
+ case Cons(KeyValuePair(k, v), xs) => find(xs, k) == None() && noDuplicates(xs)
+ }
+
+ def updateElem(l: List, e: KeyValuePairAbs): List = {
+ var res: List = Nil()
+ var l2 = l
+ var found = false
+ val KeyValuePair(ek, ev) = e
+ (while(!l2.isInstanceOf[Nil]) {
+ val Cons(KeyValuePair(k, v), tail) = l2
+ l2 = tail
+ if(k == ek) {
+ res = Cons(KeyValuePair(ek, ev), res)
+ found = true
+ } else {
+ res = Cons(KeyValuePair(k, v), res)
+ }
+ }) invariant(
+ (if(found)
+ domain(res) ++ domain(l2) == domain(l) ++ Set(ek)
+ else
+ domain(res) ++ domain(l2) == domain(l)
+ ))
+ if(!found)
+ Cons(KeyValuePair(ek, ev), res)
+ else
+ res
+ } ensuring(res => e match {
+ case KeyValuePair(k, v) => domain(res) == domain(l) ++ Set[Int](k)
+ })
+
+ @induct
+ def readOverWrite(l: List, k1: Int, k2: Int, e: Int) : Boolean = {
+ find(updateElem(l, KeyValuePair(k2,e)), k1) == (if (k1 == k2) Some(e) else find(l, k1))
+ } //holds
+}
+
diff --git a/testcases/scala-workshop/ListOperations.scala b/testcases/scala-workshop/ListOperations.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a4fc4f8dc44a90f59a772b52b1a05053316e94d2
--- /dev/null
+++ b/testcases/scala-workshop/ListOperations.scala
@@ -0,0 +1,107 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class IntPairList
+ case class IPCons(head: IntPair, tail: IntPairList) extends IntPairList
+ case class IPNil() extends IntPairList
+
+ sealed abstract class IntPair
+ case class IP(fst: Int, snd: Int) extends IntPair
+
+ def size(l: List) : Int = (l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def iplSize(l: IntPairList) : Int = (l match {
+ case IPNil() => 0
+ case IPCons(_, xs) => 1 + iplSize(xs)
+ }) ensuring(_ >= 0)
+
+ def zip(l1: List, l2: List) : IntPairList = {
+ // try to comment this and see how pattern-matching becomes
+ // non-exhaustive and post-condition fails
+ require(size(l1) == size(l2))
+
+ l1 match {
+ case Nil() => IPNil()
+ case Cons(x, xs) => l2 match {
+ case Cons(y, ys) => IPCons(IP(x, y), zip(xs, ys))
+ }
+ }
+ } ensuring(iplSize(_) == size(l1))
+
+ def sizeTailRec(l: List) : Int = sizeTailRecAcc(l, 0)
+ def sizeTailRecAcc(l: List, acc: Int) : Int = {
+ require(acc >= 0)
+ l match {
+ case Nil() => acc
+ case Cons(_, xs) => sizeTailRecAcc(xs, acc+1)
+ }
+ } ensuring(res => res == size(l) + acc)
+
+ def sizesAreEquiv(l: List) : Boolean = {
+ size(l) == sizeTailRec(l)
+ } holds
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty[Int]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def sizeAndContent(l: List) : Boolean = {
+ size(l) == 0 || content(l) != Set.empty[Int]
+ } holds
+
+ def drunk(l : List) : List = (l match {
+ case Nil() => Nil()
+ case Cons(x,l1) => Cons(x,Cons(x,drunk(l1)))
+ }) ensuring (size(_) == 2 * size(l))
+
+ def reverse(l: List) : List = reverse0(l, Nil()) ensuring(content(_) == content(l))
+ def reverse0(l1: List, l2: List) : List = (l1 match {
+ case Nil() => l2
+ case Cons(x, xs) => reverse0(xs, Cons(x, l2))
+ }) ensuring(content(_) == content(l1) ++ content(l2))
+
+ def append(l1 : List, l2 : List) : List = (l1 match {
+ case Nil() => l2
+ case Cons(x,xs) => Cons(x, append(xs, l2))
+ }) ensuring(content(_) == content(l1) ++ content(l2))
+
+ @induct
+ def nilAppend(l : List) : Boolean = (append(l, Nil()) == l) holds
+
+ @induct
+ def appendAssoc(xs : List, ys : List, zs : List) : Boolean =
+ (append(append(xs, ys), zs) == append(xs, append(ys, zs))) holds
+
+ def revAuxBroken(l1 : List, e : Int, l2 : List) : Boolean = {
+ (append(reverse(l1), Cons(e,l2)) == reverse0(l1, l2))
+ } holds
+
+ @induct
+ def sizeAppend(l1 : List, l2 : List) : Boolean =
+ (size(append(l1, l2)) == size(l1) + size(l2)) holds
+
+ @induct
+ def concat(l1: List, l2: List) : List =
+ concat0(l1, l2, Nil()) ensuring(content(_) == content(l1) ++ content(l2))
+
+ @induct
+ def concat0(l1: List, l2: List, l3: List) : List = (l1 match {
+ case Nil() => l2 match {
+ case Nil() => reverse(l3)
+ case Cons(y, ys) => {
+ concat0(Nil(), ys, Cons(y, l3))
+ }
+ }
+ case Cons(x, xs) => concat0(xs, l2, Cons(x, l3))
+ }) ensuring(content(_) == content(l1) ++ content(l2) ++ content(l3))
+}
diff --git a/testcases/scala-workshop/ListOperationsImp.scala b/testcases/scala-workshop/ListOperationsImp.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f30c9d0be06e7a0436883f082d28f6ea687b8479
--- /dev/null
+++ b/testcases/scala-workshop/ListOperationsImp.scala
@@ -0,0 +1,146 @@
+import leon.Utils._
+import leon.Annotations._
+
+object ListOperationsImp {
+
+ 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)
+
+ //just to help for specification, makes sense since specification are not executed
+ 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 sizeStrongSpec(l: List): Int = {
+ var r = 0
+ var l2 = l
+ (while(!l2.isInstanceOf[Nil]) {
+ val Cons(head, tail) = l2
+ l2 = tail
+ r = r+1
+ }) invariant(r == sizeFun(l) - sizeFun(l2))
+ r
+ } ensuring(res => res == sizeFun(l))
+
+ 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 drunk(l : List) : List = {
+ var r: List = Nil()
+ var l2 = l
+ (while(!l2.isInstanceOf[Nil]) {
+ val Cons(head, tail) = l2
+ l2 = tail
+ r = Cons(head, Cons(head, r))
+ }) invariant(sizeFun(r) == 2 * sizeFun(l) - 2 * sizeFun(l2))
+ r
+ } ensuring (sizeFun(_) == 2 * sizeFun(l))
+
+
+ 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 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))
+
+}
diff --git a/testcases/scala-workshop/PropositionalLogic.scala b/testcases/scala-workshop/PropositionalLogic.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a35c3ef9be56871900d5e9474b385f0896edccd4
--- /dev/null
+++ b/testcases/scala-workshop/PropositionalLogic.scala
@@ -0,0 +1,86 @@
+import scala.collection.immutable.Set
+import leon.Utils._
+import leon.Annotations._
+
+object PropositionalLogic {
+
+ sealed abstract class Formula
+ case class And(lhs: Formula, rhs: Formula) extends Formula
+ case class Or(lhs: Formula, rhs: Formula) extends Formula
+ case class Implies(lhs: Formula, rhs: Formula) extends Formula
+ case class Not(f: Formula) extends Formula
+ case class Literal(id: Int) extends Formula
+
+ def simplify(f: Formula): Formula = (f match {
+ case And(lhs, rhs) => And(simplify(lhs), simplify(rhs))
+ case Or(lhs, rhs) => Or(simplify(lhs), simplify(rhs))
+ case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs))
+ case Not(f) => Not(simplify(f))
+ case Literal(_) => f
+ }) ensuring(isSimplified(_))
+
+ def isSimplified(f: Formula): Boolean = f match {
+ case And(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
+ case Or(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
+ case Implies(_,_) => false
+ case Not(f) => isSimplified(f)
+ case Literal(_) => true
+ }
+
+ def nnf(formula: Formula): Formula = (formula match {
+ case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
+ case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
+ case Implies(lhs, rhs) => Implies(nnf(lhs), nnf(rhs))
+ case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
+ case Not(Not(f)) => nnf(f)
+ case Not(Literal(_)) => formula
+ case Literal(_) => formula
+ }) ensuring(isNNF(_))
+
+ def isNNF(f: Formula): Boolean = f match {
+ case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Implies(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Not(Literal(_)) => true
+ case Not(_) => false
+ case Literal(_) => true
+ }
+
+ def vars(f: Formula): Set[Int] = {
+ require(isNNF(f))
+ f match {
+ case And(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Or(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Implies(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Not(Literal(i)) => Set[Int](i)
+ case Literal(i) => Set[Int](i)
+ }
+ }
+
+ def fv(f : Formula) = { vars(nnf(f)) }
+
+ // @induct
+ // def wrongCommutative(f: Formula) : Boolean = {
+ // nnf(simplify(f)) == simplify(nnf(f))
+ // } holds
+
+ @induct
+ def simplifyBreaksNNF(f: Formula) : Boolean = {
+ require(isNNF(f))
+ isNNF(simplify(f))
+ } holds
+
+ @induct
+ def nnfIsStable(f: Formula) : Boolean = {
+ require(isNNF(f))
+ nnf(f) == f
+ } holds
+
+ @induct
+ def simplifyIsStable(f: Formula) : Boolean = {
+ require(isSimplified(f))
+ simplify(f) == f
+ } holds
+}
diff --git a/testcases/scala-workshop/RedBlackTree.scala b/testcases/scala-workshop/RedBlackTree.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bc2de6ba96ee699736d4558932b752eea9ebba9f
--- /dev/null
+++ b/testcases/scala-workshop/RedBlackTree.scala
@@ -0,0 +1,117 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case class Red() extends Color
+ case class Black() extends Color
+
+ sealed abstract class Tree
+ case class Empty() extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ sealed abstract class OptionInt
+ case class Some(v : Int) extends OptionInt
+ case class None() extends OptionInt
+
+ def content(t: Tree) : Set[Int] = t match {
+ case Empty() => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : Int = (t match {
+ case Empty() => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }) ensuring(_ >= 0)
+
+ /* We consider leaves to be black by definition */
+ def isBlack(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(),_,_,_) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(), l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red(), l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Empty() => true
+ }
+
+ def blackHeight(t : Tree) : Int = t match {
+ case Empty() => 1
+ case Node(Black(), l, _, _) => blackHeight(l) + 1
+ case Node(Red(), l, _, _) => blackHeight(l)
+ }
+
+ // <<insert element x into the tree t>>
+ def ins(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ t match {
+ case Empty() => Node(Red(),Empty(),x,Empty())
+ case Node(c,a,y,b) =>
+ if (x < y) balance(c, ins(x, a), y, b)
+ else if (x == y) Node(c,a,y,b)
+ else balance(c,a,y,ins(x, b))
+ }
+ } ensuring (res => content(res) == content(t) ++ Set(x)
+ && size(t) <= size(res) && size(res) <= size(t) + 1
+ && redDescHaveBlackChildren(res)
+ && blackBalanced(res))
+
+ def makeBlack(n: Tree): Tree = {
+ require(redDescHaveBlackChildren(n) && blackBalanced(n))
+ n match {
+ case Node(Red(),l,v,r) => Node(Black(),l,v,r)
+ case _ => n
+ }
+ } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res))
+
+ def add(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ makeBlack(ins(x, t))
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res))
+
+ def buggyAdd(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t))
+ ins(x, t)
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+
+ def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ Node(c,a,x,b) match {
+ case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
+
+ def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ Node(c,a,x,b) match {
+ case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ // case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
+}
diff --git a/testcases/scala-workshop/SearchLinkedList.scala b/testcases/scala-workshop/SearchLinkedList.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2c137fd4ad6b9d411f7e14b4ada6b834234c9e9e
--- /dev/null
+++ b/testcases/scala-workshop/SearchLinkedList.scala
@@ -0,0 +1,48 @@
+import scala.collection.immutable.Set
+import leon.Utils._
+import leon.Annotations._
+
+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/scala-workshop/Sorting.scala b/testcases/scala-workshop/Sorting.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3c683e6e5f3873d2eaa4d4413ac9fe9f01a888ff
--- /dev/null
+++ b/testcases/scala-workshop/Sorting.scala
@@ -0,0 +1,198 @@
+import leon.Annotations._
+import leon.Utils._
+
+// Sorting lists is a fundamental problem in CS.
+object Sorting {
+ // Data types
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ sealed abstract class LList
+ case class LCons(head : List, tail : LList) extends LList
+ case class LNil() extends LList
+
+ // Abstraction functions
+ def content(list : List) : Set[Int] = list match {
+ case Nil() => Set.empty[Int]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def lContent(llist : LList) : Set[Int] = llist match {
+ case LNil() => Set.empty[Int]
+ case LCons(x, xs) => content(x) ++ lContent(xs)
+ }
+
+ def size(list : List) : Int = (list match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil() => true
+ case Cons(_, Nil()) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def lIsSorted(llist : LList) : Boolean = llist match {
+ case LNil() => true
+ case LCons(x, xs) => isSorted(x) && lIsSorted(xs)
+ }
+
+ @induct
+ def sortedLemma(a: Int, x: Int, b: List) = {
+ !(isSorted(Cons(a,b)) && (content(b) contains x)) || (x >= a)
+ } holds
+
+ def abs(i : Int) : Int = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ /***************************
+ * *
+ * I N S E R T I O N *
+ * *
+ ***************************/
+
+ def insertSpec(elem : Int, list : List, res : List) : Boolean = {
+// isSorted(list) && // Part of precondition, really.
+ isSorted(res) && content(res) == content(list) ++ Set(elem)
+ }
+
+ def insertImpl(elem : Int, list : List) : List = {
+ require(isSorted(list))
+ list match {
+ case Nil() => Cons(elem, Nil())
+ case c @ Cons(x, _) if(elem <= x) => Cons(elem, c)
+ case Cons(x, xs) => Cons(x, insertImpl(elem, xs))
+ }
+ } ensuring(insertSpec(elem, list, _))
+
+ /**********************************
+ * *
+ * M E R G I N G (slow+fast) *
+ * *
+ **********************************/
+
+ def mergeSpec(list1 : List, list2 : List, res : List) : Boolean = {
+ // isSorted(list1) && isSorted(list2) && // Part of precondition, really.
+ isSorted(res) && content(res) == content(list1) ++ content(list2)
+ }
+
+ def mergeImpl(list1 : List, list2 : List) : List = {
+ require(isSorted(list1) && isSorted(list2))
+
+ list1 match {
+ case Nil() => list2
+ case Cons(x, xs) => insertImpl(x, mergeImpl(xs, list2))
+ }
+ } ensuring(res => mergeSpec(list1, list2, res))
+
+ def mergeFastImpl(list1 : List, list2 : List) : List = {
+ require(isSorted(list1) && isSorted(list2))
+
+ (list1, list2) match {
+ case (_, Nil()) => list1
+ case (Nil(), _) => list2
+ case (Cons(x, xs), Cons(y, ys)) =>
+ if(x <= y) {
+ Cons(x, mergeFastImpl(xs, list2))
+ } else {
+ Cons(y, mergeFastImpl(list1, ys))
+ }
+ }
+ } ensuring(res => mergeSpec(list1, list2, res))
+
+ /***************************
+ * *
+ * S P L I T T I N G *
+ * *
+ ***************************/
+
+ def splitSpec(list : List, res : (List,List)) : Boolean = {
+ val s1 = size(res._1)
+ val s2 = size(res._2)
+ abs(s1 - s2) <= 1 && s1 + s2 == size(list) &&
+ content(res._1) ++ content(res._2) == content(list)
+ }
+
+ def splitImpl(list : List) : (List,List) = (list match {
+ case Nil() => (Nil(), Nil())
+ case Cons(x, Nil()) => (Cons(x, Nil()), Nil())
+ case Cons(x1, Cons(x2, xs)) =>
+ val (s1,s2) = splitImpl(xs)
+ (Cons(x1, s1), Cons(x2, s2))
+ }) ensuring(res => splitSpec(list, res))
+
+ /***********************
+ * *
+ * S O R T I N G *
+ * *
+ ***********************/
+
+ def sortSpec(in : List, out : List) : Boolean = {
+ content(out) == content(in) && isSorted(out)
+ }
+
+ def insertSorted(in: List, v: Int): List = {
+ require(isSorted(in));
+
+ in match {
+ case Cons(h, t) =>
+ val r = insertSorted(t, v)
+ if (h < v) {
+ Cons(h, r)
+ } else if (h > v) {
+ Cons(v, Cons(h, t))
+ } else {
+ Cons(h, t)
+ }
+ case _ =>
+ Cons(v, Nil())
+ }
+ } ensuring { res => isSorted(res) && content(res) == content(in) ++ Set(v) }
+
+ def insertionSortImpl(in : List) : List = (in match {
+ case Nil() => Nil()
+ case Cons(x, xs) => insertImpl(x, insertionSortImpl(xs))
+ }) ensuring(res => sortSpec(in, res))
+
+ // Not really quicksort, neither mergesort.
+ def weirdSortImpl(in : List) : List = (in match {
+ case Nil() => Nil()
+ case Cons(x, Nil()) => Cons(x, Nil())
+ case _ =>
+ val (s1,s2) = splitImpl(in)
+ mergeFastImpl(weirdSortImpl(s1), weirdSortImpl(s2))
+ }) ensuring(res => sortSpec(in, res))
+
+ def toLList(list : List) : LList = (list match {
+ case Nil() => LNil()
+ case Cons(x, xs) => LCons(Cons(x, Nil()), toLList(xs))
+ }) ensuring(res => lContent(res) == content(list) && lIsSorted(res))
+
+ def mergeMap(llist : LList) : LList = {
+ require(lIsSorted(llist))
+
+ llist match {
+ case LNil() => LNil()
+ case o @ LCons(x, LNil()) => o
+ case LCons(x, LCons(y, ys)) => LCons(mergeFastImpl(x, y), mergeMap(ys))
+ }
+ } ensuring(res => lContent(res) == lContent(llist) && lIsSorted(res))
+
+ def mergeReduce(llist : LList) : List = {
+ require(lIsSorted(llist))
+
+ llist match {
+ case LNil() => Nil()
+ case LCons(x, LNil()) => x
+ case _ => mergeReduce(mergeMap(llist))
+ }
+ } ensuring(res => content(res) == lContent(llist) && isSorted(res))
+
+ def mergeSortImpl(in : List) : List = {
+ mergeReduce(toLList(in))
+ } ensuring(res => sortSpec(in, res))
+}
diff --git a/testcases/scala-workshop/SumAndMax.scala b/testcases/scala-workshop/SumAndMax.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0aa4ce7060a391d34dd047338fcd1f638054843f
--- /dev/null
+++ b/testcases/scala-workshop/SumAndMax.scala
@@ -0,0 +1,46 @@
+import leon.Utils._
+import leon.Annotations._
+
+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
+}
diff --git a/testcases/scala-workshop/SumAndMaxImp.scala b/testcases/scala-workshop/SumAndMaxImp.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d6c9896a82aebb711d05a0fa9c3f8de156a51be9
--- /dev/null
+++ b/testcases/scala-workshop/SumAndMaxImp.scala
@@ -0,0 +1,36 @@
+import leon.Utils._
+
+object SumAndMaxImp {
+
+ 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)
+
+}