diff --git a/testcases/synthesis/cav2013/Sorting.scala b/testcases/synthesis/cav2013/Sorting.scala
index d396c5eb700a8e9002b5b11a2e289382bb93c4a1..c9bee62a0344e2a53f2c7757c7615ebec73b93ad 100644
--- a/testcases/synthesis/cav2013/Sorting.scala
+++ b/testcases/synthesis/cav2013/Sorting.scala
@@ -40,6 +40,11 @@ object Sorting {
case LCons(x, xs) => isSorted(x) && lIsSorted(xs)
}
+ @induct
+ def sortedLemma(a: Int, x: Int, b: List) = {
+ !(isSorted(Cons(a,b)) && (content(b) contains x)) || (x >= a)
+ } holds
+
def abs(i : Int) : Int = {
if(i < 0) -i else i
} ensuring(_ >= 0)
@@ -51,18 +56,54 @@ object Sorting {
***************************/
def insertSpec(elem : Int, list : List, res : List) : Boolean = {
- isSorted(list) && // Part of precondition, really.
+// isSorted(list) && // Part of precondition, really.
isSorted(res) && content(res) == content(list) ++ Set(elem)
}
- // This will require:
- // 1) Propagation of path-conditions.
- // 2) Something like "inequality-split".
def insert(elem : Int, list : List) : List = {
require(isSorted(list))
choose { (res : List) => insertSpec(elem, list, res) }
}
+ //require(head < elem && isSorted(Cons(head, tail)) && r == insertImpl(elem, tail))
+ //require(head < elem && isSorted(Cons(head, tail)) && isSorted(r) && content(r) == content(tail) ++ Set(elem))
+ // head3;tail3;r4;elem4, ((head3 < elem4) ∧ isSorted(Cons(head3, tail3)) ∧ insertSpec(elem4, tail3, r4)) ≺ ⟨ insertSpec(elem4, Cons(head3, tail3), res) ⟩ res
+ def insertV(head: Int, tail: List, r: List, rh: Int, rt: List, elem: Int) = {
+ require(head < elem && isSorted(Cons(head, tail)) && content(tail) == content(r) && isSorted(r) && r == Cons(rh, rt) && sortedLemma(head, rh, r))
+
+ //insertSpec(elem, Cons(head, tail), Cons(head, r))
+ //rh >= head
+ isSorted(Cons(head, r))
+
+ } holds
+
+ //require(head < elem && isSorted(Cons(head, tail)) && isSorted(r) && content(r) == content(tail) ++ Set(elem))
+ // head3;tail3;r4;elem4, ((head3 < elem4) ∧ isSorted(Cons(head3, tail3)) ∧ insertSpec(elem4, tail3, r4)) ≺ ⟨ insertSpec(elem4, Cons(head3, tail3), res) ⟩ res
+ def insertV2(head: Int, tail: List, r: List, rh: Int, rt: List, elem: Int) = {
+ require(head < elem && isSorted(Cons(head, tail)) && r == insertImpl(elem, tail) && r == Cons(rh, rt))
+
+ //insertSpec(elem, Cons(head, tail), Cons(head, r))
+ rh >= head
+
+ } holds
+
+ def insert2(elem : Int, list : List) : List = {
+ require(isSorted(list))
+ list match {
+ case Cons(h, t) =>
+ val r = insert2(elem, t)
+ if (elem > h) {
+ choose { (res : List) => insertSpec(elem, Cons(h,t), res) }
+ } else if (elem < h) {
+ Cons(elem, Cons(h, t))
+ } else {
+ Cons(h, t)
+ }
+ case Nil() =>
+ Cons(elem, Nil())
+ }
+ } ensuring { res => insertSpec(elem, list, res) }
+
def insertImpl(elem : Int, list : List) : List = {
require(isSorted(list))
list match {
@@ -159,6 +200,42 @@ object Sorting {
content(out) == content(in) && isSorted(out)
}
+ def insertSorted(in: List, v: Int): List = {
+ require(isSorted(in));
+
+ in match {
+ case Cons(h, t) =>
+ val r = insertSorted(t, v)
+ if (h < v) {
+ Cons(h, r)
+ } else if (h > v) {
+ Cons(v, Cons(h, t))
+ } else {
+ Cons(h, t)
+ }
+ case _ =>
+ Cons(v, Nil())
+ }
+ } ensuring { res => isSorted(res) && content(res) == content(in) ++ Set(v) }
+
+ def insertSorted1(in: List, v: Int): List = {
+ require(isSorted(in));
+
+ in match {
+ case Cons(h, t) =>
+ val r = insertSorted(t, v)
+ if (h < v) {
+ choose { (res: List) => isSorted(res) && content(res) == content(in) ++ Set(v) }
+ } else if (h > v) {
+ Cons(v, Cons(h, t))
+ } else {
+ Cons(h, t)
+ }
+ case _ =>
+ Cons(v, Nil())
+ }
+ } ensuring { res => isSorted(res) && content(res) == content(in) ++ Set(v) }
+
def insertionSortImpl(in : List) : List = (in match {
case Nil() => Nil()
case Cons(x, xs) => insertImpl(x, insertionSortImpl(xs))
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Complete.scala b/testcases/synthesis/oopsla2013/BinaryTree/Complete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..51aebf173a3b3f07cc63a5464b80d7ea5084622c
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Complete.scala
@@ -0,0 +1,76 @@
+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 = {
+ Node(in, v, Leaf)
+ } ensuring { res => content(res) == content(in) ++ Set(v) }
+
+ //def insert(in: Tree, v: Int): Tree = choose {
+ // (res: Tree) => content(res) == content(in) ++ Set(v)
+ //}
+
+ def delete(in: Tree, v: Int): Tree = {
+ in match {
+ case Node(l, vv, r) =>
+ if (vv == v) {
+ delete(l, v) match {
+ case Node(ll, lv, lr) =>
+ Node(Node(ll, lv, lr), lv, delete(r, v))
+ case Leaf =>
+ delete(r, v)
+ }
+ } else {
+ Node(delete(l, v), vv, delete(r, v))
+ }
+ case Leaf =>
+ Leaf
+ }
+ } ensuring { res => 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 = {
+ in1 match {
+ case Node(l1, v1, r1) =>
+ insert(union(r1, union(l1, in2)), v1)
+ case Leaf =>
+ in2
+ }
+ } ensuring { res => content(res) == content(in1) ++ content(in2) }
+
+ //def union(in1: Tree, in2: Tree): Tree = choose {
+ // (res: Tree) => content(res) == content(in1) ++ content(in2)
+ //}
+
+ def diff(in1: Tree, in2: Tree): Tree = {
+ in2 match {
+ case Node(l2, v2, r2) =>
+ delete(diff(diff(in1, l2), r2), v2)
+ case Leaf =>
+ in1
+ }
+ } ensuring { res => 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/BinaryTree/Delete.scala b/testcases/synthesis/oopsla2013/BinaryTree/Delete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..219b3efab110336347c5bb879542021cc60d9159
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Delete.scala
@@ -0,0 +1,46 @@
+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 = {
+ Node(in, v, Leaf)
+ } ensuring { res => content(res) == content(in) ++ Set(v) }
+
+ // def delete(in: Tree, v: Int): Tree = {
+ // in match {
+ // case Node(l, vv, r) =>
+ // if (vv == v) {
+ // delete(l, v) match {
+ // case Node(ll, lv, lr) =>
+ // Node(Node(ll, lv, lr), lv, delete(r, v))
+ // case Leaf =>
+ // delete(r, v)
+ // }
+ // } else {
+ // Node(delete(l, v), vv, delete(r, v))
+ // }
+ // case Leaf =>
+ // Leaf
+ // }
+ // } ensuring { res => content(res) == content(in) -- Set(v) }
+
+ def delete(in: Tree, v: Int): Tree = choose {
+ (res: Tree) => content(res) == content(in) -- Set(v)
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Diff.scala b/testcases/synthesis/oopsla2013/BinaryTree/Diff.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bd31f758a75c25c58fcb26412fa1e6b191945973
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Diff.scala
@@ -0,0 +1,64 @@
+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 = {
+ Node(in, v, Leaf)
+ } ensuring { res => content(res) == content(in) ++ Set(v) }
+
+ def delete(in: Tree, v: Int): Tree = {
+ in match {
+ case Node(l, vv, r) =>
+ if (vv == v) {
+ delete(l, v) match {
+ case Node(ll, lv, lr) =>
+ Node(Node(ll, lv, lr), lv, delete(r, v))
+ case Leaf =>
+ delete(r, v)
+ }
+ } else {
+ Node(delete(l, v), vv, delete(r, v))
+ }
+ case Leaf =>
+ Leaf
+ }
+ } ensuring { res => content(res) == content(in) -- Set(v) }
+
+ def union(in1: Tree, in2: Tree): Tree = {
+ in1 match {
+ case Node(l1, v1, r1) =>
+ insert(union(r1, union(l1, in2)), v1)
+ case Leaf =>
+ in2
+ }
+ } ensuring { res => content(res) == content(in1) ++ content(in2) }
+
+ // def diff(in1: Tree, in2: Tree): Tree = {
+ // in2 match {
+ // case Node(l2, v2, r2) =>
+ // delete(diff(diff(in1, l2), r2), v2)
+ // case Leaf =>
+ // in1
+ // }
+ // } ensuring { res => 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/BinaryTree/Insert.scala b/testcases/synthesis/oopsla2013/BinaryTree/Insert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..32291ad3ed0cca370b7d5abb915f82abaf2dc5d9
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Insert.scala
@@ -0,0 +1,28 @@
+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 = {
+ // Node(in, v, Leaf)
+ //} ensuring { res => content(res) == content(in) ++ Set(v) }
+
+ def insert(in: Tree, v: Int): Tree = choose {
+ (res: Tree) => content(res) == content(in) ++ Set(v)
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/BinaryTree/Union.scala b/testcases/synthesis/oopsla2013/BinaryTree/Union.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c6252a2b7d8738cbf690c79fba50ebec594c82e1
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/BinaryTree/Union.scala
@@ -0,0 +1,55 @@
+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 = {
+ Node(in, v, Leaf)
+ } ensuring { res => content(res) == content(in) ++ Set(v) }
+
+ def delete(in: Tree, v: Int): Tree = {
+ in match {
+ case Node(l, vv, r) =>
+ if (vv == v) {
+ delete(l, v) match {
+ case Node(ll, lv, lr) =>
+ Node(Node(ll, lv, lr), lv, delete(r, v))
+ case Leaf =>
+ delete(r, v)
+ }
+ } else {
+ Node(delete(l, v), vv, delete(r, v))
+ }
+ case Leaf =>
+ Leaf
+ }
+ } ensuring { res => content(res) == content(in) -- Set(v) }
+
+ // def union(in1: Tree, in2: Tree): Tree = {
+ // in1 match {
+ // case Node(l1, v1, r1) =>
+ // insert(union(r1, union(l1, in2)), v1)
+ // case Leaf =>
+ // in2
+ // }
+ // } ensuring { res => content(res) == content(in1) ++ content(in2) }
+
+ def union(in1: Tree, in2: Tree): Tree = choose {
+ (res: Tree) => content(res) == content(in1) ++ content(in2)
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/Church/Add.scala b/testcases/synthesis/oopsla2013/Church/Add.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7b1b6b95fb9e928e031e91ac359e4f64ae1a663d
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/Church/Add.scala
@@ -0,0 +1,24 @@
+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 = (x match {
+ // case Z => y
+ // case S(p) => add(p, S(y))
+ // }) ensuring (value(_) == value(x) + value(y))
+
+ def add(x: Num, y: Num): Num = {
+ choose { (r : Num) =>
+ value(r) == value(x) + value(y)
+ }
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/Church/Complete.scala b/testcases/synthesis/oopsla2013/Church/Complete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c446c789d0b5c5347fdaa817473aa005b73659c2
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/Church/Complete.scala
@@ -0,0 +1,43 @@
+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 = (x match {
+ case Z => y
+ case S(p) => add(p, S(y))
+ }) ensuring (value(_) == value(x) + value(y))
+
+ //def add(x: Num, y: Num): Num = {
+ // choose { (r : Num) =>
+ // value(r) == value(x) + value(y)
+ // }
+ //}
+
+ def distinct(x : Num, y : Num) : Num = (x match {
+ case Z =>
+ S(y)
+
+ case S(p) =>
+ y match {
+ case Z =>
+ S(x)
+ case S(p) =>
+ Z
+ }
+ }) ensuring (res => res != x && res != y)
+
+ // def distinct(x: Num, y: Num): Num = {
+ // choose { (r : Num) =>
+ // r != x && r != y
+ // }
+ // }
+}
diff --git a/testcases/synthesis/oopsla2013/Church/Distinct.scala b/testcases/synthesis/oopsla2013/Church/Distinct.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a7a0189c20070a28393bb97be7f8066f82939662
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/Church/Distinct.scala
@@ -0,0 +1,37 @@
+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 = (x match {
+ case Z => y
+ case S(p) => add(p, S(y))
+ }) ensuring (value(_) == value(x) + value(y))
+
+ //def distinct(x : Num, y : Num) : Num = (x match {
+ // case Z =>
+ // S(y)
+
+ // case S(p) =>
+ // y match {
+ // case Z =>
+ // S(x)
+ // case S(p) =>
+ // Z
+ // }
+ //}) ensuring (res => res != x && res != y)
+
+ def distinct(x: Num, y: Num): Num = {
+ choose { (r : Num) =>
+ r != x && r != y
+ }
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/Church/Mult.scala b/testcases/synthesis/oopsla2013/Church/Mult.scala
new file mode 100644
index 0000000000000000000000000000000000000000..42519e663c4f59cb118a47854ed98ad2bd6b22df
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/Church/Mult.scala
@@ -0,0 +1,37 @@
+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 = (x match {
+ case Z => y
+ case S(p) => add(p, S(y))
+ }) ensuring (value(_) == value(x) + value(y))
+
+ //def distinct(x : Num, y : Num) : Num = (x match {
+ // case Z =>
+ // S(y)
+
+ // case S(p) =>
+ // y match {
+ // case Z =>
+ // S(x)
+ // case S(p) =>
+ // Z
+ // }
+ //}) ensuring (res => res != x && res != y)
+
+ def mult(x: Num, y: Num): Num = {
+ choose { (r : Num) =>
+ value(r) == value(x) * value(y)
+ }
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/Church/Squared.scala b/testcases/synthesis/oopsla2013/Church/Squared.scala
new file mode 100644
index 0000000000000000000000000000000000000000..096f212a617c433eaf474010dc1e203c86cfce7e
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/Church/Squared.scala
@@ -0,0 +1,44 @@
+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 = (x match {
+ case Z => y
+ case S(p) => add(p, S(y))
+ }) ensuring (value(_) == value(x) + value(y))
+
+ //def distinct(x : Num, y : Num) : Num = (x match {
+ // case Z =>
+ // S(y)
+
+ // case S(p) =>
+ // y match {
+ // case Z =>
+ // S(x)
+ // case S(p) =>
+ // Z
+ // }
+ //}) ensuring (res => res != x && res != y)
+
+ def mult(x: Num, y: Num): Num = (y match {
+ case S(p) =>
+ add(mult(x, p), x)
+ case Z =>
+ Z
+ }) ensuring { value(_) == value(x) * value(y) }
+
+ def squared(x: Num): Num = {
+ choose { (r : Num) =>
+ value(r) == value(x) * value(x)
+ }
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/List/Complete.scala b/testcases/synthesis/oopsla2013/List/Complete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2f6d74b81a5251131684272577e4476c02647bf1
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/List/Complete.scala
@@ -0,0 +1,74 @@
+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)
+ //}
+
+}
diff --git a/testcases/synthesis/oopsla2013/List/Delete.scala b/testcases/synthesis/oopsla2013/List/Delete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9fdef981b563018e52f43a49af6fd468e1395dc5
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/List/Delete.scala
@@ -0,0 +1,40 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Delete {
+ 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 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)
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/List/Diff.scala b/testcases/synthesis/oopsla2013/List/Diff.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3e7121eb18b807f746530aa6c1a165960343e1cf
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/List/Diff.scala
@@ -0,0 +1,58 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Diff {
+ 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 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 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 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)
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/List/Insert.scala b/testcases/synthesis/oopsla2013/List/Insert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e5b21b45d3fcf090c6af8bd3fa7dd40f45ef00f5
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/List/Insert.scala
@@ -0,0 +1,27 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Insert {
+ 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)
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/List/Union.scala b/testcases/synthesis/oopsla2013/List/Union.scala
new file mode 100644
index 0000000000000000000000000000000000000000..adcc943fdabb9052c50c84f1ec58e80d8432ef99
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/List/Union.scala
@@ -0,0 +1,49 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Union {
+ 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 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 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)
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Complete.scala b/testcases/synthesis/oopsla2013/SortedList/Complete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b83a876a3ef6e16c9c707e8dddfd94fcf83a332c
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Complete.scala
@@ -0,0 +1,171 @@
+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 insert1(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, insert1(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 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 insert2(in1: List, v: Int) = choose {
+ // (out : List) =>
+ // isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out) && size(out) == size(in1) + 1
+ //}
+
+ 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 delete(in1: List, v: Int) = choose {
+ // (out : List) =>
+ // isSorted(in1) && (content(out) == content(in1) -- Set(v)) && isSorted(out)
+ //}
+
+ def union(in1: List, in2: List): List = {
+ require(isSorted(in1) && isSorted(in2))
+ in1 match {
+ case Cons(h1, t1) =>
+ union(t1, insert1(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 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) }
+
+ //def diff(in1: List, in2: List) = choose {
+ // (out : List) =>
+ // isSorted(in1) && isSorted(in2) && (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) = (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) }
+ //}
+
+ def sort1(in : List) : List = (in match {
+ case Nil => Nil
+ case Cons(x, xs) => insert1(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/Delete.scala b/testcases/synthesis/oopsla2013/SortedList/Delete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1b99aeb00e24864515d72b8844b94043ae9cba4c
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Delete.scala
@@ -0,0 +1,80 @@
+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 insert1(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, insert1(t, v))
+ }
+ case Nil =>
+ Cons(v, Nil)
+ }
+
+ } 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 {
+ // 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 delete(in1: List, v: Int) = choose {
+ (out : List) =>
+ isSorted(in1) && (content(out) == content(in1) -- Set(v)) && isSorted(out)
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Diff.scala b/testcases/synthesis/oopsla2013/SortedList/Diff.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4dd0df64f5833882470f8301505a4e034b9f4173
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Diff.scala
@@ -0,0 +1,101 @@
+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 insert1(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, insert1(t, v))
+ }
+ case Nil =>
+ Cons(v, Nil)
+ }
+
+ } 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 {
+ 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) =>
+ union(t1, insert1(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) }
+
+ 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/SortedList/Insert1.scala b/testcases/synthesis/oopsla2013/SortedList/Insert1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1b93466404a5e4ab840a16bfaaf85c1841ee72ba
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Insert1.scala
@@ -0,0 +1,47 @@
+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 insert1(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, insert1(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)
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Insert2.scala b/testcases/synthesis/oopsla2013/SortedList/Insert2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..98c7331e9271dcc8b5dd9a30474ffdb2ea9a0050
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Insert2.scala
@@ -0,0 +1,47 @@
+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 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 insert2(in1: List, v: Int) = choose {
+ (out : List) =>
+ isSorted(in1) && (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
new file mode 100644
index 0000000000000000000000000000000000000000..03619f39ede7c65f87d535d85d0f90fd601ad4ff
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Sort.scala
@@ -0,0 +1,142 @@
+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 insert1(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, insert1(t, v))
+ }
+ case Nil =>
+ Cons(v, Nil)
+ }
+
+ } 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 {
+ 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) =>
+ insert1(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 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) = (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) => insert1(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/Split.scala b/testcases/synthesis/oopsla2013/SortedList/Split.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5d28846ea8e278912fbd0a801830def580d58234
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Split.scala
@@ -0,0 +1,128 @@
+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 insert1(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, insert1(t, v))
+ }
+ case Nil =>
+ Cons(v, Nil)
+ }
+
+ } 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 {
+ 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) =>
+ union(t1, insert1(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 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) = (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/SortedList/Split1.scala b/testcases/synthesis/oopsla2013/SortedList/Split1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..daa3b9deb6d493b320a152578832670481a44ccc
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Split1.scala
@@ -0,0 +1,128 @@
+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 insert1(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, insert1(t, v))
+ }
+ case Nil =>
+ Cons(v, Nil)
+ }
+
+ } 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 {
+ 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) =>
+ union(t1, insert1(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 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) = (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)) => (content(res._1) ++ content(res._2) == content(list)) }
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split2.scala b/testcases/synthesis/oopsla2013/SortedList/Split2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fcdcf7b68abc51190d2568ec4217b555c14f70f7
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Split2.scala
@@ -0,0 +1,128 @@
+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 insert1(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, insert1(t, v))
+ }
+ case Nil =>
+ Cons(v, Nil)
+ }
+
+ } 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 {
+ 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) =>
+ union(t1, insert1(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 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) = (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)) => (content(res._1) ++ content(res._2) == content(list)) && abs(size(res._1) - size(res._2)) <= 1 }
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Split3.scala b/testcases/synthesis/oopsla2013/SortedList/Split3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1042be56e875482207c585ac820bb4cb0c8b952a
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Split3.scala
@@ -0,0 +1,128 @@
+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 insert1(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, insert1(t, v))
+ }
+ case Nil =>
+ Cons(v, Nil)
+ }
+
+ } 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 {
+ 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) =>
+ union(t1, insert1(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 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) = (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)) => (content(res._1) ++ content(res._2) == content(list)) && abs(size(res._1) - size(res._2)) <= 1 && (size(res._1) + size(res._2) == size(list)) }
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/SortedList/Union.scala b/testcases/synthesis/oopsla2013/SortedList/Union.scala
new file mode 100644
index 0000000000000000000000000000000000000000..394ca3a7a82a4e541838f8df725abb9e10770da3
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SortedList/Union.scala
@@ -0,0 +1,91 @@
+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 insert1(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, insert1(t, v))
+ }
+ case Nil =>
+ Cons(v, Nil)
+ }
+
+ } 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 {
+ 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) =>
+ // union(t1, insert1(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)
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Complete.scala b/testcases/synthesis/oopsla2013/SparseVector/Complete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..21e2d277d5a64e50b93e66121e91454f75dec0fb
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SparseVector/Complete.scala
@@ -0,0 +1,114 @@
+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 = {
+ require(invariant(sv))
+
+ sv match {
+ case Cons(i, v, t) =>
+ if (i == at) {
+ Cons(i, newV, t)
+ } else if (i > at) {
+ Cons(at, newV, sv)
+ } else {
+ Cons(i, v, set(t, at, newV))
+ }
+ case Nil =>
+ Cons(at, newV, Nil)
+ }
+ } ensuring { res => (values(res) contains newV) && invariant(res) && (indices(res) == indices(sv) ++ Set(at)) }
+
+ //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 = {
+ require(invariant(sv))
+
+ sv match {
+ case Cons(i, v, t) =>
+ if (i == at) {
+ t
+ } else if (i > at) {
+ sv
+ } else {
+ Cons(i, v, delete(t, at))
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { res => (size(res) <= size(sv)) && 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 = {
+ require(invariant(sv))
+
+ sv match {
+ case Cons(i, v, t) =>
+ if (i == at) {
+ Some(v)
+ } else if (i > at) {
+ None
+ } else {
+ get(t, at)
+ }
+ case Nil =>
+ None
+ }
+ } ensuring { res => ((indices(sv) contains at) == isDefined(res)) && (!isDefined(res) || (values(sv) contains valueOf(res)) }
+
+ // 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/SparseVector/Delete.scala b/testcases/synthesis/oopsla2013/SparseVector/Delete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9a9acedf2cc961d8cf41269f50de85704d9b5a94
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SparseVector/Delete.scala
@@ -0,0 +1,89 @@
+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 = {
+ require(invariant(sv))
+
+ sv match {
+ case Cons(i, v, t) =>
+ if (i == at) {
+ Cons(i, newV, t)
+ } else if (i > at) {
+ Cons(at, newV, sv)
+ } else {
+ Cons(i, v, set(t, at, newV))
+ }
+ case Nil =>
+ Cons(at, newV, Nil)
+ }
+ } ensuring { res => (values(res) contains newV) && invariant(res) && (indices(res) == indices(sv) ++ Set(at)) }
+
+ // def delete(sv: SparseVector, at: Int): SparseVector = {
+ // require(invariant(sv))
+
+ // sv match {
+ // case Cons(i, v, t) =>
+ // if (i == at) {
+ // t
+ // } else if (i > at) {
+ // sv
+ // } else {
+ // Cons(i, v, delete(t, at))
+ // }
+ // case Nil =>
+ // Nil
+ // }
+ // } ensuring { res => (size(res) <= size(sv)) && 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))
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/SparseVector/Get.scala b/testcases/synthesis/oopsla2013/SparseVector/Get.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1cf7a4cd2466175550c6d001be9394d845351b68
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SparseVector/Get.scala
@@ -0,0 +1,106 @@
+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 = {
+ require(invariant(sv))
+
+ sv match {
+ case Cons(i, v, t) =>
+ if (i == at) {
+ Cons(i, newV, t)
+ } else if (i > at) {
+ Cons(at, newV, sv)
+ } else {
+ Cons(i, v, set(t, at, newV))
+ }
+ case Nil =>
+ Cons(at, newV, Nil)
+ }
+ } ensuring { res => (values(res) contains newV) && invariant(res) && (indices(res) == indices(sv) ++ Set(at)) }
+
+ def delete(sv: SparseVector, at: Int): SparseVector = {
+ require(invariant(sv))
+
+ sv match {
+ case Cons(i, v, t) =>
+ if (i == at) {
+ t
+ } else if (i > at) {
+ sv
+ } else {
+ Cons(i, v, delete(t, at))
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { res => (size(res) <= size(sv)) && invariant(res) && (indices(res) == indices(sv) -- Set(at)) }
+
+ // def get(sv: SparseVector, at: Int): Option = {
+ // require(invariant(sv))
+
+ // sv match {
+ // case Cons(i, v, t) =>
+ // if (i == at) {
+ // Some(v)
+ // } else if (i > at) {
+ // None
+ // } else {
+ // get(t, at)
+ // }
+ // case Nil =>
+ // None
+ // }
+ // } ensuring { res => ((indices(sv) contains at) == isDefined(res)) && (!isDefined(res) || (values(sv) contains valueOf(res)) }
+
+ 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/SparseVector/Set.scala b/testcases/synthesis/oopsla2013/SparseVector/Set.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f36589c39169feee5c70b42a0c42f8194fc0cac1
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/SparseVector/Set.scala
@@ -0,0 +1,72 @@
+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 = {
+ // require(invariant(sv))
+
+ // sv match {
+ // case Cons(i, v, t) =>
+ // if (i == at) {
+ // Cons(i, newV, t)
+ // } else if (i > at) {
+ // Cons(at, newV, sv)
+ // } else {
+ // Cons(i, v, set(t, at, newV))
+ // }
+ // case Nil =>
+ // Cons(at, newV, Nil)
+ // }
+ // } ensuring { res => (values(res) contains newV) && invariant(res) && (indices(res) == indices(sv) ++ Set(at)) }
+
+ 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))
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Complete.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Complete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c4a8096decc1f5c331b60b4e555afdf6ba16c706
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Complete.scala
@@ -0,0 +1,99 @@
+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 insert1(in1: List, v: Int) = choose {
+ // (out : List) =>
+ // isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+ //}
+
+ 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) {
+ t
+ } else {
+ in1
+ }
+ case Nil =>
+ Nil
+ }
+ } 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 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 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) }
+
+ //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
new file mode 100644
index 0000000000000000000000000000000000000000..a0b56fa9da45474b70a1af440932ad26fe931aa3
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Delete.scala
@@ -0,0 +1,63 @@
+import leon.Annotations._
+import leon.Utils._
+
+object Delete {
+ 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) {
+ // t
+ // } else {
+ // in1
+ // }
+ // case Nil =>
+ // Nil
+ // }
+ // } 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)
+ }
+}
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala
new file mode 100644
index 0000000000000000000000000000000000000000..eea2a1eac8c87156e7a90df8510275bc4b2dff02
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Diff.scala
@@ -0,0 +1,84 @@
+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) {
+ t
+ } 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) =>
+ union(t1, insert(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) }
+
+ 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/Insert.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..31344aec35684ccb34b5cbcce1f1f32e52f2c035
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Insert.scala
@@ -0,0 +1,47 @@
+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 insert(in1: List, v: Int) = choose {
+ (out : List) =>
+ isSorted(in1) && (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+ }
+
+}
diff --git a/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala b/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e44158330eba8111f27db44aa32d703a7ba87d4d
--- /dev/null
+++ b/testcases/synthesis/oopsla2013/StrictSortedList/Union.scala
@@ -0,0 +1,73 @@
+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) {
+ t
+ } 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) =>
+ // 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)
+ }
+}