From c02f8491fff86586c2e077dc8af4a79f7e17922d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com> Date: Fri, 12 Apr 2013 15:20:17 +0200 Subject: [PATCH] Testcases for Scala workshop 2013 The functional ones are taken from previous collections (SAS2011 and OOPSLA13 submission for Sorting). The imperative ones are based on testcases from the VSTTE competition and adaptations of functional benchmarks of SAS. We are not able to reproduce all successfull properties of the functional benchmarks, especially when the function we are implementating was not originally tail recursive. In that case, a non-trivial encoding would be required (e.g. using accumulators). Insertion sort and other sort algorithms are particularly complicated to implement with an imperative style. Functions like `insert` need to use reversal while reconstructing the list, and need in particular to prove that reversing an increasing list yields a decreasing list. We are not able to prove that yet. (Challenging benchmarks currently beyond our reach are in the top-level testcases directory, as they are not part of the Scala 2013 submission.) --- testcases/BinaryTreeImp.scala | 101 +++++++++ testcases/InsertionSortImp.scala | 107 ++++++++++ testcases/QuickSortImp.scala | 79 +++++++ testcases/scala-workshop/AmortizedQueue.scala | 124 +++++++++++ .../scala-workshop/AmortizedQueueImp.scala | 138 ++++++++++++ testcases/scala-workshop/Arithmetic.scala | 84 ++++++++ .../scala-workshop/AssociativeList.scala | 50 +++++ .../scala-workshop/AssociativeListImp.scala | 98 +++++++++ testcases/scala-workshop/ListOperations.scala | 107 ++++++++++ .../scala-workshop/ListOperationsImp.scala | 146 +++++++++++++ .../scala-workshop/PropositionalLogic.scala | 86 ++++++++ testcases/scala-workshop/RedBlackTree.scala | 117 +++++++++++ .../scala-workshop/SearchLinkedList.scala | 48 +++++ testcases/scala-workshop/Sorting.scala | 198 ++++++++++++++++++ testcases/scala-workshop/SumAndMax.scala | 46 ++++ testcases/scala-workshop/SumAndMaxImp.scala | 36 ++++ 16 files changed, 1565 insertions(+) create mode 100644 testcases/BinaryTreeImp.scala create mode 100644 testcases/InsertionSortImp.scala create mode 100644 testcases/QuickSortImp.scala create mode 100644 testcases/scala-workshop/AmortizedQueue.scala create mode 100644 testcases/scala-workshop/AmortizedQueueImp.scala create mode 100644 testcases/scala-workshop/Arithmetic.scala create mode 100644 testcases/scala-workshop/AssociativeList.scala create mode 100644 testcases/scala-workshop/AssociativeListImp.scala create mode 100644 testcases/scala-workshop/ListOperations.scala create mode 100644 testcases/scala-workshop/ListOperationsImp.scala create mode 100644 testcases/scala-workshop/PropositionalLogic.scala create mode 100644 testcases/scala-workshop/RedBlackTree.scala create mode 100644 testcases/scala-workshop/SearchLinkedList.scala create mode 100644 testcases/scala-workshop/Sorting.scala create mode 100644 testcases/scala-workshop/SumAndMax.scala create mode 100644 testcases/scala-workshop/SumAndMaxImp.scala diff --git a/testcases/BinaryTreeImp.scala b/testcases/BinaryTreeImp.scala new file mode 100644 index 000000000..3005d1991 --- /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 000000000..266905b26 --- /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 000000000..dd8e34b32 --- /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 000000000..dd5a75f89 --- /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 000000000..71d199ea9 --- /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 000000000..2b90bda91 --- /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 000000000..f5a2fc041 --- /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 000000000..dabf9c994 --- /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 000000000..a4fc4f8dc --- /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 000000000..f30c9d0be --- /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 000000000..a35c3ef9b --- /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 000000000..bc2de6ba9 --- /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 000000000..2c137fd4a --- /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 000000000..3c683e6e5 --- /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 000000000..0aa4ce706 --- /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 000000000..d6c9896a8 --- /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) + +} -- GitLab