From 75ecc2e53722d15cc16c70a1ef0d15b4d29df63a Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 23 Nov 2015 15:53:06 +0100
Subject: [PATCH] Add good synthesis testcases
---
.../synthesis/etienne-thesis/List/Diff.scala | 13 +---
.../etienne-thesis/List/Insert.scala | 4 +-
.../synthesis/etienne-thesis/List/Split.scala | 70 ++-----------------
.../synthesis/etienne-thesis/List/Union.scala | 17 +----
4 files changed, 10 insertions(+), 94 deletions(-)
diff --git a/testcases/synthesis/etienne-thesis/List/Diff.scala b/testcases/synthesis/etienne-thesis/List/Diff.scala
index 9b452ed7f..9fb3ade95 100644
--- a/testcases/synthesis/etienne-thesis/List/Diff.scala
+++ b/testcases/synthesis/etienne-thesis/List/Diff.scala
@@ -8,8 +8,8 @@ object Diff {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
@@ -34,15 +34,6 @@ 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 =>
diff --git a/testcases/synthesis/etienne-thesis/List/Insert.scala b/testcases/synthesis/etienne-thesis/List/Insert.scala
index 6da044ca3..48c38f4df 100644
--- a/testcases/synthesis/etienne-thesis/List/Insert.scala
+++ b/testcases/synthesis/etienne-thesis/List/Insert.scala
@@ -8,8 +8,8 @@ object Insert {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/synthesis/etienne-thesis/List/Split.scala b/testcases/synthesis/etienne-thesis/List/Split.scala
index 1f709a866..47793c081 100644
--- a/testcases/synthesis/etienne-thesis/List/Split.scala
+++ b/testcases/synthesis/etienne-thesis/List/Split.scala
@@ -10,8 +10,8 @@ object Complete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
@@ -19,63 +19,7 @@ object Complete {
case Cons(i, t) => Set(i) ++ content(t)
}
- def insert(in1: List, v: BigInt): List = {
- Cons(v, in1)
- } ensuring { content(_) == content(in1) ++ Set(v) }
-
- //def insert(in1: List, v: BigInt) = choose {
- // (out : List) =>
- // content(out) == content(in1) ++ Set(v)
- //}
-
- def delete(in1: List, v: BigInt): 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: BigInt) = 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) &&
@@ -86,16 +30,10 @@ object Complete {
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) }
}
+ // case (h1, (h2, t)) => (h1 :: split(t)._1, h2 :: split(t)._2)
+
}
diff --git a/testcases/synthesis/etienne-thesis/List/Union.scala b/testcases/synthesis/etienne-thesis/List/Union.scala
index b17064866..d6a5fa579 100644
--- a/testcases/synthesis/etienne-thesis/List/Union.scala
+++ b/testcases/synthesis/etienne-thesis/List/Union.scala
@@ -8,8 +8,8 @@ object Union {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1)+ size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
@@ -21,19 +21,6 @@ object Union {
Cons(v, in1)
} ensuring { content(_) == content(in1) ++ Set(v) }
- def delete(in1: List, v: BigInt): 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) =>
--
GitLab