From 6703c75eb9e1ba8e50d1b84d98eed35019d8aef6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Mika=C3=ABl=20Mayer?= <a-mikmay@microsoft.com>
Date: Thu, 10 Dec 2015 14:39:35 +0100
Subject: [PATCH] Better test cases for string synthesis
---
testcases/stringrender/DoubleListRender.scala | 35 +++++++++++++++++++
...r_Render.scala => 23_String_Grammar.scala} | 0
.../web/synthesis/24_String_DoubleList.scala | 29 +++++++++++++++
3 files changed, 64 insertions(+)
create mode 100644 testcases/stringrender/DoubleListRender.scala
rename testcases/web/synthesis/{23_String_Grammar_Render.scala => 23_String_Grammar.scala} (100%)
create mode 100644 testcases/web/synthesis/24_String_DoubleList.scala
diff --git a/testcases/stringrender/DoubleListRender.scala b/testcases/stringrender/DoubleListRender.scala
new file mode 100644
index 000000000..ed28a264b
--- /dev/null
+++ b/testcases/stringrender/DoubleListRender.scala
@@ -0,0 +1,35 @@
+/**
+ * Name: DoubleListRender.scala
+ * Creation: 09.12.2015
+ * Author: Mikael Mayer (mikael.mayer@epfl.ch)
+ * Comments: Double lists rendering specification (requires many disambiguation rounds)
+ */
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object DoubleListRender {
+ abstract class A
+ case class B(i: AA, a: A) extends A
+ case class N() extends A
+
+ abstract class AA
+ case class BB(i: A, a: AA) extends AA
+ case class NN() extends AA
+
+ // Obviously wrong, but it is useful to use the display function.
+ def twoOutOfThreeAsAreTheSame(a: A, b: A, c: A): Boolean = {
+ a == b || a == c || b == c
+ } holds
+
+ def AtoString(a : A): String = {
+ ???
+ } ensuring {
+ (res : String) => (a, res) passes {
+ case B(BB(N(), BB(B(NN(), B(NN(), N())), NN())), N()) =>
+ "[([], [(), ()])]"
+ }
+ }
+}
\ No newline at end of file
diff --git a/testcases/web/synthesis/23_String_Grammar_Render.scala b/testcases/web/synthesis/23_String_Grammar.scala
similarity index 100%
rename from testcases/web/synthesis/23_String_Grammar_Render.scala
rename to testcases/web/synthesis/23_String_Grammar.scala
diff --git a/testcases/web/synthesis/24_String_DoubleList.scala b/testcases/web/synthesis/24_String_DoubleList.scala
new file mode 100644
index 000000000..eb66400e2
--- /dev/null
+++ b/testcases/web/synthesis/24_String_DoubleList.scala
@@ -0,0 +1,29 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon.collection.ListOps._
+import leon.lang.synthesis._
+
+object DoubleListRender {
+ abstract class A
+ case class B(i: AA, a: A) extends A
+ case class N() extends A
+
+ abstract class AA
+ case class BB(i: A, a: AA) extends AA
+ case class NN() extends AA
+
+ // Obviously wrong, but it is useful to use the display function.
+ def twoOutOfThreeAsAreTheSame(a: A, b: A, c: A): Boolean = {
+ a == b || a == c || b == c
+ } holds
+
+ def AtoString(a : A): String = {
+ ???
+ } ensuring {
+ (res : String) => (a, res) passes {
+ case B(BB(N(), BB(B(NN(), B(NN(), N())), NN())), N()) =>
+ "[([], [(), ()])]"
+ }
+ }
+}
\ No newline at end of file
--
GitLab