From 13959168b2914ce0d4c4d05e334a4bf051562e7f Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Wed, 15 Apr 2015 15:04:01 +0200
Subject: [PATCH] Every Synthesis benchmark in leon-web is now a regression
test
---
.../regression/synthesis/Church/Add.scala | 14 +--
.../synthesis/Church/Distinct.scala | 23 +---
.../regression/synthesis/Church/Mult.scala | 24 +----
.../regression/synthesis/Church/Squared.scala | 27 +----
.../regression/synthesis/List/Delete.scala | 34 ++----
.../regression/synthesis/List/Diff.scala | 41 ++-----
.../regression/synthesis/List/Insert.scala | 23 ++--
.../regression/synthesis/List/Split.scala | 101 ------------------
.../regression/synthesis/List/Split1.scala | 30 ++++++
.../regression/synthesis/List/Split2.scala | 31 ++++++
.../regression/synthesis/List/Split3.scala | 36 +++++++
.../regression/synthesis/List/Union.scala | 43 ++------
.../synthesis/SortedList/Delete.scala | 33 ++++++
.../synthesis/SortedList/Diff.scala | 50 +++++++++
.../synthesis/SortedList/Insert1.scala | 34 ++++++
.../synthesis/SortedList/Insert2.scala | 34 ++++++
.../synthesis/SortedList/InsertSort.scala | 51 +++++++++
.../synthesis/SortedList/Union.scala | 50 +++++++++
.../synthesis/StrictSortedList/Delete.scala | 33 ++++++
.../synthesis/StrictSortedList/Insert.scala | 34 ++++++
.../synthesis/StrictSortedList/Union.scala | 50 +++++++++
21 files changed, 518 insertions(+), 278 deletions(-)
delete mode 100644 src/test/resources/regression/synthesis/List/Split.scala
create mode 100644 src/test/resources/regression/synthesis/List/Split1.scala
create mode 100644 src/test/resources/regression/synthesis/List/Split2.scala
create mode 100644 src/test/resources/regression/synthesis/List/Split3.scala
create mode 100644 src/test/resources/regression/synthesis/SortedList/Delete.scala
create mode 100644 src/test/resources/regression/synthesis/SortedList/Diff.scala
create mode 100644 src/test/resources/regression/synthesis/SortedList/Insert1.scala
create mode 100644 src/test/resources/regression/synthesis/SortedList/Insert2.scala
create mode 100644 src/test/resources/regression/synthesis/SortedList/InsertSort.scala
create mode 100644 src/test/resources/regression/synthesis/SortedList/Union.scala
create mode 100644 src/test/resources/regression/synthesis/StrictSortedList/Delete.scala
create mode 100644 src/test/resources/regression/synthesis/StrictSortedList/Insert.scala
create mode 100644 src/test/resources/regression/synthesis/StrictSortedList/Union.scala
diff --git a/src/test/resources/regression/synthesis/Church/Add.scala b/src/test/resources/regression/synthesis/Church/Add.scala
index d060360c2..694f76a15 100644
--- a/src/test/resources/regression/synthesis/Church/Add.scala
+++ b/src/test/resources/regression/synthesis/Church/Add.scala
@@ -1,27 +1,21 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
import leon.lang._
import leon.lang.synthesis._
+import leon.annotation._
-object ChurchNumerals {
+object Numerals {
sealed abstract class Num
case object Z extends Num
case class S(pred: Num) extends Num
- def value(n:Num) : Int = {
+ def value(n: Num): BigInt = {
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) =>
+ choose { (r: Num) =>
value(r) == value(x) + value(y)
}
}
diff --git a/src/test/resources/regression/synthesis/Church/Distinct.scala b/src/test/resources/regression/synthesis/Church/Distinct.scala
index 3e503f4ab..827d8d70f 100644
--- a/src/test/resources/regression/synthesis/Church/Distinct.scala
+++ b/src/test/resources/regression/synthesis/Church/Distinct.scala
@@ -1,37 +1,24 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
import leon.lang._
import leon.lang.synthesis._
-object ChurchNumerals {
+import leon.annotation._
+
+object Numerals {
sealed abstract class Num
case object Z extends Num
case class S(pred: Num) extends Num
- def value(n:Num) : Int = {
+ def value(n: Num): BigInt = {
n match {
case Z => 0
case S(p) => 1 + value(p)
}
} ensuring (_ >= 0)
- def add(x : Num, y : Num) : Num = (x match {
+ 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/src/test/resources/regression/synthesis/Church/Mult.scala b/src/test/resources/regression/synthesis/Church/Mult.scala
index 39c0286d0..1e58606d0 100644
--- a/src/test/resources/regression/synthesis/Church/Mult.scala
+++ b/src/test/resources/regression/synthesis/Church/Mult.scala
@@ -1,40 +1,26 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
import leon.lang._
import leon.lang.synthesis._
+import leon.annotation._
-object ChurchNumerals {
+object Numerals {
sealed abstract class Num
case object Z extends Num
case class S(pred: Num) extends Num
- def value(n:Num) : Int = {
+ def value(n: Num): BigInt = {
n match {
case Z => 0
case S(p) => 1 + value(p)
}
} ensuring (_ >= 0)
- def add(x : Num, y : Num) : Num = (x match {
+ 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) =>
+ choose { (r: Num) =>
value(r) == value(x) * value(y)
}
}
diff --git a/src/test/resources/regression/synthesis/Church/Squared.scala b/src/test/resources/regression/synthesis/Church/Squared.scala
index 9328e70ff..32b05900f 100644
--- a/src/test/resources/regression/synthesis/Church/Squared.scala
+++ b/src/test/resources/regression/synthesis/Church/Squared.scala
@@ -1,38 +1,19 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
import leon.lang._
import leon.lang.synthesis._
+import leon.annotation._
-object ChurchNumerals {
+object Numerals {
sealed abstract class Num
case object Z extends Num
case class S(pred: Num) extends Num
- def value(n:Num) : Int = {
+ def value(n:Num) : BigInt = {
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)
@@ -41,7 +22,7 @@ object ChurchNumerals {
}) ensuring { value(_) == value(x) * value(y) }
def squared(x: Num): Num = {
- choose { (r : Num) =>
+ choose { (r: Num) =>
value(r) == value(x) * value(x)
}
}
diff --git a/src/test/resources/regression/synthesis/List/Delete.scala b/src/test/resources/regression/synthesis/List/Delete.scala
index 02f13ec38..a548f46e2 100644
--- a/src/test/resources/regression/synthesis/List/Delete.scala
+++ b/src/test/resources/regression/synthesis/List/Delete.scala
@@ -1,43 +1,25 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-import leon.annotation._
import leon.lang._
import leon.lang.synthesis._
+import leon.annotation._
object Delete {
sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
+ case class Cons(head: BigInt, tail: List) extends List
case object Nil extends List
- def size(l: List) : Int = (l match {
+ def size(l: List) : BigInt = (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]
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
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) =>
+ def delete(in1: List, v: BigInt) = {
+ choose { (out : List) =>
content(out) == content(in1) -- Set(v)
+ }
}
}
diff --git a/src/test/resources/regression/synthesis/List/Diff.scala b/src/test/resources/regression/synthesis/List/Diff.scala
index 5ae469ea7..0943955b1 100644
--- a/src/test/resources/regression/synthesis/List/Diff.scala
+++ b/src/test/resources/regression/synthesis/List/Diff.scala
@@ -1,29 +1,23 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-import leon.annotation._
import leon.lang._
import leon.lang.synthesis._
+import leon.annotation._
object Diff {
sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
+ case class Cons(head: BigInt, tail: List) extends List
case object Nil extends List
- def size(l: List) : Int = (l match {
+ def size(l: List) : BigInt = (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]
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
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 = {
+ def delete(in1: List, v: BigInt): List = {
in1 match {
case Cons(h,t) =>
if (h == v) {
@@ -36,26 +30,9 @@ object Diff {
}
} 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) =>
+ def diff(in1: List, in2: List) = {
+ choose { (out : List) =>
content(out) == content(in1) -- content(in2)
+ }
}
}
diff --git a/src/test/resources/regression/synthesis/List/Insert.scala b/src/test/resources/regression/synthesis/List/Insert.scala
index 0a2cb88b0..62e91d9b9 100644
--- a/src/test/resources/regression/synthesis/List/Insert.scala
+++ b/src/test/resources/regression/synthesis/List/Insert.scala
@@ -1,30 +1,25 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-import leon.annotation._
import leon.lang._
import leon.lang.synthesis._
+import leon.annotation._
object Insert {
sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
+ case class Cons(head: BigInt, tail: List) extends List
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => BigInt(0)
- case Cons(_, t) => size(t) + 1
+ 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]
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
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) =>
+ def insert(in1: List, v: BigInt) = {
+ choose { (out : List) =>
content(out) == content(in1) ++ Set(v)
+ }
}
}
diff --git a/src/test/resources/regression/synthesis/List/Split.scala b/src/test/resources/regression/synthesis/List/Split.scala
deleted file mode 100644
index 989d509da..000000000
--- a/src/test/resources/regression/synthesis/List/Split.scala
+++ /dev/null
@@ -1,101 +0,0 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-import leon.annotation._
-import leon.lang._
-import leon.lang.synthesis._
-
-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/src/test/resources/regression/synthesis/List/Split1.scala b/src/test/resources/regression/synthesis/List/Split1.scala
new file mode 100644
index 000000000..facbda843
--- /dev/null
+++ b/src/test/resources/regression/synthesis/List/Split1.scala
@@ -0,0 +1,30 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object List {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def abs(i: BigInt) : BigInt = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ def split(list: List): (List, List) = {
+ choose { (res: (List, List)) =>
+ (content(res._1) ++ content(res._2) == content(list))
+ }
+ }
+
+}
diff --git a/src/test/resources/regression/synthesis/List/Split2.scala b/src/test/resources/regression/synthesis/List/Split2.scala
new file mode 100644
index 000000000..38c07caf5
--- /dev/null
+++ b/src/test/resources/regression/synthesis/List/Split2.scala
@@ -0,0 +1,31 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object List {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def abs(i: BigInt) : BigInt = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ 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/src/test/resources/regression/synthesis/List/Split3.scala b/src/test/resources/regression/synthesis/List/Split3.scala
new file mode 100644
index 000000000..15c74190e
--- /dev/null
+++ b/src/test/resources/regression/synthesis/List/Split3.scala
@@ -0,0 +1,36 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object List {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def abs(i: BigInt): BigInt = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ def tcons(h1: BigInt, h2: BigInt, tl: (List, List)) = {
+ (Cons(h1, tl._1), Cons(h2, tl._2))
+ }
+
+ 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/src/test/resources/regression/synthesis/List/Union.scala b/src/test/resources/regression/synthesis/List/Union.scala
index a4acf629b..0b21dc037 100644
--- a/src/test/resources/regression/synthesis/List/Union.scala
+++ b/src/test/resources/regression/synthesis/List/Union.scala
@@ -1,52 +1,25 @@
-/* Copyright 2009-2014 EPFL, Lausanne */
-
-import leon.annotation._
import leon.lang._
import leon.lang.synthesis._
+import leon.annotation._
object Union {
sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
+ case class Cons(head: BigInt, tail: List) extends List
case object Nil extends List
- def size(l: List) : Int = (l match {
+ def size(l: List) : BigInt = (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]
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
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) =>
+ def union(in1: List, in2: List) = {
+ choose { (out : List) =>
content(out) == content(in1) ++ content(in2)
+ }
}
}
diff --git a/src/test/resources/regression/synthesis/SortedList/Delete.scala b/src/test/resources/regression/synthesis/SortedList/Delete.scala
new file mode 100644
index 000000000..31305ca09
--- /dev/null
+++ b/src/test/resources/regression/synthesis/SortedList/Delete.scala
@@ -0,0 +1,33 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ 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: BigInt) = {
+ require(isSorted(in1))
+ choose { (out: List) =>
+ (content(out) == content(in1) -- Set(v)) && isSorted(out)
+ }
+ }
+}
diff --git a/src/test/resources/regression/synthesis/SortedList/Diff.scala b/src/test/resources/regression/synthesis/SortedList/Diff.scala
new file mode 100644
index 000000000..9e4e32bae
--- /dev/null
+++ b/src/test/resources/regression/synthesis/SortedList/Diff.scala
@@ -0,0 +1,50 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ 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: BigInt): 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 diff(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+ choose { (out: List) =>
+ (content(out) == content(in1) -- content(in2)) && isSorted(out)
+ }
+ }
+
+}
diff --git a/src/test/resources/regression/synthesis/SortedList/Insert1.scala b/src/test/resources/regression/synthesis/SortedList/Insert1.scala
new file mode 100644
index 000000000..affc5b455
--- /dev/null
+++ b/src/test/resources/regression/synthesis/SortedList/Insert1.scala
@@ -0,0 +1,34 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ 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: BigInt) = {
+ require(isSorted(in1))
+ choose { (out: List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+ }
+ }
+
+}
diff --git a/src/test/resources/regression/synthesis/SortedList/Insert2.scala b/src/test/resources/regression/synthesis/SortedList/Insert2.scala
new file mode 100644
index 000000000..e44eac286
--- /dev/null
+++ b/src/test/resources/regression/synthesis/SortedList/Insert2.scala
@@ -0,0 +1,34 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ 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: BigInt) = {
+ require(isSorted(in1))
+ choose { (out: List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out) && size(out) == size(in1) + 1
+ }
+ }
+
+}
diff --git a/src/test/resources/regression/synthesis/SortedList/InsertSort.scala b/src/test/resources/regression/synthesis/SortedList/InsertSort.scala
new file mode 100644
index 000000000..8f5b78247
--- /dev/null
+++ b/src/test/resources/regression/synthesis/SortedList/InsertSort.scala
@@ -0,0 +1,51 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ 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: BigInt): 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 sort(list: List): List = {
+ choose { (res: List) =>
+ isSorted(res) &&
+ content(list) == content(res)
+ }
+ }
+
+}
diff --git a/src/test/resources/regression/synthesis/SortedList/Union.scala b/src/test/resources/regression/synthesis/SortedList/Union.scala
new file mode 100644
index 000000000..95d17bb61
--- /dev/null
+++ b/src/test/resources/regression/synthesis/SortedList/Union.scala
@@ -0,0 +1,50 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ 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: BigInt): 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 union(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+ choose { (out: List) =>
+ (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ }
+ }
+}
diff --git a/src/test/resources/regression/synthesis/StrictSortedList/Delete.scala b/src/test/resources/regression/synthesis/StrictSortedList/Delete.scala
new file mode 100644
index 000000000..81827ed03
--- /dev/null
+++ b/src/test/resources/regression/synthesis/StrictSortedList/Delete.scala
@@ -0,0 +1,33 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Delete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ 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: BigInt) = {
+ require(isSorted(in1))
+ choose { (out : List) =>
+ (content(out) == content(in1) -- Set(v)) && isSorted(out)
+ }
+ }
+}
diff --git a/src/test/resources/regression/synthesis/StrictSortedList/Insert.scala b/src/test/resources/regression/synthesis/StrictSortedList/Insert.scala
new file mode 100644
index 000000000..6c7543ad3
--- /dev/null
+++ b/src/test/resources/regression/synthesis/StrictSortedList/Insert.scala
@@ -0,0 +1,34 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ 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: BigInt) = {
+ require(isSorted(in1))
+ choose { (out : List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+ }
+ }
+
+}
diff --git a/src/test/resources/regression/synthesis/StrictSortedList/Union.scala b/src/test/resources/regression/synthesis/StrictSortedList/Union.scala
new file mode 100644
index 000000000..cf2fcd727
--- /dev/null
+++ b/src/test/resources/regression/synthesis/StrictSortedList/Union.scala
@@ -0,0 +1,50 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ 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: BigInt): 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 union(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+ choose { (out : List) =>
+ (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ }
+ }
+}
--
GitLab