From c8c767a7d10ab90dcc4a61a3358225673c72ef14 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Fri, 18 May 2012 01:33:19 +0000
Subject: [PATCH] List testcase
---
testcases/testgen/List.scala | 14 ++++++++++++++
1 file changed, 14 insertions(+)
create mode 100644 testcases/testgen/List.scala
diff --git a/testcases/testgen/List.scala b/testcases/testgen/List.scala
new file mode 100644
index 000000000..8d436d370
--- /dev/null
+++ b/testcases/testgen/List.scala
@@ -0,0 +1,14 @@
+import leon.Utils._
+
+object List {
+
+ abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def size(l: List): Int = waypoint(1, (l match {
+ case Cons(_, tail) => 1 + size(tail)
+ case Nil() => 0
+ })) ensuring(_ >= 0)
+
+}
--
GitLab