From b42e1da7671a534e0a159406ce8351ba49b7bdf5 Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <viktor.kuncak@epfl.ch>
Date: Sat, 12 Jan 2013 21:23:32 +0100
Subject: [PATCH] i/o examples for generating lists and concat
---
.../synthesis/cav2013/ListByExample.scala | 61 +++++++++++++++++++
1 file changed, 61 insertions(+)
create mode 100644 testcases/synthesis/cav2013/ListByExample.scala
diff --git a/testcases/synthesis/cav2013/ListByExample.scala b/testcases/synthesis/cav2013/ListByExample.scala
new file mode 100644
index 000000000..b1f076774
--- /dev/null
+++ b/testcases/synthesis/cav2013/ListByExample.scala
@@ -0,0 +1,61 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object Lists {
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def size(l:List): Int = (l match {
+ case Nil() => 0
+ case Cons(h,t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def listUp(a:Int,b:Int) : List = {
+ require(a <= b)
+ if (a == b) Cons(a,Nil())
+ else Cons(a, listUp(a+1,b))
+ } ensuring (res => size(res)==1+b-a)
+
+ def listUp_syn(a:Int,b:Int) : List = {
+ require(a <= b)
+ choose((res:List) =>
+ size(res)==1+b-a &&
+ (!(a==5 && b==9) || res==Cons(5,Cons(6,Cons(7,Cons(8,Cons(9,Nil())))))) &&
+ (!(a==100 && b==105) ||
+ res==Cons(100,Cons(101,Cons(102,Cons(103,Cons(104,Cons(105,Nil())))))))
+ )
+ }
+
+ def listDown(a:Int,b:Int) : List = {
+ require(a >= b)
+ if (a == b) Cons(a,Nil())
+ else Cons(a, listUp(a-1,b))
+ } ensuring (res => size(res)==1+b-a)
+
+ def listDown_syn(a:Int,b:Int) : List = {
+ require(a >= b)
+ choose((res:List) =>
+ size(res)==1+b-a &&
+ (!(a==9 && b==5) || res==Cons(9,Cons(8,Cons(7,Cons(6,Cons(5,Nil())))))) &&
+ (!(a==105 && b==100) ||
+ res==Cons(105,Cons(104,Cons(103,Cons(102,Cons(101,Cons(100,Nil())))))))
+ )
+ }
+
+ def concat_syn(a:List, b:List) : List = {
+ choose((res:List) =>
+ size(res) == size(a) + size(b) &&
+ (!(a==listUp(1,5) && b==listUp(6,9)) ||
+ res==listUp(1,9)) &&
+ (!(a==listUp(101,105) && b==listUp(106,109)) ||
+ res==listUp(101,109)) &&
+ (!(a==listUp(201,205) && b==listUp(206,209)) ||
+ res==listUp(201,209)) &&
+ (!(a==listUp(301,304) && b==listUp(304,310)) ||
+ res==listUp(301,310))
+ )
+ }
+
+}
--
GitLab