From ce2e0b1691c1a0d74b585c3188cf135faeed9ab9 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <colder@php.net>
Date: Mon, 26 Aug 2013 15:18:54 +0200
Subject: [PATCH] New/Fixed testcases for oopsla
---
testcases/insynth-leon-tests/Arguments.scala | 13 ++
.../insynth-leon-tests/BubbleSortBug.scala | 30 ++++
.../CaseClassSelectExample.scala | 24 +++
testcases/insynth-leon-tests/Hole.scala | 13 ++
.../ListOperationsHole.scala | 24 +++
.../insynth-leon-tests/RedBlackTreeFull.scala | 117 ++++++++++++++
testcases/insynth-synthesis-tests/Hole.scala | 13 ++
.../insynth-synthesis-tests/LocalScope.scala | 31 ++++
.../RedBlackTreeSynthResult.scala | 95 ++++++++++++
.../RedBlackTreeSynthResultBad.scala | 95 ++++++++++++
.../synthesis/BatchedQueue/BatchedQueue.scala | 76 ++++++++++
.../BatchedQueue/BatchedQueueCheckf.scala | 49 ++++++
.../BatchedQueue/BatchedQueueFull.scala | 101 +++++++++++++
.../BatchedQueue/BatchedQueueSnoc.scala | 60 ++++++++
.../BatchedQueue/BatchedQueueSnocWeird.scala | 63 ++++++++
.../BatchedQueue/BatchedQueueTail.scala | 56 +++++++
.../lesynth/synthesis/BinarySearch.scala | 42 +++++
.../BinarySearchTreeFull.scala | 143 ++++++++++++++++++
.../BinarySearchTreeMember.scala | 115 ++++++++++++++
.../InsertionSort/InsertionSortInsert.scala | 61 ++++++++
.../InsertionSort/InsertionSortSort.scala | 57 +++++++
.../lesynth/synthesis/List/ListConcat.scala | 20 +++
.../lesynth/synthesis/List/ListSearch.scala | 50 ++++++
.../synthesis/MergeSort/MergeSortMerge.scala | 55 +++++++
.../synthesis/MergeSort/MergeSortSort.scala | 86 +++++++++++
.../MergeSort/MergeSortSortWithVal.scala | 85 +++++++++++
.../Other/AddressesMakeAddressBook.scala | 103 +++++++++++++
.../AddressesMakeAddressBookWithHelpers.scala | 106 +++++++++++++
.../Other/AddressesMergeAddressBooks.scala | 81 ++++++++++
.../synthesis/RedBlackTree/RedBlackTree.scala | 81 ++++++++++
.../RedBlackTree/RedBlackTreeInsert.scala | 77 ++++++++++
testcases/lesynth/test/Addresses.scala | 52 +++++++
.../test/AddressesMergeAddressBooks.scala | 70 +++++++++
.../lesynth/test/refinement/ListConcat.scala | 20 +++
.../test/refinement/ListConcatWithEmpty.scala | 37 +++++
.../test/verifier/BinarySearchTree.scala | 65 ++++++++
.../lesynth/test/verifier/ListConcat.scala | 44 ++++++
.../AddressesMakeAddressBook.scala | 103 +++++++++++++
.../AddressesMakeAddressBookStrong.scala | 129 ++++++++++++++++
.../AddressesMakeAddressBookSynthWrong.scala | 113 ++++++++++++++
.../AddressesMakeAddressBookWithHelpers.scala | 106 +++++++++++++
.../AddressesMergeAddressBooks.scala | 78 ++++++++++
.../AddressesMergeAddressBooksStep1.scala | 73 +++++++++
.../AddressesMergeAddressBooksStep2.scala | 83 ++++++++++
.../BatchedQueue/BatchedQueueCheckf.scala | 49 ++++++
.../BatchedQueue/BatchedQueueFull.scala | 91 +++++++++++
.../BatchedQueue/BatchedQueueSnoc.scala | 60 ++++++++
.../oopsla2013/BinaryTree/Batch.scala | 36 +++++
.../synthesis/oopsla2013/Church/Batch.scala | 25 +++
.../oopsla2013/InsertionSort/Complete.scala | 48 ++++++
.../oopsla2013/InsertionSort/Insert.scala | 53 +++++++
.../oopsla2013/InsertionSort/Sort.scala | 52 +++++++
.../synthesis/oopsla2013/List/Batch.scala | 38 +++++
.../synthesis/oopsla2013/List/Split.scala | 98 ++++++++++++
.../oopsla2013/MergeSort/Complete.scala | 85 +++++++++++
.../oopsla2013/MergeSort/MergeSortSort.scala | 86 +++++++++++
.../MergeSort/MergeSortSortWithVal.scala | 85 +++++++++++
.../oopsla2013/SortedList/Batch.scala | 89 +++++++++++
.../oopsla2013/SortedList/Complete.scala | 10 +-
.../oopsla2013/SortedList/Delete.scala | 31 ++--
.../oopsla2013/SortedList/Diff.scala | 33 ++--
.../oopsla2013/SortedList/Insert1.scala | 13 +-
.../oopsla2013/SortedList/Insert2.scala | 10 +-
.../oopsla2013/SortedList/Sort.scala | 25 +--
.../oopsla2013/SortedList/SortInsert.scala | 105 +++++++++++++
.../oopsla2013/SortedList/SortMerge.scala | 114 ++++++++++++++
.../SortedList/SortMergeWithHint.scala | 124 +++++++++++++++
.../oopsla2013/SortedList/Split.scala | 23 +--
.../oopsla2013/SortedList/Split1.scala | 23 +--
.../oopsla2013/SortedList/Split2.scala | 23 +--
.../oopsla2013/SortedList/Split3.scala | 23 +--
.../oopsla2013/SortedList/Union.scala | 23 +--
.../oopsla2013/SortedList/UnionIO.scala | 52 +++++++
.../oopsla2013/SparseVector/Batch.scala | 63 ++++++++
.../oopsla2013/StrictSortedList/Batch.scala | 46 ++++++
.../oopsla2013/StrictSortedList/Delete.scala | 7 +-
.../oopsla2013/StrictSortedList/Diff.scala | 8 +-
.../oopsla2013/StrictSortedList/Insert.scala | 7 +-
.../oopsla2013/StrictSortedList/Union.scala | 8 +-
79 files changed, 4468 insertions(+), 193 deletions(-)
create mode 100644 testcases/insynth-leon-tests/Arguments.scala
create mode 100644 testcases/insynth-leon-tests/BubbleSortBug.scala
create mode 100644 testcases/insynth-leon-tests/CaseClassSelectExample.scala
create mode 100644 testcases/insynth-leon-tests/Hole.scala
create mode 100644 testcases/insynth-leon-tests/ListOperationsHole.scala
create mode 100644 testcases/insynth-leon-tests/RedBlackTreeFull.scala
create mode 100644 testcases/insynth-synthesis-tests/Hole.scala
create mode 100644 testcases/insynth-synthesis-tests/LocalScope.scala
create mode 100644 testcases/lesynth-results/RedBlackTreeSynthResult.scala
create mode 100644 testcases/lesynth-results/RedBlackTreeSynthResultBad.scala
create mode 100644 testcases/lesynth/synthesis/BatchedQueue/BatchedQueue.scala
create mode 100644 testcases/lesynth/synthesis/BatchedQueue/BatchedQueueCheckf.scala
create mode 100644 testcases/lesynth/synthesis/BatchedQueue/BatchedQueueFull.scala
create mode 100644 testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnoc.scala
create mode 100644 testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnocWeird.scala
create mode 100644 testcases/lesynth/synthesis/BatchedQueue/BatchedQueueTail.scala
create mode 100644 testcases/lesynth/synthesis/BinarySearch.scala
create mode 100644 testcases/lesynth/synthesis/BinarySearchTree/BinarySearchTreeFull.scala
create mode 100644 testcases/lesynth/synthesis/BinarySearchTree/BinarySearchTreeMember.scala
create mode 100644 testcases/lesynth/synthesis/InsertionSort/InsertionSortInsert.scala
create mode 100644 testcases/lesynth/synthesis/InsertionSort/InsertionSortSort.scala
create mode 100644 testcases/lesynth/synthesis/List/ListConcat.scala
create mode 100644 testcases/lesynth/synthesis/List/ListSearch.scala
create mode 100644 testcases/lesynth/synthesis/MergeSort/MergeSortMerge.scala
create mode 100644 testcases/lesynth/synthesis/MergeSort/MergeSortSort.scala
create mode 100644 testcases/lesynth/synthesis/MergeSort/MergeSortSortWithVal.scala
create mode 100644 testcases/lesynth/synthesis/Other/AddressesMakeAddressBook.scala
create mode 100644 testcases/lesynth/synthesis/Other/AddressesMakeAddressBookWithHelpers.scala
create mode 100644 testcases/lesynth/synthesis/Other/AddressesMergeAddressBooks.scala
create mode 100644 testcases/lesynth/synthesis/RedBlackTree/RedBlackTree.scala
create mode 100644 testcases/lesynth/synthesis/RedBlackTree/RedBlackTreeInsert.scala
create mode 100644 testcases/lesynth/test/Addresses.scala
create mode 100644 testcases/lesynth/test/AddressesMergeAddressBooks.scala
create mode 100644 testcases/lesynth/test/refinement/ListConcat.scala
create mode 100644 testcases/lesynth/test/refinement/ListConcatWithEmpty.scala
create mode 100644 testcases/lesynth/test/verifier/BinarySearchTree.scala
create mode 100644 testcases/lesynth/test/verifier/ListConcat.scala
create mode 100644 testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala
create mode 100644 testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala
create mode 100644 testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala
create mode 100644 testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala
create mode 100644 testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala
create mode 100644 testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala
create mode 100644 testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala
create mode 100644 testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueCheckf.scala
create mode 100644 testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueFull.scala
create mode 100644 testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueSnoc.scala
create mode 100644 testcases/synthesis/oopsla2013/BinaryTree/Batch.scala
create mode 100644 testcases/synthesis/oopsla2013/Church/Batch.scala
create mode 100644 testcases/synthesis/oopsla2013/InsertionSort/Complete.scala
create mode 100644 testcases/synthesis/oopsla2013/InsertionSort/Insert.scala
create mode 100644 testcases/synthesis/oopsla2013/InsertionSort/Sort.scala
create mode 100644 testcases/synthesis/oopsla2013/List/Batch.scala
create mode 100644 testcases/synthesis/oopsla2013/List/Split.scala
create mode 100644 testcases/synthesis/oopsla2013/MergeSort/Complete.scala
create mode 100644 testcases/synthesis/oopsla2013/MergeSort/MergeSortSort.scala
create mode 100644 testcases/synthesis/oopsla2013/MergeSort/MergeSortSortWithVal.scala
create mode 100644 testcases/synthesis/oopsla2013/SortedList/Batch.scala
create mode 100644 testcases/synthesis/oopsla2013/SortedList/SortInsert.scala
create mode 100644 testcases/synthesis/oopsla2013/SortedList/SortMerge.scala
create mode 100644 testcases/synthesis/oopsla2013/SortedList/SortMergeWithHint.scala
create mode 100644 testcases/synthesis/oopsla2013/SortedList/UnionIO.scala
create mode 100644 testcases/synthesis/oopsla2013/SparseVector/Batch.scala
create mode 100644 testcases/synthesis/oopsla2013/StrictSortedList/Batch.scala
diff --git a/testcases/insynth-leon-tests/Arguments.scala b/testcases/insynth-leon-tests/Arguments.scala
new file mode 100644
index 000000000..cae6e5f9e
--- /dev/null
+++ b/testcases/insynth-leon-tests/Arguments.scala
@@ -0,0 +1,13 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Hole {
+
+ def method(t: Int, x: Boolean, y: Boolean) : Int = ({
+ if (t > 5)
+ hole(5)
+ else
+ t
+ }) ensuring ( _ > 0 )
+
+}
diff --git a/testcases/insynth-leon-tests/BubbleSortBug.scala b/testcases/insynth-leon-tests/BubbleSortBug.scala
new file mode 100644
index 000000000..4377e4399
--- /dev/null
+++ b/testcases/insynth-leon-tests/BubbleSortBug.scala
@@ -0,0 +1,30 @@
+import leon.Utils._
+
+/* The calculus of Computation textbook */
+
+object BubbleSortBug {
+
+ def sort(a: Array[Int]): Array[Int] = ({
+ require(a.length >= 1)
+ var i = a.length - 1
+ var j = 0
+ val sa = a.clone
+ (while(i > 0) {
+ j = 0
+ (while(j < i) {
+ if(sa(j) < sa(j+1)) {
+ val tmp = sa(j)
+ sa(j) = sa(j+1)
+
+ hole(0)
+
+ sa(j+1) = tmp
+ }
+ j = j + 1
+ }) invariant(j >= 0 && j <= i && i < sa.length)
+ i = i - 1
+ }) invariant(i >= 0 && i < sa.length)
+ sa
+ }) ensuring(res => true)
+
+}
diff --git a/testcases/insynth-leon-tests/CaseClassSelectExample.scala b/testcases/insynth-leon-tests/CaseClassSelectExample.scala
new file mode 100644
index 000000000..5239efa37
--- /dev/null
+++ b/testcases/insynth-leon-tests/CaseClassSelectExample.scala
@@ -0,0 +1,24 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object CaseClassSelectExample {
+
+ sealed abstract class OptionInt
+ case class Some(v : Int) extends OptionInt
+ case class None() extends OptionInt
+
+ // this won't work
+// sealed abstract class AbsHasVal(v: Int)
+// case class Concrete(x: Int) extends AbsHasVal(x)
+
+ def selectIntFromSome(some: Some) = {
+ some.v
+ }
+
+ // this won't work
+// def selectIntFromSome(a: Concrete) = {
+// a.v
+// }
+
+}
diff --git a/testcases/insynth-leon-tests/Hole.scala b/testcases/insynth-leon-tests/Hole.scala
new file mode 100644
index 000000000..f860590f3
--- /dev/null
+++ b/testcases/insynth-leon-tests/Hole.scala
@@ -0,0 +1,13 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Hole {
+
+ def method(t: Int) : Int = ({
+ if (t > 5)
+ hole(5)
+ else
+ t
+ }) ensuring ( _ > 0 )
+
+}
diff --git a/testcases/insynth-leon-tests/ListOperationsHole.scala b/testcases/insynth-leon-tests/ListOperationsHole.scala
new file mode 100644
index 000000000..bd3cb28e6
--- /dev/null
+++ b/testcases/insynth-leon-tests/ListOperationsHole.scala
@@ -0,0 +1,24 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+// def isEmpty(l: List) = l match {
+// case Nil() => true
+// case Cons(_, _) => false
+// }
+
+ def concat(l1: List, l2: List) : List = ({
+ hole(l1)
+ }) ensuring(res => content(res) == content(l1) ++ content(l2))
+
+}
diff --git a/testcases/insynth-leon-tests/RedBlackTreeFull.scala b/testcases/insynth-leon-tests/RedBlackTreeFull.scala
new file mode 100644
index 000000000..bc2de6ba9
--- /dev/null
+++ b/testcases/insynth-leon-tests/RedBlackTreeFull.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/insynth-synthesis-tests/Hole.scala b/testcases/insynth-synthesis-tests/Hole.scala
new file mode 100644
index 000000000..091afbdb4
--- /dev/null
+++ b/testcases/insynth-synthesis-tests/Hole.scala
@@ -0,0 +1,13 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Hole {
+
+ def method(t: Int) : Int = ({
+ if (t > 5)
+ hole(5)
+ else
+ t
+ })// ensuring ( _ > 0 )
+
+}
diff --git a/testcases/insynth-synthesis-tests/LocalScope.scala b/testcases/insynth-synthesis-tests/LocalScope.scala
new file mode 100644
index 000000000..4d3969347
--- /dev/null
+++ b/testcases/insynth-synthesis-tests/LocalScope.scala
@@ -0,0 +1,31 @@
+import leon.Utils._
+
+object LocalScope {
+ 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 blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_, l, v, r) => {
+ // hide r
+ val r: Int = 5
+ //val f: ((Int, Int) => Boolean) = (x: Int, y: Int) => false
+
+ Some(5) match {
+ case Some(newInt) => hole(0)
+ }
+
+ false
+ }
+
+ case Empty() => true
+ }
+}
\ No newline at end of file
diff --git a/testcases/lesynth-results/RedBlackTreeSynthResult.scala b/testcases/lesynth-results/RedBlackTreeSynthResult.scala
new file mode 100644
index 000000000..c1c1c46b3
--- /dev/null
+++ b/testcases/lesynth-results/RedBlackTreeSynthResult.scala
@@ -0,0 +1,95 @@
+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
+
+ 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)
+ }
+
+ /* 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)
+ }
+
+ 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)))
+
+ // <<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))
+// }
+ if ((redNodesHaveBlackChildren(t) && blackBalanced(t))) {
+ (t match {
+ case Empty() =>
+ Node(Red(), Empty(), x, Empty())
+ case n: Node =>
+ if ((n.value == x)) {
+ balance(Black(), n.right, x, n.left)
+ } else {
+ balance(n.color, n.left, x, ins(n.value, n.right))
+ }
+ })
+ } else {
+ leon.Utils.error[Tree]("Precondition failed")
+ }
+ } ensuring (res => content(res) == content(t) ++ Set(x)
+ && size(t) <= size(res) && size(res) <= size(t) + 1
+ && redDescHaveBlackChildren(res)
+ && blackBalanced(res))
+
+}
diff --git a/testcases/lesynth-results/RedBlackTreeSynthResultBad.scala b/testcases/lesynth-results/RedBlackTreeSynthResultBad.scala
new file mode 100644
index 000000000..4be3aae0f
--- /dev/null
+++ b/testcases/lesynth-results/RedBlackTreeSynthResultBad.scala
@@ -0,0 +1,95 @@
+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
+
+ 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)
+ }
+
+ /* 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)
+ }
+
+ 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)))
+
+ // <<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))
+// }
+ if ((redNodesHaveBlackChildren(t) && blackBalanced(t))) {
+ (t match {
+ case Empty() =>
+ Node(Red(), Empty(), x, Empty())
+ case n: Node =>
+ if ((n.value == x)) {
+ Node(n.color, n.left, x, n.right)
+ } else {
+ balance(n.color, n.right, n.value, ins(x, n.left))
+ }
+ })
+ } else {
+ leon.Utils.error[Tree]("Precondition failed")
+ }
+ } ensuring (res => content(res) == content(t) ++ Set(x)
+ && size(t) <= size(res) && size(res) <= size(t) + 1
+ && redDescHaveBlackChildren(res)
+ && blackBalanced(res))
+
+}
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueue.scala b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueue.scala
new file mode 100644
index 000000000..941bbadf9
--- /dev/null
+++ b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueue.scala
@@ -0,0 +1,76 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object BatchedQueue {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def content(p: Queue): Set[Int] =
+ content(p.f) ++ content(p.r)
+
+ def isEmpty(p: Queue): Boolean = p.f == Nil
+
+ case class Queue(f: List, r: List)
+
+ def rev_append(aList: List, bList: List): List = (aList match {
+ case Nil => bList
+ case Cons(x, xs) => rev_append(xs, Cons(x, bList))
+ }) ensuring (content(_) == content(aList) ++ content(bList))
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (content(_) == content(list))
+
+ def checkf(f: List, r: List): Queue = (f match {
+ case Nil => Queue(reverse(r), Nil)
+ case _ => Queue(f, r)
+ }) ensuring {
+ res => content(res) == content(f) ++ content(r)
+ }
+
+ def head(p: Queue): Set[Int] = (
+ p.f match {
+ case Nil => Set[Int]()
+ case Cons(x, xs) => Set(x)
+ }) ensuring (
+ res =>
+ if (isEmpty(p)) true
+ else content(p) == res ++ content(tail(p)))
+
+ def tail(p: Queue): Queue = {
+ require(!isEmpty(p))
+ p.f match {
+ case Nil => p
+ case Cons(_, xs) => checkf(xs, p.r)
+ }
+ }
+ //
+ // def last(p: Queue): Int = {
+ // require(!isEmpty(p))
+ // p.r match {
+ // case Nil => reverse(p.f).asInstanceOf[Cons].head
+ // case Cons(x, _) => x
+ // }
+ // }
+
+ def snoc(p: Queue, x: Int): Queue =
+ checkf(p.f, Cons(x, p.r)) ensuring (
+ res =>
+ content(res) == content(p) ++ Set(x) &&
+ (if (isEmpty(p)) true
+ else content(tail(res)) ++ Set(x) == content(tail(res))))
+
+ def main(args: Array[String]): Unit = {
+ val pair = Queue(Cons(4, Nil), Cons(3, Nil))
+
+ println(head(pair))
+ println(content(pair) == head(pair) ++ content(tail(pair)))
+
+ println(head(Queue(Nil, Nil)))
+ }
+}
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueCheckf.scala b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueCheckf.scala
new file mode 100644
index 000000000..4faa50286
--- /dev/null
+++ b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueCheckf.scala
@@ -0,0 +1,49 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object BatchedQueue {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def content(p: Queue): Set[Int] =
+ content(p.f) ++ content(p.r)
+
+ case class Queue(f: List, r: List)
+
+ def rev_append(aList: List, bList: List): List = (aList match {
+ case Nil => bList
+ case Cons(x, xs) => rev_append(xs, Cons(x, bList))
+ }) ensuring (content(_) == content(aList) ++ content(bList))
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (content(_) == content(list))
+
+ def invariantList(q:Queue, f: List, r: List): Boolean = {
+ rev_append(q.f, q.r) == rev_append(f, r) &&
+ { if (q.f == Nil) q.r == Nil else true }
+ }
+
+ def tail(p: Queue): Queue = {
+ p.f match {
+ case Nil => p
+ case Cons(_, xs) => checkf(xs, p.r)
+ }
+ }
+
+//(f match {
+// case Nil => Queue(reverse(r), Nil)
+// case _ => Queue(f, r)
+ def checkf(f: List, r: List): Queue = {
+ choose {
+ (res: Queue) =>
+ invariantList(res, f, r)
+ }
+ }
+
+}
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueFull.scala b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueFull.scala
new file mode 100644
index 000000000..cc5f1f73a
--- /dev/null
+++ b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueFull.scala
@@ -0,0 +1,101 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object BatchedQueue {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def content(p: Queue): Set[Int] =
+ content(p.f) ++ content(p.r)
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def size(q: Queue) : Int =
+ size(q.f) + size(q.r)
+
+ def isEmpty(p: Queue): Boolean = p.f == Nil
+
+ case class Queue(f: List, r: List)
+
+ def rev_append(aList: List, bList: List): List = (aList match {
+ case Nil => bList
+ case Cons(x, xs) => rev_append(xs, Cons(x, bList))
+ }) ensuring (
+ res =>
+ content(res) == content(aList) ++ content(bList) &&
+ size(res) == size(aList) + size(bList)
+ )
+
+ def invariantList(q:Queue, f: List, r: List): Boolean = ({
+ rev_append(q.f, q.r) == rev_append(f, r)
+ }) ensuring (
+ res =>
+ true
+ )
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (
+ res =>
+ content(res) == content(list) && size(res) == size(list)
+ )
+
+ def checkf(f: List, r: List): Queue = (f match {
+ case Nil => Queue(reverse(r), Nil)
+ case _ => Queue(f, r)
+ }) ensuring {
+ res => content(res) == content(f) ++ content(r) &&
+ size(res) == size(f) + size(r) &&
+ invariantList(res, f, r)
+ }
+
+ def head(p: Queue): Set[Int] = (
+ p.f match {
+ case Nil => Set[Int]()
+ case Cons(x, xs) => Set(x)
+ }) ensuring (
+ res =>
+ if (isEmpty(p)) true
+ else content(p) == res ++ content(tail(p)))
+
+ def tail(p: Queue): Queue = {
+ require(!isEmpty(p))
+ p.f match {
+ case Nil => p
+ case Cons(_, xs) => checkf(xs, p.r)
+ }
+ } ensuring {
+ (res: Queue) => content(res) ++ head(p) == content(p) &&
+ (if (isEmpty(p)) true
+ else size(res) + 1 == size(p))
+ }
+ //
+ // def last(p: Queue): Int = {
+ // require(!isEmpty(p))
+ // p.r match {
+ // case Nil => reverse(p.f).asInstanceOf[Cons].head
+ // case Cons(x, _) => x
+ // }
+ // }
+
+ def snoc(p: Queue, x: Int): Queue =
+ checkf(p.f, Cons(x, p.r)) ensuring (
+ res =>
+ content(res) == content(p) ++ Set(x) &&
+ size(res) == size(p) + 1 &&
+ (
+ if (isEmpty(p)) true
+ else (content(tail(res)) ++ Set(x) == content(tail(res)) &&
+ size(res.f) == size(p.f))
+ )
+ )
+
+}
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnoc.scala b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnoc.scala
new file mode 100644
index 000000000..6541b33b5
--- /dev/null
+++ b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnoc.scala
@@ -0,0 +1,60 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object BatchedQueue {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def content(p: Queue): Set[Int] =
+ content(p.f) ++ content(p.r)
+
+ case class Queue(f: List, r: List)
+
+ def rev_append(aList: List, bList: List): List = (aList match {
+ case Nil => bList
+ case Cons(x, xs) => rev_append(xs, Cons(x, bList))
+ }) ensuring (content(_) == content(aList) ++ content(bList))
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (content(_) == content(list))
+
+ def invariantList(q:Queue, f: List, r: List): Boolean = {
+ rev_append(q.f, q.r) == rev_append(f, r) &&
+ { if (q.f == Nil) q.r == Nil else true }
+ }
+
+ def tail(p: Queue): Queue = {
+ p.f match {
+ case Nil => p
+ case Cons(_, xs) => checkf(xs, p.r)
+ }
+ }
+
+ def checkf(f: List, r: List): Queue = (f match {
+ case Nil => Queue(reverse(r), Nil)
+ case _ => Queue(f, r)
+ }) ensuring {
+ res => content(res) == content(f) ++ content(r)
+ }
+ //
+ // def last(p: Queue): Int = {
+ // require(!isEmpty(p))
+ // p.r match {
+ // case Nil => reverse(p.f).asInstanceOf[Cons].head
+ // case Cons(x, _) => x
+ // }
+ // }
+
+ def snoc(p: Queue, x: Int): Queue =
+ choose { (res: Queue) =>
+ content(res) == content(p) ++ Set(x) &&
+ (p.f == Nil || content(tail(res)) ++
+ Set(x) == content(tail(res)))
+ }
+}
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnocWeird.scala b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnocWeird.scala
new file mode 100644
index 000000000..0b9eccfc3
--- /dev/null
+++ b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueSnocWeird.scala
@@ -0,0 +1,63 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object BatchedQueue {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def content(p: Queue): Set[Int] =
+ content(p.f) ++ content(p.r)
+
+ def isEmpty(p: Queue): Boolean = p.f == Nil
+
+ case class Queue(f: List, r: List)
+
+ def rev_append(aList: List, bList: List): List = (aList match {
+ case Nil => bList
+ case Cons(x, xs) => rev_append(xs, Cons(x, bList))
+ }) ensuring (content(_) == content(aList) ++ content(bList))
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (content(_) == content(list))
+
+ def queueInvariant(q:Queue) = if (q.f == Nil) q.r == Nil else true
+
+ def invariantList(q:Queue, f: List, r: List): Boolean = {
+ rev_append(q.f, q.r) == rev_append(f, r) &&
+ { if (q.f == Nil) q.r == Nil else true }
+ }
+
+ def checkf(f: List, r: List): Queue = (f match {
+ case Nil => Queue(reverse(r), Nil)
+ case _ => Queue(f, r)
+ }) ensuring {
+ res => content(res) == content(f) ++ content(r)
+ }
+ //
+ // def last(p: Queue): Int = {
+ // require(!isEmpty(p))
+ // p.r match {
+ // case Nil => reverse(p.f).asInstanceOf[Cons].head
+ // case Cons(x, _) => x
+ // }
+ // }
+
+ def snoc(p: Queue, x: Int): Queue = {
+ require(queueInvariant(p))
+ choose { (res: Queue) =>
+ content(res) == content(p) ++ Set(x) &&
+ {res.f match {
+ case Nil => content(res) ++ Set(x) == content(res)
+ case Cons(_, xs) =>
+ content(checkf(xs, p.r)) ++ Set(x) == content(checkf(xs, p.r))
+ }}
+
+ }
+ }
+}
diff --git a/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueTail.scala b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueTail.scala
new file mode 100644
index 000000000..d35737dab
--- /dev/null
+++ b/testcases/lesynth/synthesis/BatchedQueue/BatchedQueueTail.scala
@@ -0,0 +1,56 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object BatchedQueue {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def content(p: Queue): Set[Int] =
+ content(p.f) ++ content(p.r)
+
+ def isEmpty(p: Queue): Boolean = p.f == Nil
+
+ case class Queue(f: List, r: List)
+
+ def rev_append(aList: List, bList: List): List = (aList match {
+ case Nil => bList
+ case Cons(x, xs) => rev_append(xs, Cons(x, bList))
+ }) ensuring (content(_) == content(aList) ++ content(bList))
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (content(_) == content(list))
+
+ def invariantList(q:Queue, f: List, r: List): Boolean = {
+ rev_append(q.f, q.r) == rev_append(f, r) &&
+ { if (q.f == Nil) q.r == Nil else true }
+ }
+
+ def checkf(f: List, r: List): Queue = (f match {
+ case Nil => Queue(reverse(r), Nil)
+ case _ => Queue(f, r)
+ }) ensuring {
+ res => content(res) == content(f) ++ content(r)
+ }
+
+ def tail(p: Queue): Queue = {
+ require( if (p.f == Nil) p.r == Nil else true )
+// p.f match {
+// case Nil => p
+// case Cons(_, xs) => checkf(xs, p.r)
+// }
+ choose {
+ (res: Queue) =>
+ p.f match {
+ case Nil => isEmpty(res)
+ case Cons(x, xs) => content(res) ++ Set(x) == content(p) && content(res) != content(p)
+ }
+ }
+ }
+
+}
diff --git a/testcases/lesynth/synthesis/BinarySearch.scala b/testcases/lesynth/synthesis/BinarySearch.scala
new file mode 100644
index 000000000..d35de5266
--- /dev/null
+++ b/testcases/lesynth/synthesis/BinarySearch.scala
@@ -0,0 +1,42 @@
+import leon.Utils._
+
+object BinarySearch {
+
+ def binarySearch(a: Array[Int], key: Int): Int =
+ choose{ (res: Int) =>
+ res >= -1 &&
+ res < a.length &&
+ (if(res >= 0) a(res) == key else !occurs(a, 0, a.length, key))
+ }
+
+
+ def occurs(a: Array[Int], from: Int, to: Int, key: Int): Boolean = {
+ require(a.length >= 0 && to <= a.length && from >= 0)
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= to)
+ false
+ else {
+ if(a(i) == key) true else rec(i+1)
+ }
+ }
+ if(from >= to)
+ false
+ else
+ rec(from)
+ }
+
+
+ def sorted(a: Array[Int], l: Int, u: Int) : Boolean = {
+ require(a.length >= 0 && l >= 0 && l <= u && u < a.length)
+ val t = sortedWhile(true, l, l, u, a)
+ t._1
+ }
+
+ def sortedWhile(isSorted: Boolean, k: Int, l: Int, u: Int, a: Array[Int]): (Boolean, Int) = {
+ require(a.length >= 0 && l >= 0 && l <= u && u < a.length && k >= l && k <= u)
+ if(k < u) {
+ sortedWhile(if(a(k) > a(k + 1)) false else isSorted, k + 1, l, u, a)
+ } else (isSorted, k)
+ }
+}
diff --git a/testcases/lesynth/synthesis/BinarySearchTree/BinarySearchTreeFull.scala b/testcases/lesynth/synthesis/BinarySearchTree/BinarySearchTreeFull.scala
new file mode 100644
index 000000000..e45440740
--- /dev/null
+++ b/testcases/lesynth/synthesis/BinarySearchTree/BinarySearchTreeFull.scala
@@ -0,0 +1,143 @@
+import scala.collection.immutable.Set
+
+import leon.Annotations._
+import leon.Utils._
+
+object BinarySearchTree {
+ sealed abstract class Tree
+ case class Node(left: Tree, value: Int, right: Tree) extends Tree
+ case class Leaf() extends Tree
+
+ def contents(tree: Tree): Set[Int] = tree match {
+ case Leaf() => Set.empty[Int]
+ case Node(l, v, r) => contents(l) ++ Set(v) ++ contents(r)
+ }
+
+ def isSortedMinMax(t: Tree, min: Int, max: Int): Boolean = t match {
+ case Node(l, v, r) =>
+ isSortedMinMax(l, min, v) &&
+ isSortedMinMax(r, v, max) &&
+ v < max && v > min
+ case _ => true
+ }
+
+ def isSortedMin(t: Tree, min: Int): Boolean = t match {
+ case Node(l, v, r) =>
+ isSortedMinMax(l, min, v) &&
+ isSortedMin(r, v) &&
+ v > min
+ case _ => true
+ }
+
+ def isSortedMax(t: Tree, max: Int): Boolean = t match {
+ case Node(l, v, r) =>
+ isSortedMax(l, v) &&
+ isSortedMinMax(r, v, max) &&
+ v < max
+ case _ => true
+ }
+
+ def isSorted(t: Tree): Boolean = t match {
+ case Node(l, v, r) =>
+ isSortedMin(r, v) &&
+ isSortedMax(l, v)
+ case _ => true
+ }
+
+// def isSorted(tree: Tree): Boolean = tree match {
+// case Leaf() => true
+// case Node(Leaf(), v, Leaf()) => true
+// case Node(l @ Node(_, vIn, _), v, Leaf()) => v > vIn && isSorted(l)
+// case Node(Leaf(), v, r @ Node(_, vIn, _)) => v < vIn && isSorted(r)
+// case Node(l @ Node(_, vInLeft, _), v, r @ Node(_, vInRight, _)) =>
+// v > vInLeft && v < vInRight && isSorted(l) && isSorted(r)
+// }
+//
+// def isSorted(tree: Tree): Boolean = tree match {
+// case Leaf() => true
+// case Node(l, v, r) => isLowerThan(l, v) && isGreaterThan(r, v) && isSorted(l) && isSorted(r)
+// }
+//
+// def isLowerThan(tree: Tree, max: Int): Boolean = tree match {
+// case Leaf() => true
+// case Node(l, v, r) => v < max && isLowerThan(l, max) && isLowerThan(r, max)
+// }
+//
+// def isGreaterThan(tree: Tree, min: Int): Boolean = tree match {
+// case Leaf() => true
+// case Node(l, v, r) => v > min && isGreaterThan(r, min) && isGreaterThan(l, min)
+// }
+//
+// def isSorted(tree: Tree): Boolean = tree match {
+// case Leaf() => true
+// case Node(l, v, r) => isSorted(l) && isSorted(r) &&
+// contents(l).forall( v > _ ) && contents(r).forall( v < _ )
+// }
+
+ def member(tree: Tree, value: Int): Boolean = {
+ require(isSorted(tree))
+ tree match {
+ case Leaf() => false
+ case n @ Node(l, v, r) => if (v < value) {
+ member(r, value)
+ } else if (v > value) {
+ member(l, value)
+ } else {
+ true
+ }
+ }
+ } ensuring (res =>
+ (res && contents(tree).contains(value)) ||
+ (!res && !contents(tree).contains(value))
+ )
+
+// def insert(tree: Tree, value: Int): Node = {
+// require(isSorted(tree))
+// tree match {
+// case Leaf() => Node(Leaf(), value, Leaf())
+// case n @ Node(l, v, r) => if (v < value) {
+// Node(l, v, insert(r, value))
+// } else if (v > value) {
+// Node(insert(l, value), v, r)
+// } else {
+// n
+// }
+// }
+// } ensuring (res => contents(res) == contents(tree) ++ Set(value) && isSorted(res))
+
+// def treeMin(tree: Node): Int = {
+// require(isSorted(tree))
+// tree match {
+// case Node(left, v, _) => left match {
+// case Leaf() => v
+// case n @ Node(_, _, _) => treeMin(n)
+// }
+// }
+// }
+//
+// def treeMax(tree: Node): Int = {
+// require(isSorted(tree))
+// tree match {
+// case Node(_, v, right) => right match {
+// case Leaf() => v
+// case n @ Node(_, _, _) => treeMax(n)
+// }
+// }
+// }
+
+// def remove(tree: Tree, value: Int): Node = {
+// require(isSorted(tree))
+// tree match {
+// case l @ Leaf() => l
+// case n @ Node(l, v, r) => if (v < value) {
+// Node(l, v, insert(r, value))
+// } else if (v > value) {
+// Node(insert(l, value), v, r)
+// } else {
+// n
+// }
+// }
+// } ensuring (res => contents(res) == contents(tree) -- Set(value))
+
+}
+
diff --git a/testcases/lesynth/synthesis/BinarySearchTree/BinarySearchTreeMember.scala b/testcases/lesynth/synthesis/BinarySearchTree/BinarySearchTreeMember.scala
new file mode 100644
index 000000000..416c6ef57
--- /dev/null
+++ b/testcases/lesynth/synthesis/BinarySearchTree/BinarySearchTreeMember.scala
@@ -0,0 +1,115 @@
+import scala.collection.immutable.Set
+
+import leon.Annotations._
+import leon.Utils._
+
+object BinarySearchTree {
+ sealed abstract class Tree
+ case class Node(left: Tree, value: Int, right: Tree) extends Tree
+ case class Leaf() extends Tree
+
+ def contents(tree: Tree): Set[Int] = tree match {
+ case Leaf() => Set.empty[Int]
+ case Node(l, v, r) => contents(l) ++ Set(v) ++ contents(r)
+ }
+// def isSorted(tree: Tree): Boolean = tree match {
+// case Leaf() => true
+// case Node(Leaf(), v, Leaf()) => true
+// case Node(l@Node(_, vIn, _), v, Leaf()) => v > vIn && isSorted(l)
+// case Node(Leaf(), v, r@Node(_, vIn, _)) => v < vIn && isSorted(r)
+// case Node(l@Node(_, vInLeft, _), v, r@Node(_, vInRight, _)) =>
+// v > vInLeft && v < vInRight && isSorted(l) && isSorted(r)
+// }
+//
+
+ def isSorted(tree: Tree): Boolean =
+ isSortedMaxMin(tree, Int.MinValue, Int.MaxValue)
+
+ def max(a: Int, b: Int) = if (a < b) b else a
+
+ def min(a: Int, b: Int) = if (a > b) b else a
+
+ def isSortedMaxMin(tree: Tree, minVal: Int, maxVal: Int): Boolean = tree match {
+ case Leaf() => true
+ case Node(left, v, right) =>
+ minVal < v && v < maxVal &&
+ // go left, update upper bound
+ isSortedMaxMin(left, minVal, min(maxVal, v)) &&
+ isSortedMaxMin(right, max(minVal, v), maxVal)
+ }
+
+ def member(tree: Tree, value: Int): Boolean = {
+ require(isSorted(tree))
+ choose {
+ (res: Boolean) =>
+ (
+ if (res) (contents(tree) == contents(tree) ++ Set(value))
+ else !(contents(tree) == contents(tree) ++ Set(value))
+ )
+ }
+ }
+
+// def member(tree: Tree, value: Int): Boolean = {
+// require(isSorted(tree))
+// tree match {
+// case Leaf() => false
+// case n @ Node(l, v, r) => if (v < value) {
+// member(r, value)
+// } else if (v > value) {
+// member(l, value)
+// } else {
+// true
+// }
+// }
+// } ensuring (_ || !(contents(tree) == contents(tree) ++ Set(value)))
+//
+// def insert(tree: Tree, value: Int): Node = {
+// require(isSorted(tree))
+// tree match {
+// case Leaf() => Node(Leaf(), value, Leaf())
+// case n @ Node(l, v, r) => if (v < value) {
+// Node(l, v, insert(r, value))
+// } else if (v > value) {
+// Node(insert(l, value), v, r)
+// } else {
+// n
+// }
+// }
+// } ensuring (res => contents(res) == contents(tree) ++ Set(value) && isSorted(res))
+
+ // def treeMin(tree: Node): Int = {
+ // require(isSorted(tree).sorted)
+ // tree match {
+ // case Node(left, v, _) => left match {
+ // case Leaf() => v
+ // case n@Node(_, _, _) => treeMin(n)
+ // }
+ // }
+ // }
+ //
+ // def treeMax(tree: Node): Int = {
+ // require(isSorted(tree).sorted)
+ // tree match {
+ // case Node(_, v, right) => right match {
+ // case Leaf() => v
+ // case n@Node(_, _, _) => treeMax(n)
+ // }
+ // }
+ // }
+
+// def remove(tree: Tree, value: Int): Node = {
+// require(isSorted(tree))
+// tree match {
+// case l @ Leaf() => l
+// case n @ Node(l, v, r) => if (v < value) {
+// Node(l, v, insert(r, value))
+// } else if (v > value) {
+// Node(insert(l, value), v, r)
+// } else {
+// n
+// }
+// }
+// } ensuring (contents(_) == contents(tree) -- Set(value))
+
+}
+
diff --git a/testcases/lesynth/synthesis/InsertionSort/InsertionSortInsert.scala b/testcases/lesynth/synthesis/InsertionSort/InsertionSortInsert.scala
new file mode 100644
index 000000000..ac832856e
--- /dev/null
+++ b/testcases/lesynth/synthesis/InsertionSort/InsertionSortInsert.scala
@@ -0,0 +1,61 @@
+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
+
+ 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 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))
+ }
+
+ /* 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))
+ choose { (res : List) =>
+ (
+ contents(res) == contents(l) ++ Set(e) &&
+ isSorted(res) &&
+ size(res) == size(l) + 1
+ )
+ }
+// val cond1: Boolean = /*!*/
+// l match {
+// case Nil() => /*!*/ // Cons(e,Nil())
+// case Cons(x,xs) =>
+// val cond2: Boolean = /*!*/
+// 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
+// )
+
+ /* 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)
+ )
+
+}
diff --git a/testcases/lesynth/synthesis/InsertionSort/InsertionSortSort.scala b/testcases/lesynth/synthesis/InsertionSort/InsertionSortSort.scala
new file mode 100644
index 000000000..7daae9703
--- /dev/null
+++ b/testcases/lesynth/synthesis/InsertionSort/InsertionSortSort.scala
@@ -0,0 +1,57 @@
+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
+
+ 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 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))
+ }
+
+ /* 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
+)
+
+ /* Insertion sort yields a sorted list of same size and content as the input
+ * list */
+ def xxsort(l: List): List = choose {
+ (res : List) =>
+ contents(res) == contents(l) &&
+ isSorted(res) &&
+ size(res) == size(l)
+// val cond: Boolean = /*!*/
+// case Nil() => /*!*/ // Nil()
+// case Cons(x,xs) => /*!*/ // sortedIns(x, sort(xs))
+ }
+// ensuring(res => contents(res) == contents(l)
+// && isSorted(res)
+// && size(res) == size(l)
+// )
+
+}
diff --git a/testcases/lesynth/synthesis/List/ListConcat.scala b/testcases/lesynth/synthesis/List/ListConcat.scala
new file mode 100644
index 000000000..96a2d909a
--- /dev/null
+++ b/testcases/lesynth/synthesis/List/ListConcat.scala
@@ -0,0 +1,20 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def concat(l1: List, l2: List) : List = choose {
+ (out : List) =>
+ content(out) == content(l1) ++ content(l2)
+ }
+
+}
diff --git a/testcases/lesynth/synthesis/List/ListSearch.scala b/testcases/lesynth/synthesis/List/ListSearch.scala
new file mode 100644
index 000000000..c70269a41
--- /dev/null
+++ b/testcases/lesynth/synthesis/List/ListSearch.scala
@@ -0,0 +1,50 @@
+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 Option
+ case class Some(i: Int) extends Option
+ case object None extends Option
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil() => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+//
+// def isEmpty(l: List) = l match {
+// case Nil() => true
+// case Cons(_, _) => false
+// }
+
+
+ def linearSearch(l: List, c: Int): Option = {
+ l match {
+ case Nil() => None
+ case Cons(lHead, lTail) =>
+ if (lHead == c) Some(size(l))
+ else Some(linearSearch(lTail, c))
+ }
+ } ensuring(res => if(res > -1) atInd(l, size(l) - res) == c else !content(l).contains(c))
+
+ def atInd(l: List, ind: Int): Int = {
+ require(ind >= 0 && ind < size(l))
+
+ l match {
+ case Nil() => -1
+ case Cons(lHead, lTail) =>
+ if (ind == 0) lHead
+ else atInd(lTail, ind - 1)
+ }
+
+ } ensuring( res =>
+ if (size(l) == 0) res == -1 else content(l).contains(res)
+ )
+}
diff --git a/testcases/lesynth/synthesis/MergeSort/MergeSortMerge.scala b/testcases/lesynth/synthesis/MergeSort/MergeSortMerge.scala
new file mode 100644
index 000000000..8b2582192
--- /dev/null
+++ b/testcases/lesynth/synthesis/MergeSort/MergeSortMerge.scala
@@ -0,0 +1,55 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object MergeSort {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ sealed abstract class PairAbs
+ case class Pair(fst : List, snd : List) extends PairAbs
+
+ def contents(l : List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l : List) : Boolean = l match {
+ case Nil() => true
+ case Cons(x,xs) => xs match {
+ case Nil() => true
+ case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
+ }
+ }
+
+ def size(list : List) : Int = list match {
+ case Nil() => 0
+ case Cons(x,xs) => 1 + size(xs)
+ }
+
+ def merge(aList : List, bList : List) : List = {
+ require(isSorted(aList) && isSorted(bList))
+ choose( (res: List) =>
+ ensuring(res => contents(res) == contents(aList) ++ contents(bList) && isSorted(res))
+ )
+ }
+
+// def merge(aList : List, bList : List) : List = {
+// require(isSorted(aList) && isSorted(bList))
+//
+// bList match {
+// case Nil() => aList
+// case Cons(x,xs) =>
+// aList match {
+// case Nil() => bList
+// case Cons(y,ys) =>
+// if (y < x)
+// Cons(y,merge(ys, bList))
+// else
+// Cons(x,merge(aList, xs))
+// }
+// }
+// } ensuring(res => contents(res) == contents(aList) ++ contents(bList) && isSorted(res))
+
+}
diff --git a/testcases/lesynth/synthesis/MergeSort/MergeSortSort.scala b/testcases/lesynth/synthesis/MergeSort/MergeSortSort.scala
new file mode 100644
index 000000000..987c538c4
--- /dev/null
+++ b/testcases/lesynth/synthesis/MergeSort/MergeSortSort.scala
@@ -0,0 +1,86 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object MergeSort {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ sealed abstract class PairAbs
+ case class Pair(fst : List, snd : List) extends PairAbs
+
+ def contents(l : List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l : List) : Boolean = l match {
+ case Nil() => true
+ case Cons(x,xs) => xs match {
+ case Nil() => true
+ case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
+ }
+ }
+
+ def size(list : List) : Int = list match {
+ case Nil() => 0
+ case Cons(x,xs) => 1 + size(xs)
+ }
+
+ def splithelper(aList : List, bList : List, n : Int) : Pair = {
+ if (n <= 0) Pair(aList,bList)
+ else
+ bList match {
+ case Nil() => Pair(aList,bList)
+ case Cons(x,xs) => splithelper(Cons(x,aList),xs,n-1)
+ }
+ } ensuring(res => contents(aList) ++ contents(bList) == contents(res.fst) ++ contents(res.snd))
+
+// def split(list : List, n : Int): Pair = {
+// splithelper(Nil(),list,n)
+// } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+ def split(list: List): Pair = {
+ splithelper(Nil(),list,size(list)/2)
+ } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+ def merge(aList : List, bList : List) : List = {
+ require(isSorted(aList) && isSorted(bList))
+ bList match {
+ case Nil() => aList
+ case Cons(x,xs) =>
+ aList match {
+ case Nil() => bList
+ case Cons(y,ys) =>
+ if (y < x)
+ Cons(y,merge(ys, bList))
+ else
+ Cons(x,merge(aList, xs))
+ }
+ }
+ } ensuring(res => contents(res) == contents(aList) ++ contents(bList) && isSorted(res))
+
+ def isEmpty(list: List) : Boolean = list match {
+ case Nil() => true
+ case Cons(x,xs) => false
+ }
+
+ def sort(list : List) : List = choose {
+
+ (res : List) =>
+ contents(res) == contents(list) && isSorted(res)
+
+// list match {
+// case Nil() => list
+// case Cons(x,Nil()) => list
+// case _ =>
+// val p = split(list,size(list)/2)
+// merge(mergeSort(p.fst), mergeSort(p.snd))
+
+// merge(mergeSort(split(list).fst), mergeSort(split(list).snd))
+ }
+
+ //ensuring(res => contents(res) == contents(list) && isSorted(res))
+
+}
diff --git a/testcases/lesynth/synthesis/MergeSort/MergeSortSortWithVal.scala b/testcases/lesynth/synthesis/MergeSort/MergeSortSortWithVal.scala
new file mode 100644
index 000000000..2cccf5c98
--- /dev/null
+++ b/testcases/lesynth/synthesis/MergeSort/MergeSortSortWithVal.scala
@@ -0,0 +1,85 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object MergeSort {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ sealed abstract class PairAbs
+ case class Pair(fst : List, snd : List) extends PairAbs
+
+ def contents(l : List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l : List) : Boolean = l match {
+ case Nil() => true
+ case Cons(x,xs) => xs match {
+ case Nil() => true
+ case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
+ }
+ }
+
+ def size(list : List) : Int = list match {
+ case Nil() => 0
+ case Cons(x,xs) => 1 + size(xs)
+ }
+
+ def splithelper(aList : List, bList : List, n : Int) : Pair = {
+ if (n <= 0) Pair(aList,bList)
+ else
+ bList match {
+ case Nil() => Pair(aList,bList)
+ case Cons(x,xs) => splithelper(Cons(x,aList),xs,n-1)
+ }
+ } ensuring(res => contents(aList) ++ contents(bList) == contents(res.fst) ++ contents(res.snd))
+
+// def split(list : List, n : Int): Pair = {
+// splithelper(Nil(),list,n)
+// } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+ def split(list: List): Pair = {
+ splithelper(Nil(),list,size(list)/2)
+ } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+ def merge(aList : List, bList : List) : List = {
+ require(isSorted(aList) && isSorted(bList))
+ bList match {
+ case Nil() => aList
+ case Cons(x,xs) =>
+ aList match {
+ case Nil() => bList
+ case Cons(y,ys) =>
+ if (y < x)
+ Cons(y,merge(ys, bList))
+ else
+ Cons(x,merge(aList, xs))
+ }
+ }
+ } ensuring(res => contents(res) == contents(aList) ++ contents(bList) && isSorted(res))
+
+ def isEmpty(list: List) : Boolean = list match {
+ case Nil() => true
+ case Cons(x,xs) => false
+ }
+
+ def sort(list : List) : List =
+ list match {
+ case Nil() => list
+ case Cons(_,Nil()) => list
+ case _ => {
+ val p = split(list)
+ choose {(res : List) =>
+ contents(res) == contents(list) && isSorted(res)
+ }
+ }
+ }
+
+// merge(mergeSort(split(list).fst), mergeSort(split(list).snd))
+
+ //ensuring(res => contents(res) == contents(list) && isSorted(res))
+
+}
diff --git a/testcases/lesynth/synthesis/Other/AddressesMakeAddressBook.scala b/testcases/lesynth/synthesis/Other/AddressesMakeAddressBook.scala
new file mode 100644
index 000000000..6b9a73a9c
--- /dev/null
+++ b/testcases/lesynth/synthesis/Other/AddressesMakeAddressBook.scala
@@ -0,0 +1,103 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+ case class Info(
+ address: Int,
+ zipcode: Int,
+ local: Boolean
+ )
+
+ case class Address(info: Info, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def isEmpty(ab: AddressBook) = size(ab) == 0
+
+ def content(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// !hasPrivate(res.business) &&
+// hasPrivate(res.pers)
+// }
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+//
+// def makeAddressBook(l: List): AddressBook =
+// choose {
+// (res: AddressBook) =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+
+ def makeAddressBook(l: List): AddressBook =
+ choose {
+ (res: AddressBook) =>
+ size(res) == size(l) && addressBookInvariant(res)
+ }
+
+}
diff --git a/testcases/lesynth/synthesis/Other/AddressesMakeAddressBookWithHelpers.scala b/testcases/lesynth/synthesis/Other/AddressesMakeAddressBookWithHelpers.scala
new file mode 100644
index 000000000..c22541f8c
--- /dev/null
+++ b/testcases/lesynth/synthesis/Other/AddressesMakeAddressBookWithHelpers.scala
@@ -0,0 +1,106 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+
+ case class Address(a: Int, b: Int, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+
+ def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+
+ def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def content(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+ def merge(l1: List, l2: List): List = l1 match {
+ case Nil => l2
+ case Cons(a, tail) => Cons(a, merge(tail, l2))
+ }
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// !hasPrivate(res.business) &&
+// hasPrivate(res.pers)
+// }
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+//
+// def makeAddressBook(l: List): AddressBook =
+// choose {
+// (res: AddressBook) =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+
+ def makeAddressBook(l: List): AddressBook =
+ choose {
+ (res: AddressBook) =>
+ size(res) == size(l) &&
+ allPrivate(res.pers) && allBusiness(res.business) &&
+ content(res) == content(l)
+ }
+
+}
diff --git a/testcases/lesynth/synthesis/Other/AddressesMergeAddressBooks.scala b/testcases/lesynth/synthesis/Other/AddressesMergeAddressBooks.scala
new file mode 100644
index 000000000..0d6d8c067
--- /dev/null
+++ b/testcases/lesynth/synthesis/Other/AddressesMergeAddressBooks.scala
@@ -0,0 +1,81 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+ case class Info(
+ address: Int,
+ zipcode: Int,
+ phoneNumber: Int
+ )
+
+ case class Address(info: Info, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+
+ def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+
+ def isEmpty(ab: AddressBook) = size(ab) == 0
+
+ def content(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+ def makeAddressBook(l: List): AddressBook = (l match {
+ case Nil => AddressBook(Nil, Nil)
+ case Cons(a, l1) => {
+ val res = makeAddressBook(l1)
+ if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+ else AddressBook(Cons(a, res.business), res.pers)
+ }
+ }) ensuring {
+ (res: AddressBook) =>
+ size(res) == size(l) && addressBookInvariant(res)
+ }
+
+ def merge(l1: List, l2: List): List = l1 match {
+ case Nil => l2
+ case Cons(a, tail) => Cons(a, merge(tail, l2))
+ }
+
+ def mergeAddressBooks(ab1: AddressBook, ab2: AddressBook) = {
+ require(addressBookInvariant(ab1) && addressBookInvariant(ab2))
+ choose {
+ (res: AddressBook) =>
+ (size(res) == size(ab1) + size(ab2)) && addressBookInvariant(res)
+ }
+ }
+
+}
diff --git a/testcases/lesynth/synthesis/RedBlackTree/RedBlackTree.scala b/testcases/lesynth/synthesis/RedBlackTree/RedBlackTree.scala
new file mode 100644
index 000000000..f72664258
--- /dev/null
+++ b/testcases/lesynth/synthesis/RedBlackTree/RedBlackTree.scala
@@ -0,0 +1,81 @@
+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
+
+ 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)
+ }
+
+ /* 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)
+ }
+
+ 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)))
+
+ // <<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))
+
+}
diff --git a/testcases/lesynth/synthesis/RedBlackTree/RedBlackTreeInsert.scala b/testcases/lesynth/synthesis/RedBlackTree/RedBlackTreeInsert.scala
new file mode 100644
index 000000000..e6413ffaf
--- /dev/null
+++ b/testcases/lesynth/synthesis/RedBlackTree/RedBlackTreeInsert.scala
@@ -0,0 +1,77 @@
+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
+
+ 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)
+ }
+
+ /* 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)
+ }
+
+ 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)))
+
+ // <<insert element x into the tree t>>
+ def ins(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ choose { (res: Tree) =>
+ content(res) == content(t) ++ Set(x) &&
+ size (t) <= size(res) && size(res) <= size(t) + 1 &&
+ redDescHaveBlackChildren (res) &&
+ blackBalanced (res)
+ }
+ }
+
+}
\ No newline at end of file
diff --git a/testcases/lesynth/test/Addresses.scala b/testcases/lesynth/test/Addresses.scala
new file mode 100644
index 000000000..52260559c
--- /dev/null
+++ b/testcases/lesynth/test/Addresses.scala
@@ -0,0 +1,52 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+
+ case class Address(aComp: Int, bComp: Int, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def setA(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(a, l1) => Set(a) ++ setA(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+
+ def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+
+ def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def makeAddressBook(l: List): AddressBook =
+ choose {
+ (res: AddressBook) =>
+ size(res) == size(l) &&
+ allPrivate(res.pers) && allBusiness(res.business)
+ }
+
+}
diff --git a/testcases/lesynth/test/AddressesMergeAddressBooks.scala b/testcases/lesynth/test/AddressesMergeAddressBooks.scala
new file mode 100644
index 000000000..d308ac247
--- /dev/null
+++ b/testcases/lesynth/test/AddressesMergeAddressBooks.scala
@@ -0,0 +1,70 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+
+ case class Address(a: Int, b: Int, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def setA(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(a, l1) => Set(a) ++ setA(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+
+ def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+
+ def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def makeAddressBook(l: List): AddressBook = (l match {
+ case Nil => AddressBook(Nil, Nil)
+ case Cons(a, l1) => {
+ val res = makeAddressBook(l1)
+ if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+ else AddressBook(Cons(a, res.business), res.pers)
+ }
+ }) ensuring {
+ (res: AddressBook) =>
+ size(res) == size(l) &&
+ allPrivate(res.pers) && allBusiness(res.business)
+ }
+
+ def merge(l1: List, l2: List): List = l1 match {
+ case Nil => l2
+ case Cons(a, tail) => Cons(a, merge(tail, l2))
+ }
+
+ def mergeAddressBooks(ab1: AddressBook, ab2: AddressBook) =
+ choose {
+ (res: AddressBook) =>
+ size(res) == size(ab1) + size(ab2) &&
+ allPrivate(res.pers) && allBusiness(res.business)
+ }
+
+}
diff --git a/testcases/lesynth/test/refinement/ListConcat.scala b/testcases/lesynth/test/refinement/ListConcat.scala
new file mode 100644
index 000000000..96a2d909a
--- /dev/null
+++ b/testcases/lesynth/test/refinement/ListConcat.scala
@@ -0,0 +1,20 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def concat(l1: List, l2: List) : List = choose {
+ (out : List) =>
+ content(out) == content(l1) ++ content(l2)
+ }
+
+}
diff --git a/testcases/lesynth/test/refinement/ListConcatWithEmpty.scala b/testcases/lesynth/test/refinement/ListConcatWithEmpty.scala
new file mode 100644
index 000000000..336fd7e68
--- /dev/null
+++ b/testcases/lesynth/test/refinement/ListConcatWithEmpty.scala
@@ -0,0 +1,37 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def isEmpty(l: List) = l match {
+ case Nil() => true
+ case Cons(head, tail) => false
+ }
+
+ def isEmptyBad(l: List) = l match {
+ case Nil() => true
+ case Cons(head, tail) => true
+ }
+
+ def hasContent(l: List) = l match {
+ case Nil() => false
+ case Cons(head, tail) => true
+ }
+
+// !content(l).isEmpty
+
+ def concat(l1: List, l2: List) : List = choose {
+ (out : List) =>
+ content(out) == content(l1) ++ content(l2)
+ }
+
+}
diff --git a/testcases/lesynth/test/verifier/BinarySearchTree.scala b/testcases/lesynth/test/verifier/BinarySearchTree.scala
new file mode 100644
index 000000000..3ddc3fba8
--- /dev/null
+++ b/testcases/lesynth/test/verifier/BinarySearchTree.scala
@@ -0,0 +1,65 @@
+import scala.collection.immutable.Set
+
+import leon.Annotations._
+import leon.Utils._
+
+object BinarySearchTree {
+ sealed abstract class Tree
+ case class Node(left: Tree, value: Int, right: Tree) extends Tree
+ case class Leaf() extends Tree
+
+ def contents(tree: Tree): Set[Int] = tree match {
+ case Leaf() => Set.empty[Int]
+ case Node(l, v, r) => contents(l) ++ Set(v) ++ contents(r)
+ }
+
+ def isSorted(tree: Tree): Boolean = tree match {
+ case Leaf() => true
+ case Node(Leaf(), v, Leaf()) => true
+ case Node(l@Node(_, vIn, _), v, Leaf()) => v > vIn && isSorted(l)
+ case Node(Leaf(), v, r@Node(_, vIn, _)) => v < vIn && isSorted(r)
+ case Node(l@Node(_, vInLeft, _), v, r@Node(_, vInRight, _)) =>
+ v > vInLeft && v < vInRight && isSorted(l) && isSorted(r)
+ }
+
+ def member(tree: Tree, value: Int): Boolean = {
+ require(isSorted(tree))
+ choose {
+ (res: Boolean) =>
+ (
+ if (res) (contents(tree) == contents(tree) ++ Set(value))
+ else !(contents(tree) == contents(tree) ++ Set(value))
+ )
+ }
+ }
+
+ def goodMember(tree: Tree, value: Int): Boolean = {
+ require(isSorted(tree))
+ tree match {
+ case Leaf() => false
+ case n @ Node(l, v, r) => if (v < value) {
+ member(r, value)
+ } else if (v > value) {
+ member(l, value)
+ } else {
+ true
+ }
+ }
+ } ensuring (_ || !(contents(tree) == contents(tree) ++ Set(value)))
+
+ def badMember(tree: Tree, value: Int): Boolean = {
+ require(isSorted(tree))
+ tree match {
+ case Leaf() => false
+ case n @ Node(l, v, r) => if (v <= value) {
+ member(r, value)
+ } else if (v > value) {
+ member(l, value)
+ } else {
+ true
+ }
+ }
+ } ensuring (_ || !(contents(tree) == contents(tree) ++ Set(value)))
+
+}
+
diff --git a/testcases/lesynth/test/verifier/ListConcat.scala b/testcases/lesynth/test/verifier/ListConcat.scala
new file mode 100644
index 000000000..39b756d84
--- /dev/null
+++ b/testcases/lesynth/test/verifier/ListConcat.scala
@@ -0,0 +1,44 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def content(l: List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def concat(l1: List, l2: List) : List = choose {
+ (out : List) =>
+ content(out) == content(l1) ++ content(l2)
+ }
+
+ def goodConcat1(l1: List, l2: List) : List =
+ l1 match {
+ case Nil() => l2
+ case Cons(l1Head, l1Tail) =>
+ l1 match {
+ case Nil() => l2
+ case _ => Cons(l1Head, Cons(l1Head, concat(l1Tail, l2)))
+ }
+ }
+
+ def goodConcat2(l1: List, l2: List) : List =
+ l1 match {
+ case Nil() => l2
+ case Cons(l1Head, l1Tail) =>
+ Cons(l1Head, Cons(l1Head, concat(l1Tail, l2)))
+ }
+
+ def badConcat1(l1: List, l2: List) : List =
+ l1 match {
+ case Nil() => l1
+ case Cons(l1Head, l1Tail) =>
+ Cons(l1Head, Cons(l1Head, concat(l1Tail, l2)))
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala
new file mode 100644
index 000000000..027d90bcb
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala
@@ -0,0 +1,103 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+ case class Info(
+ address: Int,
+ zipcode: Int,
+ local: Boolean
+ )
+
+ case class Address(info: Info, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def sizeA(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def isEmpty(ab: AddressBook) = sizeA(ab) == 0
+
+ def content(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// !hasPrivate(res.business) &&
+// hasPrivate(res.pers)
+// }
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+//
+// def makeAddressBook(l: List): AddressBook =
+// choose {
+// (res: AddressBook) =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+
+ def makeAddressBook(l: List): AddressBook =
+ choose {
+ (res: AddressBook) =>
+ sizeA(res) == size(l) && addressBookInvariant(res)
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala
new file mode 100644
index 000000000..579c6d4b7
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala
@@ -0,0 +1,129 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+ case class Info(
+ address: Int,
+ zipcode: Int,
+ local: Boolean
+ )
+
+ case class Address(info: Info, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def sizeA(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+// def isEmpty(ab: AddressBook) = sizeA(ab) == 0
+
+ def contentA(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// !hasPrivate(res.business) &&
+// hasPrivate(res.pers)
+// }
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+//
+// def makeAddressBook(l: List): AddressBook =
+// choose {
+// (res: AddressBook) =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+
+/*
+ // MANUAL SOLUTION:
+ def makeAB(l:List) : AddressBook = {
+ l match {
+ case Nil => AddressBook(Nil,Nil)
+ case Cons(a,t) => {
+ val ab1 = makeAB(t)
+ if (a.priv) AddressBook(ab1.business, Cons(a,ab1.pers))
+ else AddressBook(Cons(a,ab1.business), ab1.pers)
+ }
+ }
+ } ensuring((res: AddressBook) =>
+ sizeA(res) == size(l) &&
+ addressBookInvariant(res) &&
+ contentA(res) == content(l))
+
+*/
+
+/* // Perhaps this can be useful?
+ def cond(b:Boolean, ab1: AddressBook, ab2: AddressBook) : AddressBook = {
+ if (b) ab1 else ab2
+ }
+*/
+
+ def makeAddressBook(l: List): AddressBook =
+ choose {
+ (res: AddressBook) =>
+ sizeA(res) == size(l) &&
+ addressBookInvariant(res) &&
+ contentA(res) == content(l)
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala
new file mode 100644
index 000000000..e47b26007
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala
@@ -0,0 +1,113 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+ case class Info(
+ address: Int,
+ zipcode: Int,
+ local: Boolean
+ )
+
+ case class Address(info: Info, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def sizeA(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def isEmpty(ab: AddressBook) = sizeA(ab) == 0
+
+ def content(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// !hasPrivate(res.business) &&
+// hasPrivate(res.pers)
+// }
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+//
+// def makeAddressBook(l: List): AddressBook =
+// choose {
+// (res: AddressBook) =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+
+ def makeAddressBook(l: List): AddressBook = {
+ l match {
+ case Nil => AddressBook(Nil,l)
+ case Cons(h,t) => {
+ if (allPrivate(t))
+ AddressBook(Nil, Cons(Address(h.info, allPrivate(t)), t))
+ else
+ AddressBook(Cons(Address(h.info, isEmpty(makeAddressBook(t))),
+ makeAddressBook(t).business),
+ makeAddressBook(t).pers)
+ }
+ }
+ } ensuring ((res: AddressBook) =>
+ sizeA(res) == size(l) && addressBookInvariant(res))
+
+}
+
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala
new file mode 100644
index 000000000..98bb95f59
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala
@@ -0,0 +1,106 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+
+ case class Address(a: Int, b: Int, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+
+ def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+
+ def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def contentA(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+ def merge(l1: List, l2: List): List = l1 match {
+ case Nil => l2
+ case Cons(a, tail) => Cons(a, merge(tail, l2))
+ }
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// !hasPrivate(res.business) &&
+// hasPrivate(res.pers)
+// }
+
+// def makeAddressBook(l: List): AddressBook = (l match {
+// case Nil => AddressBook(Nil, Nil)
+// case Cons(a, l1) => {
+// val res = makeAddressBook(l1)
+// if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+// else AddressBook(Cons(a, res.business), res.pers)
+// }
+// }) ensuring {
+// res =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+//
+// def makeAddressBook(l: List): AddressBook =
+// choose {
+// (res: AddressBook) =>
+// size(res) == size(l) &&
+// (if (size(res.business) > 0) {
+// !hasPrivate(res.business)
+// } else true ) &&
+// (if (size(res.pers) > 0) {
+// hasPrivate(res.pers)
+// } else true )
+// }
+
+ def makeAddressBook(l: List): AddressBook =
+ choose {
+ (res: AddressBook) =>
+ size(res) == size(l) &&
+ allPrivate(res.pers) && allBusiness(res.business) &&
+ contentA(res) == content(l)
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala
new file mode 100644
index 000000000..8cb51d248
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala
@@ -0,0 +1,78 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+ case class Info(
+ address: Int,
+ zipcode: Int,
+ phoneNumber: Int
+ )
+
+ case class Address(info: Info, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def sizeA(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def addToPers(ab: AddressBook, adr: Address) = ({
+ require(addressBookInvariant(ab))
+ AddressBook(ab.business, Cons(adr, ab.pers))
+ }) ensuring(res => addressBookInvariant(res))
+
+ def addToBusiness(ab: AddressBook, adr: Address) = ({
+ require(addressBookInvariant(ab))
+ AddressBook(Cons(adr, ab.business), ab.pers)
+ }) ensuring(res => addressBookInvariant(res))
+
+ def isEmpty(ab: AddressBook) = sizeA(ab) == 0
+
+ def contentA(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+ def merge(l1: List, l2: List): List = (l1 match {
+ case Nil => l2
+ case Cons(a, tail) => Cons(a, merge(tail, l2))
+ }) ensuring(res => size(res)==size(l1) + size(l2) &&
+ (!allPrivate(l1) || !allPrivate(l2) || allPrivate(res)) &&
+ (!allBusiness(l1) || !allBusiness(l2) || !allBusiness(res))
+ )
+
+ def mergeAddressBooks(ab1: AddressBook, ab2: AddressBook) = {
+ require(addressBookInvariant(ab1) && addressBookInvariant(ab2))
+ choose {
+ (res: AddressBook) =>
+ (sizeA(res) == sizeA(ab1) + sizeA(ab2)) && addressBookInvariant(res)
+ }
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala
new file mode 100644
index 000000000..e29c6dfc9
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala
@@ -0,0 +1,73 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+ case class Info(
+ address: Int,
+ zipcode: Int,
+ phoneNumber: Int
+ )
+
+ case class Address(info: Info, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+
+ def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+
+ def isEmpty(ab: AddressBook) = size(ab) == 0
+
+ def content(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+ def makeAddressBook(l: List): AddressBook = (l match {
+ case Nil => AddressBook(Nil, Nil)
+ case Cons(a, l1) => {
+ val res = makeAddressBook(l1)
+ if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+ else AddressBook(Cons(a, res.business), res.pers)
+ }
+ }) ensuring {
+ (res: AddressBook) =>
+ size(res) == size(l) && addressBookInvariant(res)
+ }
+
+ def merge(l1: List, l2: List): List = {
+ choose((res:List) => size(res) == size(l1) + size(l2) &&
+ (!allBusiness(l1) || !allBusiness(l2) ||allBusiness(res)) &&
+ (!allPrivate(l1) || !allPrivate(l2) ||allPrivate(res)))
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala
new file mode 100644
index 000000000..ddf3ca49b
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala
@@ -0,0 +1,83 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Addresses {
+ case class Info(
+ address: Int,
+ zipcode: Int,
+ phoneNumber: Int
+ )
+
+ case class Address(info: Info, priv: Boolean)
+
+ sealed abstract class List
+ case class Cons(a: Address, tail:List) extends List
+ case object Nil extends List
+
+ def content(l: List) : Set[Address] = l match {
+ case Nil => Set.empty[Address]
+ case Cons(addr, l1) => Set(addr) ++ content(l1)
+ }
+
+ def size(l: List) : Int = l match {
+ case Nil => 0
+ case Cons(head, tail) => 1 + size(tail)
+ }
+
+ def allPrivate(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) allPrivate(l1)
+ else false
+ }
+
+ def allBusiness(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(a, l1) =>
+ if (a.priv) false
+ else allBusiness(l1)
+ }
+
+ case class AddressBook(business : List, pers : List)
+
+ def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
+
+ def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+
+ def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+
+ def isEmpty(ab: AddressBook) = size(ab) == 0
+
+ def content(ab: AddressBook) : Set[Address] = content(ab.pers) ++ content(ab.business)
+
+ def addressBookInvariant(ab: AddressBook) = allPrivate(ab.pers) && allBusiness(ab.business)
+
+ def makeAddressBook(l: List): AddressBook = (l match {
+ case Nil => AddressBook(Nil, Nil)
+ case Cons(a, l1) => {
+ val res = makeAddressBook(l1)
+ if (a.priv) AddressBook(res.business, Cons(a, res.pers))
+ else AddressBook(Cons(a, res.business), res.pers)
+ }
+ }) ensuring {
+ (res: AddressBook) =>
+ size(res) == size(l) && addressBookInvariant(res)
+ }
+
+ def merge(l1: List, l2: List): List = (l1 match {
+ case Nil => l2
+ case Cons(a, tail) => Cons(a, merge(tail, l2))
+ }) ensuring(res => size(res) == size(l1) + size(l2) &&
+ (!allBusiness(l1) || !allBusiness(l2) ||allBusiness(res)) &&
+ (!allPrivate(l1) || !allPrivate(l2) ||allPrivate(res)))
+
+ def mergeAddressBooks(ab1: AddressBook, ab2: AddressBook) = {
+ require(addressBookInvariant(ab1) && addressBookInvariant(ab2))
+ choose {
+ (res: AddressBook) =>
+ (size(res) == size(ab1) + size(ab2)) && addressBookInvariant(res)
+ }
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueCheckf.scala b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueCheckf.scala
new file mode 100644
index 000000000..4faa50286
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueCheckf.scala
@@ -0,0 +1,49 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object BatchedQueue {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def content(p: Queue): Set[Int] =
+ content(p.f) ++ content(p.r)
+
+ case class Queue(f: List, r: List)
+
+ def rev_append(aList: List, bList: List): List = (aList match {
+ case Nil => bList
+ case Cons(x, xs) => rev_append(xs, Cons(x, bList))
+ }) ensuring (content(_) == content(aList) ++ content(bList))
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (content(_) == content(list))
+
+ def invariantList(q:Queue, f: List, r: List): Boolean = {
+ rev_append(q.f, q.r) == rev_append(f, r) &&
+ { if (q.f == Nil) q.r == Nil else true }
+ }
+
+ def tail(p: Queue): Queue = {
+ p.f match {
+ case Nil => p
+ case Cons(_, xs) => checkf(xs, p.r)
+ }
+ }
+
+//(f match {
+// case Nil => Queue(reverse(r), Nil)
+// case _ => Queue(f, r)
+ def checkf(f: List, r: List): Queue = {
+ choose {
+ (res: Queue) =>
+ invariantList(res, f, r)
+ }
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueFull.scala b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueFull.scala
new file mode 100644
index 000000000..1ede1397f
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueFull.scala
@@ -0,0 +1,91 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object BatchedQueue {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def content(p: Queue): Set[Int] =
+ content(p.f) ++ content(p.r)
+
+ case class Queue(f: List, r: List)
+
+ def rev_append(aList: List, bList: List): List = (aList match {
+ case Nil => bList
+ case Cons(x, xs) => rev_append(xs, Cons(x, bList))
+ }) ensuring (
+ res =>
+ content(res) == content(aList) ++ content(bList) &&
+ size(res) == size(aList) + size(bList)
+ )
+
+ def invariantList(q:Queue, f: List, r: List): Boolean = ({
+ rev_append(q.f, q.r) == rev_append(f, r)
+ }) ensuring (
+ res =>
+ true
+ )
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (
+ res =>
+ content(res) == content(list) && size(res) == size(list)
+ )
+
+ def checkf(f: List, r: List): Queue = (f match {
+ case Nil => Queue(reverse(r), Nil)
+ case _ => Queue(f, r)
+ }) ensuring {
+ res => content(res) == content(f) ++ content(r) &&
+ size(res) == size(f) + size(r) &&
+ invariantList(res, f, r)
+ }
+
+ def head(p: Queue): Set[Int] = (
+ p.f match {
+ case Nil => Set[Int]()
+ case Cons(x, xs) => Set(x)
+ }) ensuring (
+ res =>
+ if (isEmpty(p)) true
+ else content(p) == res ++ content(tail(p)))
+
+ def tail(p: Queue): Queue = {
+ require(!isEmpty(p))
+ p.f match {
+ case Nil => p
+ case Cons(_, xs) => checkf(xs, p.r)
+ }
+ } ensuring {
+ (res: Queue) => content(res) ++ head(p) == content(p) &&
+ (if (isEmpty(p)) true
+ else size(res) + 1 == size(p))
+ }
+ //
+ // def last(p: Queue): Int = {
+ // require(!isEmpty(p))
+ // p.r match {
+ // case Nil => reverse(p.f).asInstanceOf[Cons].head
+ // case Cons(x, _) => x
+ // }
+ // }
+
+ def snoc(p: Queue, x: Int): Queue =
+ checkf(p.f, Cons(x, p.r)) ensuring (
+ res =>
+ content(res) == content(p) ++ Set(x) &&
+ size(res) == size(p) + 1 &&
+ (
+ if (isEmpty(p)) true
+ else (content(tail(res)) ++ Set(x) == content(tail(res)) &&
+ size(res.f) == size(p.f))
+ )
+ )
+
+}
diff --git a/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueSnoc.scala b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueSnoc.scala
new file mode 100644
index 000000000..6541b33b5
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/BatchedQueue/BatchedQueueSnoc.scala
@@ -0,0 +1,60 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object BatchedQueue {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty
+ case Cons(head, tail) => Set(head) ++ content(tail)
+ }
+
+ def content(p: Queue): Set[Int] =
+ content(p.f) ++ content(p.r)
+
+ case class Queue(f: List, r: List)
+
+ def rev_append(aList: List, bList: List): List = (aList match {
+ case Nil => bList
+ case Cons(x, xs) => rev_append(xs, Cons(x, bList))
+ }) ensuring (content(_) == content(aList) ++ content(bList))
+
+ def reverse(list: List) = rev_append(list, Nil) ensuring (content(_) == content(list))
+
+ def invariantList(q:Queue, f: List, r: List): Boolean = {
+ rev_append(q.f, q.r) == rev_append(f, r) &&
+ { if (q.f == Nil) q.r == Nil else true }
+ }
+
+ def tail(p: Queue): Queue = {
+ p.f match {
+ case Nil => p
+ case Cons(_, xs) => checkf(xs, p.r)
+ }
+ }
+
+ def checkf(f: List, r: List): Queue = (f match {
+ case Nil => Queue(reverse(r), Nil)
+ case _ => Queue(f, r)
+ }) ensuring {
+ res => content(res) == content(f) ++ content(r)
+ }
+ //
+ // def last(p: Queue): Int = {
+ // require(!isEmpty(p))
+ // p.r match {
+ // case Nil => reverse(p.f).asInstanceOf[Cons].head
+ // case Cons(x, _) => x
+ // }
+ // }
+
+ def snoc(p: Queue, x: Int): Queue =
+ choose { (res: Queue) =>
+ content(res) == content(p) ++ Set(x) &&
+ (p.f == Nil || content(tail(res)) ++
+ Set(x) == content(tail(res)))
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Batch.scala b/testcases/synthesis/oopsla2013/BinaryTree/Batch.scala
new file mode 100644
index 000000000..0a2fb81ef
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Batch.scala
@@ -0,0 +1,36 @@
+import leon.Annotations._
+import leon.Utils._
+
+object BinaryTree {
+ sealed abstract class Tree
+ case class Node(left : Tree, value : Int, right : Tree) extends Tree
+ case object Leaf extends Tree
+
+ def content(t : Tree): Set[Int] = t match {
+ case Leaf => Set()
+ 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) + size(r) + 1
+ }
+ } ensuring { _ >= 0 }
+
+ def insert(in: Tree, v: Int): Tree = choose {
+ (res: Tree) => content(res) == content(in) ++ Set(v)
+ }
+
+ def delete(in: Tree, v: Int): Tree = choose {
+ (res: Tree) => content(res) == content(in) -- Set(v)
+ }
+
+ def union(in1: Tree, in2: Tree): Tree = choose {
+ (res: Tree) => content(res) == content(in1) ++ content(in2)
+ }
+
+ def diff(in1: Tree, in2: Tree): Tree = choose {
+ (res: Tree) => content(res) == content(in1) -- content(in2)
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/Church/Batch.scala b/testcases/synthesis/oopsla2013/Church/Batch.scala
new file mode 100644
index 000000000..491166f56
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/Church/Batch.scala
@@ -0,0 +1,25 @@
+import leon.Utils._
+object ChurchNumerals {
+ sealed abstract class Num
+ case object Z extends Num
+ case class S(pred: Num) extends Num
+
+ def value(n:Num) : Int = {
+ n match {
+ case Z => 0
+ case S(p) => 1 + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ def add(x: Num, y: Num): Num = {
+ choose { (r : Num) =>
+ value(r) == value(x) + value(y)
+ }
+ }
+
+ def distinct(x: Num, y: Num): Num = {
+ choose { (r : Num) =>
+ r != x && r != y
+ }
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/InsertionSort/Complete.scala b/testcases/synthesis/oopsla2013/InsertionSort/Complete.scala
new file mode 100644
index 000000000..f741708ad
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/InsertionSort/Complete.scala
@@ -0,0 +1,48 @@
+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
+
+ 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 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))
+ }
+
+ /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+ * the expected content and size */
+ def insert(e: Int, l: List): List = {
+ 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)
+
+ /* 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))
+
+}
diff --git a/testcases/synthesis/oopsla2013/InsertionSort/Insert.scala b/testcases/synthesis/oopsla2013/InsertionSort/Insert.scala
new file mode 100644
index 000000000..c9402ee74
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/InsertionSort/Insert.scala
@@ -0,0 +1,53 @@
+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
+
+ 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 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))
+ }
+
+ /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+ * the expected content and size */
+ def insert(e: Int, l: List): List = {
+ require(isSorted(l))
+ choose { (res: List) =>
+ (
+ contents(res) == contents(l) ++ Set(e) &&
+ isSorted(res) &&
+ size(res) == size(l) + 1)
+ }
+ // l match {
+ // case Nil() => Cons(e, Nil())
+ // case Cons(x, xs) =>
+ // if (x <= e) Cons(x, sortedIns(e, xs))
+ // else Cons(e, l)
+ // }
+ }
+
+ /* 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) => insert(x, sort(xs))
+ }) ensuring (res => contents(res) == contents(l)
+ && isSorted(res)
+ && size(res) == size(l))
+
+}
diff --git a/testcases/synthesis/oopsla2013/InsertionSort/Sort.scala b/testcases/synthesis/oopsla2013/InsertionSort/Sort.scala
new file mode 100644
index 000000000..e75c803dd
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/InsertionSort/Sort.scala
@@ -0,0 +1,52 @@
+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
+
+ 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 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))
+ }
+
+ /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+ * the expected content and size */
+ def insert(e: Int, l: List): List = {
+ require(isSorted(l))
+ l match {
+ case Nil() => Cons(e, Nil())
+ case Cons(x, xs) =>
+ if (x <= e) Cons(x, insert(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 = {
+ choose { (res: List) =>
+ ( contents(res) == contents(l)
+ && isSorted(res)
+ && size(res) == size(l))
+ }
+ }
+ // case Nil() => Nil()
+ // case Cons(x, xs) => sortedIns(x, sort(xs))
+
+}
\ No newline at end of file
diff --git a/testcases/synthesis/oopsla2013/List/Batch.scala b/testcases/synthesis/oopsla2013/List/Batch.scala
new file mode 100644
index 000000000..f008b7575
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/List/Batch.scala
@@ -0,0 +1,38 @@
+import leon.Annotations._
+import leon.Utils._
+
+object List {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty[Int]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def insert(in1: List, v: Int) = choose {
+ (out : List) =>
+ content(out) == content(in1) ++ Set(v)
+ }
+
+ def delete(in1: List, v: Int) = choose {
+ (out : List) =>
+ content(out) == content(in1) -- Set(v)
+ }
+
+ def union(in1: List, in2: List) = choose {
+ (out : List) =>
+ content(out) == content(in1) ++ content(in2)
+ }
+
+ def diff(in1: List, in2: List) = choose {
+ (out : List) =>
+ content(out) == content(in1) -- content(in2)
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/List/Split.scala b/testcases/synthesis/oopsla2013/List/Split.scala
new file mode 100644
index 000000000..5aa4a8f1f
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/List/Split.scala
@@ -0,0 +1,98 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty[Int]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def insert(in1: List, v: Int): List = {
+ Cons(v, in1)
+ } ensuring { content(_) == content(in1) ++ Set(v) }
+
+ //def insert(in1: List, v: Int) = choose {
+ // (out : List) =>
+ // content(out) == content(in1) ++ Set(v)
+ //}
+
+ def delete(in1: List, v: Int): List = {
+ in1 match {
+ case Cons(h,t) =>
+ if (h == v) {
+ delete(t, v)
+ } else {
+ Cons(h, delete(t, v))
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { content(_) == content(in1) -- Set(v) }
+
+ //def delete(in1: List, v: Int) = choose {
+ // (out : List) =>
+ // content(out) == content(in1) -- Set(v)
+ //}
+
+ def union(in1: List, in2: List): List = {
+ in1 match {
+ case Cons(h, t) =>
+ Cons(h, union(t, in2))
+ case Nil =>
+ in2
+ }
+ } ensuring { content(_) == content(in1) ++ content(in2) }
+
+ //def union(in1: List, in2: List) = choose {
+ // (out : List) =>
+ // content(out) == content(in1) ++ content(in2)
+ //}
+
+ def diff(in1: List, in2: List): List = {
+ in2 match {
+ case Nil =>
+ in1
+ case Cons(h, t) =>
+ diff(delete(in1, h), t)
+ }
+ } ensuring { content(_) == content(in1) -- content(in2) }
+
+ //def diff(in1: List, in2: List) = choose {
+ // (out : List) =>
+ // content(out) == content(in1) -- content(in2)
+ //}
+
+ 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 abs(i : Int) : Int = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ // def split(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) = split(xs)
+ // (Cons(x1, s1), Cons(x2, s2))
+ // }) ensuring(res => splitSpec(list, res))
+
+ def split(list : List) : (List,List) = {
+ choose { (res : (List,List)) => splitSpec(list, res) }
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/MergeSort/Complete.scala b/testcases/synthesis/oopsla2013/MergeSort/Complete.scala
new file mode 100644
index 000000000..a373e82ca
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/MergeSort/Complete.scala
@@ -0,0 +1,85 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object MergeSort {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class PairAbs
+ case class Pair(fst: List, snd: List) extends PairAbs
+
+ def contents(l: List): Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x, xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l: List): Boolean = l match {
+ case Nil() => true
+ case Cons(x, xs) => xs match {
+ case Nil() => true
+ case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
+ }
+ }
+
+ def size(list: List): Int = list match {
+ case Nil() => 0
+ case Cons(x, xs) => 1 + size(xs)
+ }
+
+ def splithelper(aList: List, bList: List, n: Int): Pair = {
+ if (n <= 0) Pair(aList, bList)
+ else
+ bList match {
+ case Nil() => Pair(aList, bList)
+ case Cons(x, xs) => splithelper(Cons(x, aList), xs, n - 1)
+ }
+ } ensuring (res =>
+ contents(aList) ++ contents(bList) == contents(res.fst) ++ contents(res.snd)
+ &&
+ size(aList) + size(bList) == size(res.fst) + size(res.snd)
+ )
+
+ def split(list: List): Pair = {
+ splithelper(Nil(), list, 2)
+ } ensuring (res =>
+ contents(list) == contents(res.fst) ++ contents(res.snd)
+ &&
+ size(list) == size(res.fst) + size(res.snd)
+ )
+
+ def merge(aList: List, bList: List): List = {
+ require(isSorted(aList) && isSorted(bList))
+ bList match {
+ case Nil() => aList
+ case Cons(x, xs) =>
+ aList match {
+ case Nil() => bList
+ case Cons(y, ys) =>
+ if (y < x)
+ Cons(y, merge(ys, bList))
+ else
+ Cons(x, merge(aList, xs))
+ }
+ }
+ } ensuring (res => contents(res) ==
+ contents(aList) ++ contents(bList) && isSorted(res) &&
+ size(res) == size(aList) + size(bList)
+ )
+
+ def isEmpty(list: List): Boolean = list match {
+ case Nil() => true
+ case Cons(x, xs) => false
+ }
+
+ def sort(list: List): List = {
+ list match {
+ case Nil() => list
+ case Cons(x, Nil()) => list
+ case _ =>
+ merge(sort(split(list).fst), sort(split(list).snd))
+ }
+ } ensuring (res => contents(res) == contents(list) && isSorted(res) && size(res) == size(list))
+
+}
diff --git a/testcases/synthesis/oopsla2013/MergeSort/MergeSortSort.scala b/testcases/synthesis/oopsla2013/MergeSort/MergeSortSort.scala
new file mode 100644
index 000000000..987c538c4
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/MergeSort/MergeSortSort.scala
@@ -0,0 +1,86 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object MergeSort {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ sealed abstract class PairAbs
+ case class Pair(fst : List, snd : List) extends PairAbs
+
+ def contents(l : List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l : List) : Boolean = l match {
+ case Nil() => true
+ case Cons(x,xs) => xs match {
+ case Nil() => true
+ case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
+ }
+ }
+
+ def size(list : List) : Int = list match {
+ case Nil() => 0
+ case Cons(x,xs) => 1 + size(xs)
+ }
+
+ def splithelper(aList : List, bList : List, n : Int) : Pair = {
+ if (n <= 0) Pair(aList,bList)
+ else
+ bList match {
+ case Nil() => Pair(aList,bList)
+ case Cons(x,xs) => splithelper(Cons(x,aList),xs,n-1)
+ }
+ } ensuring(res => contents(aList) ++ contents(bList) == contents(res.fst) ++ contents(res.snd))
+
+// def split(list : List, n : Int): Pair = {
+// splithelper(Nil(),list,n)
+// } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+ def split(list: List): Pair = {
+ splithelper(Nil(),list,size(list)/2)
+ } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+ def merge(aList : List, bList : List) : List = {
+ require(isSorted(aList) && isSorted(bList))
+ bList match {
+ case Nil() => aList
+ case Cons(x,xs) =>
+ aList match {
+ case Nil() => bList
+ case Cons(y,ys) =>
+ if (y < x)
+ Cons(y,merge(ys, bList))
+ else
+ Cons(x,merge(aList, xs))
+ }
+ }
+ } ensuring(res => contents(res) == contents(aList) ++ contents(bList) && isSorted(res))
+
+ def isEmpty(list: List) : Boolean = list match {
+ case Nil() => true
+ case Cons(x,xs) => false
+ }
+
+ def sort(list : List) : List = choose {
+
+ (res : List) =>
+ contents(res) == contents(list) && isSorted(res)
+
+// list match {
+// case Nil() => list
+// case Cons(x,Nil()) => list
+// case _ =>
+// val p = split(list,size(list)/2)
+// merge(mergeSort(p.fst), mergeSort(p.snd))
+
+// merge(mergeSort(split(list).fst), mergeSort(split(list).snd))
+ }
+
+ //ensuring(res => contents(res) == contents(list) && isSorted(res))
+
+}
diff --git a/testcases/synthesis/oopsla2013/MergeSort/MergeSortSortWithVal.scala b/testcases/synthesis/oopsla2013/MergeSort/MergeSortSortWithVal.scala
new file mode 100644
index 000000000..2cccf5c98
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/MergeSort/MergeSortSortWithVal.scala
@@ -0,0 +1,85 @@
+import scala.collection.immutable.Set
+
+import leon.Utils._
+
+object MergeSort {
+ sealed abstract class List
+ case class Cons(head : Int, tail : List) extends List
+ case class Nil() extends List
+
+ sealed abstract class PairAbs
+ case class Pair(fst : List, snd : List) extends PairAbs
+
+ def contents(l : List) : Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l : List) : Boolean = l match {
+ case Nil() => true
+ case Cons(x,xs) => xs match {
+ case Nil() => true
+ case Cons(y, ys) => x <= y && isSorted(Cons(y, ys))
+ }
+ }
+
+ def size(list : List) : Int = list match {
+ case Nil() => 0
+ case Cons(x,xs) => 1 + size(xs)
+ }
+
+ def splithelper(aList : List, bList : List, n : Int) : Pair = {
+ if (n <= 0) Pair(aList,bList)
+ else
+ bList match {
+ case Nil() => Pair(aList,bList)
+ case Cons(x,xs) => splithelper(Cons(x,aList),xs,n-1)
+ }
+ } ensuring(res => contents(aList) ++ contents(bList) == contents(res.fst) ++ contents(res.snd))
+
+// def split(list : List, n : Int): Pair = {
+// splithelper(Nil(),list,n)
+// } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+ def split(list: List): Pair = {
+ splithelper(Nil(),list,size(list)/2)
+ } ensuring(res => contents(list) == contents(res.fst) ++ contents(res.snd))
+
+ def merge(aList : List, bList : List) : List = {
+ require(isSorted(aList) && isSorted(bList))
+ bList match {
+ case Nil() => aList
+ case Cons(x,xs) =>
+ aList match {
+ case Nil() => bList
+ case Cons(y,ys) =>
+ if (y < x)
+ Cons(y,merge(ys, bList))
+ else
+ Cons(x,merge(aList, xs))
+ }
+ }
+ } ensuring(res => contents(res) == contents(aList) ++ contents(bList) && isSorted(res))
+
+ def isEmpty(list: List) : Boolean = list match {
+ case Nil() => true
+ case Cons(x,xs) => false
+ }
+
+ def sort(list : List) : List =
+ list match {
+ case Nil() => list
+ case Cons(_,Nil()) => list
+ case _ => {
+ val p = split(list)
+ choose {(res : List) =>
+ contents(res) == contents(list) && isSorted(res)
+ }
+ }
+ }
+
+// merge(mergeSort(split(list).fst), mergeSort(split(list).snd))
+
+ //ensuring(res => contents(res) == contents(list) && isSorted(res))
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Batch.scala b/testcases/synthesis/oopsla2013/SortedList/Batch.scala
new file mode 100644
index 000000000..adb1f6de9
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Batch.scala
@@ -0,0 +1,89 @@
+import leon.Annotations._
+import leon.Utils._
+
+object SortedList {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty[Int]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ 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 insert(in1: List, v: Int) = {
+ require(isSorted(in1))
+
+ choose {
+ (out : List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+ }
+ }
+
+ def delete(in1: List, v: Int) = {
+ require(isSorted(in1))
+
+ choose {
+ (out : List) =>
+ isSorted(in1) && (content(out) == content(in1) -- Set(v)) && isSorted(out)
+ }
+ }
+
+ def union(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+
+ choose {
+ (out : List) =>
+ && (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ }
+ }
+
+ def diff(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+
+ choose {
+ (out : List) =>
+ && (content(out) == content(in1) -- content(in2)) && isSorted(out)
+ }
+ }
+
+ // ***********************
+ // Sorting algorithms
+ // ***********************
+
+ 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 abs(i : Int) : Int = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ def sortSpec(in : List, out : List) : Boolean = {
+ content(out) == content(in) && isSorted(out)
+ }
+
+ def split(list : List) : (List,List) = {
+ choose { (res : (List,List)) => splitSpec(list, res) }
+ }
+
+ def sort(list: List): List = choose {
+ (res: List) => sortSpec(list, res)
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Complete.scala b/testcases/synthesis/oopsla2013/SortedList/Complete.scala
index b83a876a3..ca1086c4c 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Complete.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Complete.scala
@@ -23,7 +23,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- def insert1(in1: List, v: Int): List = {
+ def insert(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
case Cons(h, t) =>
@@ -32,7 +32,7 @@ object Complete {
} else if (v == h) {
in1
} else {
- Cons(h, insert1(t, v))
+ Cons(h, insert(t, v))
}
case Nil =>
Cons(v, Nil)
@@ -40,7 +40,7 @@ object Complete {
} ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- //def insert1(in1: List, v: Int) = choose {
+ //def insert(in1: List, v: Int) = choose {
// (out : List) =>
// isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out)
//}
@@ -92,7 +92,7 @@ object Complete {
require(isSorted(in1) && isSorted(in2))
in1 match {
case Cons(h1, t1) =>
- union(t1, insert1(in2, h1))
+ union(t1, insert(in2, h1))
case Nil =>
in2
}
@@ -152,7 +152,7 @@ object Complete {
def sort1(in : List) : List = (in match {
case Nil => Nil
- case Cons(x, xs) => insert1(sort1(xs), x)
+ case Cons(x, xs) => insert(sort1(xs), x)
}) ensuring(res => sortSpec(in, res))
// Not really quicksort, neither mergesort.
diff --git a/testcases/synthesis/oopsla2013/SortedList/Delete.scala b/testcases/synthesis/oopsla2013/SortedList/Delete.scala
index 1b99aeb00..c3ebd3f78 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Delete.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Delete.scala
@@ -23,7 +23,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- def insert1(in1: List, v: Int): List = {
+ def insert(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
case Cons(h, t) =>
@@ -32,7 +32,7 @@ object Complete {
} else if (v == h) {
in1
} else {
- Cons(h, insert1(t, v))
+ Cons(h, insert(t, v))
}
case Nil =>
Cons(v, Nil)
@@ -40,23 +40,6 @@ object Complete {
} ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert2(in1: List, v: Int): List = {
- require(isSorted(in1))
- in1 match {
- case Cons(h, t) =>
- if (v < h) {
- Cons(v, in1)
- } else if (v == h) {
- Cons(v, in1)
- } else {
- Cons(h, insert2(t, v))
- }
- case Nil =>
- Cons(v, Nil)
- }
-
- } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
-
// def delete(in1: List, v: Int): List = {
// require(isSorted(in1))
// in1 match {
@@ -73,8 +56,12 @@ object Complete {
// }
// } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
- def delete(in1: List, v: Int) = choose {
- (out : List) =>
- isSorted(in1) && (content(out) == content(in1) -- Set(v)) && isSorted(out)
+ def delete(in1: List, v: Int) = {
+ require(isSorted(in1))
+
+ choose {
+ (out : List) =>
+ (content(out) == content(in1) -- Set(v)) && isSorted(out)
+ }
}
}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Diff.scala b/testcases/synthesis/oopsla2013/SortedList/Diff.scala
index 4dd0df64f..e4fa1dca9 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Diff.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Diff.scala
@@ -23,7 +23,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- def insert1(in1: List, v: Int): List = {
+ def insert(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
case Cons(h, t) =>
@@ -32,7 +32,7 @@ object Complete {
} else if (v == h) {
in1
} else {
- Cons(h, insert1(t, v))
+ Cons(h, insert(t, v))
}
case Nil =>
Cons(v, Nil)
@@ -40,23 +40,6 @@ object Complete {
} ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert2(in1: List, v: Int): List = {
- require(isSorted(in1))
- in1 match {
- case Cons(h, t) =>
- if (v < h) {
- Cons(v, in1)
- } else if (v == h) {
- Cons(v, in1)
- } else {
- Cons(h, insert2(t, v))
- }
- case Nil =>
- Cons(v, Nil)
- }
-
- } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
-
def delete(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
@@ -77,7 +60,7 @@ object Complete {
require(isSorted(in1) && isSorted(in2))
in1 match {
case Cons(h1, t1) =>
- union(t1, insert1(in2, h1))
+ union(t1, insert(in2, h1))
case Nil =>
in2
}
@@ -93,9 +76,13 @@ object Complete {
// }
// } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
- def diff(in1: List, in2: List) = choose {
- (out : List) =>
- isSorted(in1) && isSorted(in2) && (content(out) == content(in1) -- content(in2)) && isSorted(out)
+ def diff(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+
+ choose {
+ (out : List) =>
+ (content(out) == content(in1) -- content(in2)) && isSorted(out)
+ }
}
}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Insert1.scala b/testcases/synthesis/oopsla2013/SortedList/Insert1.scala
index 1b9346640..f790fd50c 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Insert1.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Insert1.scala
@@ -23,7 +23,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- // def insert1(in1: List, v: Int): List = {
+ // def insert(in1: List, v: Int): List = {
// require(isSorted(in1))
// in1 match {
// case Cons(h, t) =>
@@ -32,16 +32,17 @@ object Complete {
// } else if (v == h) {
// in1
// } else {
- // Cons(h, insert1(t, v))
+ // Cons(h, insert(t, v))
// }
// case Nil =>
// Cons(v, Nil)
// }
// } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert1(in1: List, v: Int) = choose {
- (out : List) =>
- isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out)
- }
+ def insert(in1: List, v: Int) = {
+ require(isSorted(in1))
+ choose { (out : List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out) }
+ }
}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Insert2.scala b/testcases/synthesis/oopsla2013/SortedList/Insert2.scala
index 98c7331e9..14556e667 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Insert2.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Insert2.scala
@@ -39,9 +39,13 @@ object Complete {
// }
// } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
- def insert2(in1: List, v: Int) = choose {
- (out : List) =>
- isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out) && size(out) == size(in1) + 1
+ def insert2(in1: List, v: Int) = {
+ require(isSorted(in1))
+
+ choose {
+ (out : List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out) && size(out) == size(in1) + 1
+ }
}
}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Sort.scala b/testcases/synthesis/oopsla2013/SortedList/Sort.scala
index 03619f39e..721ea6fa9 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Sort.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Sort.scala
@@ -23,7 +23,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- def insert1(in1: List, v: Int): List = {
+ def insert(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
case Cons(h, t) =>
@@ -32,7 +32,7 @@ object Complete {
} else if (v == h) {
in1
} else {
- Cons(h, insert1(t, v))
+ Cons(h, insert(t, v))
}
case Nil =>
Cons(v, Nil)
@@ -40,23 +40,6 @@ object Complete {
} ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert2(in1: List, v: Int): List = {
- require(isSorted(in1))
- in1 match {
- case Cons(h, t) =>
- if (v < h) {
- Cons(v, in1)
- } else if (v == h) {
- Cons(v, in1)
- } else {
- Cons(h, insert2(t, v))
- }
- case Nil =>
- Cons(v, Nil)
- }
-
- } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
-
def delete(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
@@ -77,7 +60,7 @@ object Complete {
require(isSorted(in1) && isSorted(in2))
in1 match {
case Cons(h1, t1) =>
- insert1(union(t1, in2), h1)
+ insert(union(t1, in2), h1)
case Nil =>
in2
}
@@ -123,7 +106,7 @@ object Complete {
// def sort1(in : List) : List = (in match {
// case Nil => Nil
- // case Cons(x, xs) => insert1(sort1(xs), x)
+ // case Cons(x, xs) => insert(sort1(xs), x)
// }) ensuring(res => sortSpec(in, res))
// // Not really quicksort, neither mergesort.
diff --git a/testcases/synthesis/oopsla2013/SortedList/SortInsert.scala b/testcases/synthesis/oopsla2013/SortedList/SortInsert.scala
new file mode 100644
index 000000000..d3bf0090d
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/SortInsert.scala
@@ -0,0 +1,105 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty[Int]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ 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 insert(in1: List, v: Int): List = {
+ require(isSorted(in1))
+ in1 match {
+ case Cons(h, t) =>
+ if (v < h) {
+ Cons(v, in1)
+ } else if (v == h) {
+ in1
+ } else {
+ Cons(h, insert(t, v))
+ }
+ case Nil =>
+ Cons(v, Nil)
+ }
+
+ } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+
+ def delete(in1: List, v: Int): List = {
+ require(isSorted(in1))
+ in1 match {
+ case Cons(h,t) =>
+ if (h < v) {
+ Cons(h, delete(t, v))
+ } else if (h == v) {
+ delete(t, v)
+ } else {
+ in1
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+ def union(in1: List, in2: List): List = {
+ require(isSorted(in1) && isSorted(in2))
+ in1 match {
+ case Cons(h1, t1) =>
+ insert(union(t1, in2), h1)
+ case Nil =>
+ in2
+ }
+ } ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+ def diff(in1: List, in2: List): List = {
+ require(isSorted(in1) && isSorted(in2))
+ in2 match {
+ case Cons(h2, t2) =>
+ diff(delete(in1, h2), t2)
+ case Nil =>
+ in1
+ }
+ } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
+
+ // ***********************
+ // Sorting algorithms
+ // ***********************
+ def sortSpec(in : List, out : List) : Boolean = {
+ content(out) == content(in) && isSorted(out)
+ }
+
+ // def sort1(in : List) : List = (in match {
+ // case Nil => Nil
+ // case Cons(x, xs) => insert(sort1(xs), x)
+ // }) ensuring(res => sortSpec(in, res))
+
+ // // Not really quicksort, neither mergesort.
+ // def sort2(in : List) : List = (in match {
+ // case Nil => Nil
+ // case Cons(x, Nil) => Cons(x, Nil)
+ // case _ =>
+ // val (s1,s2) = split(in)
+ // union(sort2(s1), sort2(s2))
+ // }) ensuring(res => sortSpec(in, res))
+
+ def sort(list: List): List = choose {
+ (res: List) => sortSpec(list, res)
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/SortMerge.scala b/testcases/synthesis/oopsla2013/SortedList/SortMerge.scala
new file mode 100644
index 000000000..bf0794fe7
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/SortMerge.scala
@@ -0,0 +1,114 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def abs(i : Int) : Int = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty[Int]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ 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 delete(in1: List, v: Int): List = {
+ require(isSorted(in1))
+ in1 match {
+ case Cons(h,t) =>
+ if (h < v) {
+ Cons(h, delete(t, v))
+ } else if (h == v) {
+ delete(t, v)
+ } else {
+ in1
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+ def union(in1: List, in2: List): List = {
+ require(isSorted(in1) && isSorted(in2) && abs(size(in1)-size(in2)) <= 1)
+ (in1, in2) match {
+ case (Cons(h1, t1), Cons(h2, t2)) =>
+ if (h1 < h2) {
+ Cons(h1, union(t1, Cons(h2, t2)))
+ } else {
+ Cons(h2, union(Cons(h1, t1), t2))
+ }
+ case (Nil, l2) =>
+ l2
+ case (l1, Nil) =>
+ l1
+ }
+ } ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+ def diff(in1: List, in2: List): List = {
+ require(isSorted(in1) && isSorted(in2))
+ in2 match {
+ case Cons(h2, t2) =>
+ diff(delete(in1, h2), t2)
+ case Nil =>
+ in1
+ }
+ } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
+
+ // ***********************
+ // Sorting algorithms
+ // ***********************
+
+ 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 sortSpec(in : List, out : List) : Boolean = {
+ content(out) == content(in) && isSorted(out)
+ }
+
+
+ def split(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) = split(xs)
+ (Cons(x1, s1), Cons(x2, s2))
+ }) ensuring(res => splitSpec(list, res))
+
+ // def sort1(in : List) : List = (in match {
+ // case Nil => Nil
+ // case Cons(x, xs) => insert(sort1(xs), x)
+ // }) ensuring(res => sortSpec(in, res))
+
+ // // Not really quicksort, neither mergesort.
+ // def sort2(in : List) : List = (in match {
+ // case Nil => Nil
+ // case Cons(x, Nil) => Cons(x, Nil)
+ // case _ =>
+ // val (s1,s2) = split(in)
+ // union(sort2(s1), sort2(s2))
+ // }) ensuring(res => sortSpec(in, res))
+
+ def sort(list: List): List = choose {
+ (res: List) => sortSpec(list, res)
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/SortMergeWithHint.scala b/testcases/synthesis/oopsla2013/SortedList/SortMergeWithHint.scala
new file mode 100644
index 000000000..daff218c9
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/SortMergeWithHint.scala
@@ -0,0 +1,124 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def abs(i : Int) : Int = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty[Int]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ 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 delete(in1: List, v: Int): List = {
+ require(isSorted(in1))
+ in1 match {
+ case Cons(h,t) =>
+ if (h < v) {
+ Cons(h, delete(t, v))
+ } else if (h == v) {
+ delete(t, v)
+ } else {
+ in1
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+ def union(in1: List, in2: List): List = {
+ require(isSorted(in1) && isSorted(in2) && abs(size(in1)-size(in2)) <= 1)
+ (in1, in2) match {
+ case (Cons(h1, t1), Cons(h2, t2)) =>
+ if (h1 < h2) {
+ Cons(h1, union(t1, Cons(h2, t2)))
+ } else {
+ Cons(h2, union(Cons(h1, t1), t2))
+ }
+ case (Nil, l2) =>
+ l2
+ case (l1, Nil) =>
+ l1
+ }
+ } ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+ def diff(in1: List, in2: List): List = {
+ require(isSorted(in1) && isSorted(in2))
+ in2 match {
+ case Cons(h2, t2) =>
+ diff(delete(in1, h2), t2)
+ case Nil =>
+ in1
+ }
+ } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
+
+ // ***********************
+ // Sorting algorithms
+ // ***********************
+
+ 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 sortSpec(in : List, out : List) : Boolean = {
+ content(out) == content(in) && isSorted(out)
+ }
+
+
+ def split(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) = split(xs)
+ (Cons(x1, s1), Cons(x2, s2))
+ }) ensuring(res => splitSpec(list, res))
+
+ // def sort1(in : List) : List = (in match {
+ // case Nil => Nil
+ // case Cons(x, xs) => insert(sort1(xs), x)
+ // }) ensuring(res => sortSpec(in, res))
+
+ // // Not really quicksort, neither mergesort.
+ // def sort2(in : List) : List = (in match {
+ // case Nil => Nil
+ // case Cons(x, Nil) => Cons(x, Nil)
+ // case _ =>
+ // val (s1,s2) = split(in)
+ // union(sort2(s1), sort2(s2))
+ // }) ensuring(res => sortSpec(in, res))
+
+ def sort(list: List): List = (list match {
+ case Nil => Nil
+ case Cons(_, Nil) => list
+ case _ => split(list) match {
+ case (l1, l2) =>
+ val r1 = sort(l1)
+ val r2 = sort(l2)
+
+ choose {
+ (res: List) => sortSpec(list, res)
+ }
+ }
+ }) ensuring { res => size(res) == size(list) && sortSpec(list, res) }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split.scala b/testcases/synthesis/oopsla2013/SortedList/Split.scala
index 5d28846ea..485146c3c 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Split.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Split.scala
@@ -23,7 +23,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- def insert1(in1: List, v: Int): List = {
+ def insert(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
case Cons(h, t) =>
@@ -32,7 +32,7 @@ object Complete {
} else if (v == h) {
in1
} else {
- Cons(h, insert1(t, v))
+ Cons(h, insert(t, v))
}
case Nil =>
Cons(v, Nil)
@@ -40,23 +40,6 @@ object Complete {
} ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert2(in1: List, v: Int): List = {
- require(isSorted(in1))
- in1 match {
- case Cons(h, t) =>
- if (v < h) {
- Cons(v, in1)
- } else if (v == h) {
- Cons(v, in1)
- } else {
- Cons(h, insert2(t, v))
- }
- case Nil =>
- Cons(v, Nil)
- }
-
- } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
-
def delete(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
@@ -77,7 +60,7 @@ object Complete {
require(isSorted(in1) && isSorted(in2))
in1 match {
case Cons(h1, t1) =>
- union(t1, insert1(in2, h1))
+ union(t1, insert(in2, h1))
case Nil =>
in2
}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split1.scala b/testcases/synthesis/oopsla2013/SortedList/Split1.scala
index daa3b9deb..ef2090109 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Split1.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Split1.scala
@@ -23,7 +23,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- def insert1(in1: List, v: Int): List = {
+ def insert(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
case Cons(h, t) =>
@@ -32,7 +32,7 @@ object Complete {
} else if (v == h) {
in1
} else {
- Cons(h, insert1(t, v))
+ Cons(h, insert(t, v))
}
case Nil =>
Cons(v, Nil)
@@ -40,23 +40,6 @@ object Complete {
} ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert2(in1: List, v: Int): List = {
- require(isSorted(in1))
- in1 match {
- case Cons(h, t) =>
- if (v < h) {
- Cons(v, in1)
- } else if (v == h) {
- Cons(v, in1)
- } else {
- Cons(h, insert2(t, v))
- }
- case Nil =>
- Cons(v, Nil)
- }
-
- } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
-
def delete(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
@@ -77,7 +60,7 @@ object Complete {
require(isSorted(in1) && isSorted(in2))
in1 match {
case Cons(h1, t1) =>
- union(t1, insert1(in2, h1))
+ union(t1, insert(in2, h1))
case Nil =>
in2
}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split2.scala b/testcases/synthesis/oopsla2013/SortedList/Split2.scala
index fcdcf7b68..37192748c 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Split2.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Split2.scala
@@ -23,7 +23,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- def insert1(in1: List, v: Int): List = {
+ def insert(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
case Cons(h, t) =>
@@ -32,7 +32,7 @@ object Complete {
} else if (v == h) {
in1
} else {
- Cons(h, insert1(t, v))
+ Cons(h, insert(t, v))
}
case Nil =>
Cons(v, Nil)
@@ -40,23 +40,6 @@ object Complete {
} ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert2(in1: List, v: Int): List = {
- require(isSorted(in1))
- in1 match {
- case Cons(h, t) =>
- if (v < h) {
- Cons(v, in1)
- } else if (v == h) {
- Cons(v, in1)
- } else {
- Cons(h, insert2(t, v))
- }
- case Nil =>
- Cons(v, Nil)
- }
-
- } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
-
def delete(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
@@ -77,7 +60,7 @@ object Complete {
require(isSorted(in1) && isSorted(in2))
in1 match {
case Cons(h1, t1) =>
- union(t1, insert1(in2, h1))
+ union(t1, insert(in2, h1))
case Nil =>
in2
}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split3.scala b/testcases/synthesis/oopsla2013/SortedList/Split3.scala
index 1042be56e..f764e19e9 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Split3.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Split3.scala
@@ -23,7 +23,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- def insert1(in1: List, v: Int): List = {
+ def insert(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
case Cons(h, t) =>
@@ -32,7 +32,7 @@ object Complete {
} else if (v == h) {
in1
} else {
- Cons(h, insert1(t, v))
+ Cons(h, insert(t, v))
}
case Nil =>
Cons(v, Nil)
@@ -40,23 +40,6 @@ object Complete {
} ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert2(in1: List, v: Int): List = {
- require(isSorted(in1))
- in1 match {
- case Cons(h, t) =>
- if (v < h) {
- Cons(v, in1)
- } else if (v == h) {
- Cons(v, in1)
- } else {
- Cons(h, insert2(t, v))
- }
- case Nil =>
- Cons(v, Nil)
- }
-
- } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
-
def delete(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
@@ -77,7 +60,7 @@ object Complete {
require(isSorted(in1) && isSorted(in2))
in1 match {
case Cons(h1, t1) =>
- union(t1, insert1(in2, h1))
+ union(t1, insert(in2, h1))
case Nil =>
in2
}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Union.scala b/testcases/synthesis/oopsla2013/SortedList/Union.scala
index 394ca3a7a..5d8767c31 100644
--- a/testcases/synthesis/oopsla2013/SortedList/Union.scala
+++ b/testcases/synthesis/oopsla2013/SortedList/Union.scala
@@ -24,7 +24,7 @@ object Complete {
case Cons(_, xs) => isSorted(xs)
}
- def insert1(in1: List, v: Int): List = {
+ def insert(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
case Cons(h, t) =>
@@ -33,7 +33,7 @@ object Complete {
} else if (v == h) {
in1
} else {
- Cons(h, insert1(t, v))
+ Cons(h, insert(t, v))
}
case Nil =>
Cons(v, Nil)
@@ -41,23 +41,6 @@ object Complete {
} ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert2(in1: List, v: Int): List = {
- require(isSorted(in1))
- in1 match {
- case Cons(h, t) =>
- if (v < h) {
- Cons(v, in1)
- } else if (v == h) {
- Cons(v, in1)
- } else {
- Cons(h, insert2(t, v))
- }
- case Nil =>
- Cons(v, Nil)
- }
-
- } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) && size(res) == size(in1) + 1 }
-
def delete(in1: List, v: Int): List = {
require(isSorted(in1))
in1 match {
@@ -78,7 +61,7 @@ object Complete {
// require(isSorted(in1) && isSorted(in2))
// in1 match {
// case Cons(h1, t1) =>
- // union(t1, insert1(in2, h1))
+ // union(t1, insert(in2, h1))
// case Nil =>
// in2
// }
diff --git a/testcases/synthesis/oopsla2013/SortedList/UnionIO.scala b/testcases/synthesis/oopsla2013/SortedList/UnionIO.scala
new file mode 100644
index 000000000..ffaf5f1d1
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/UnionIO.scala
@@ -0,0 +1,52 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty[Int]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ 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 union(in1: List, in2: List): List = {
+ // require(isSorted(in1) && isSorted(in2))
+ // in1 match {
+ // case Cons(h1, t1) =>
+ // union(t1, insert(in2, h1))
+ // case Nil =>
+ // in2
+ // }
+ // } ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
+
+/*
+ def union(in1: List, in2: List) = choose {
+ (out : List) =>
+ isSorted(in1) && isSorted(in2) && (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ }
+*/
+
+ def union(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+ choose { (out : List) =>
+ (in1!= Cons(10,Cons(20,Cons(30,Cons(40,Nil)))) ||
+ in2!= Cons(11,Cons(13,Cons(25,Cons(45,Cons(48,Cons(60,Nil)))))) ||
+ out == Cons(10,Cons(11,Cons(13,Cons(20,Cons(25,Cons(30,Cons(40,Cons(45,Cons(48,Cons(60,Nil))))))))))) &&
+ (content(out) == content(in1) ++ content(in2)) && isSorted(out) }
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Batch.scala b/testcases/synthesis/oopsla2013/SparseVector/Batch.scala
new file mode 100644
index 000000000..230aa7ff2
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SparseVector/Batch.scala
@@ -0,0 +1,63 @@
+import leon.Annotations._
+import leon.Utils._
+
+object SparseVector {
+ sealed abstract class SparseVector
+ case class Cons(index: Int, value : Int, tail: SparseVector) extends SparseVector
+ case object Nil extends SparseVector
+
+ sealed abstract class Option
+ case class Some(v: Int) extends Option
+ case object None extends Option
+
+ def size(sv: SparseVector): Int = {
+ sv match {
+ case Cons(i, v, t) =>
+ 1 + size(t)
+ case Nil =>
+ 0
+ }
+ } ensuring { _ >= 0 }
+
+ def isDefined(o: Option) = o match {
+ case Some(v) => true
+ case None => false
+ }
+
+ def valueOf(o: Option) = o match {
+ case Some(v) => v
+ case None => -42
+ }
+
+ def values(sv: SparseVector): Set[Int] = sv match {
+ case Cons(i, v, t) =>
+ values(t) ++ Set(v)
+ case Nil =>
+ Set()
+ }
+
+ def indices(sv: SparseVector): Set[Int] = sv match {
+ case Cons(i, v, t) =>
+ indices(t) ++ Set(i)
+ case Nil =>
+ Set()
+ }
+
+ def invariant(sv: SparseVector): Boolean = sv match {
+ case Cons(i1, v1, t1 @ Cons(i2, v2, t2)) =>
+ (i1 < i2) && invariant(t1)
+ case _ => true
+ }
+
+ def set(sv: SparseVector, at: Int, newV: Int): SparseVector = choose {
+ (res: SparseVector) => invariant(sv) && (values(res) contains newV) && invariant(res) && (indices(res) == indices(sv) ++ Set(at))
+ }
+
+ def delete(sv: SparseVector, at: Int): SparseVector = choose {
+ (res: SparseVector) => invariant(sv) && (size(res) <= size(sv)) && invariant(res) && (indices(res) == indices(sv) -- Set(at))
+ }
+
+ def get(sv: SparseVector, at: Int): Option = choose {
+ (res: Option) => invariant(sv) && ((indices(sv) contains at) == isDefined(res)) && (!isDefined(res) || (values(sv) contains valueOf(res)))
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Batch.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Batch.scala
new file mode 100644
index 000000000..0be1a7af6
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Batch.scala
@@ -0,0 +1,46 @@
+import leon.Annotations._
+import leon.Utils._
+
+object StrictSortedList {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : Int = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[Int] = l match {
+ case Nil => Set.empty[Int]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ 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 insert(in1: List, v: Int) = choose {
+ (out : List) =>
+ isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+ }
+
+ def delete(in1: List, v: Int) = choose {
+ (out : List) =>
+ isSorted(in1) && (content(out) == content(in1) -- Set(v)) && isSorted(out)
+ }
+
+ def union(in1: List, in2: List) = choose {
+ (out : List) =>
+ isSorted(in1) && isSorted(in2) && (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ }
+
+ def diff(in1: List, in2: List) = choose {
+ (out : List) =>
+ isSorted(in1) && isSorted(in2) && (content(out) == content(in1) -- content(in2)) && isSorted(out)
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala
index a0b56fa9d..4b04ae60d 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala
@@ -56,8 +56,9 @@ object Delete {
// }
// } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
- def delete(in1: List, v: Int) = choose {
- (out : List) =>
- isSorted(in1) && (content(out) == content(in1) -- Set(v)) && isSorted(out)
+ def delete(in1: List, v: Int) = {
+ require(isSorted(in1))
+ choose {(out : List) => content(out) == content(in1) -- Set(v) &&
+ isSorted(out) }
}
}
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala
index eea2a1eac..aa38b4ca1 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala
@@ -76,9 +76,9 @@ object Complete {
// }
// } ensuring { res => content(res) == content(in1) -- content(in2) && isSorted(res) }
- def diff(in1: List, in2: List) = choose {
- (out : List) =>
- isSorted(in1) && isSorted(in2) && (content(out) == content(in1) -- content(in2)) && isSorted(out)
+ def diff(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+ choose((out : List) =>
+ content(out) == content(in1) -- content(in2) && isSorted(out))
}
-
}
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala
index 31344aec3..cac8b1551 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala
@@ -39,9 +39,10 @@ object Complete {
// }
// } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
- def insert(in1: List, v: Int) = choose {
- (out : List) =>
- isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+ def insert(in1: List, v: Int) = {
+ require(isSorted(in1))
+ choose((out : List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out))
}
}
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala
index e44158330..c990996b4 100644
--- a/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala
@@ -66,8 +66,10 @@ object Complete {
// }
//} ensuring { res => content(res) == content(in1) ++ content(in2) && isSorted(res) }
- def union(in1: List, in2: List) = choose {
- (out : List) =>
- isSorted(in1) && isSorted(in2) && (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ def union(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+ choose( (out : List) => (content(out) == content(in1) ++ content(in2)) &&
+ isSorted(out)
+ )
}
}
--
GitLab