From c12d6081e59061690c093e91341a1474e4404eae Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Mon, 25 Jun 2012 20:50:26 +0200
Subject: [PATCH] update List
---
testcases/testgen/List.scala | 12 +++++++++---
1 file changed, 9 insertions(+), 3 deletions(-)
diff --git a/testcases/testgen/List.scala b/testcases/testgen/List.scala
index 8d436d370..b21928d92 100644
--- a/testcases/testgen/List.scala
+++ b/testcases/testgen/List.scala
@@ -1,4 +1,5 @@
import leon.Utils._
+import leon.Annotations._
object List {
@@ -6,9 +7,14 @@ object 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)
+ @main
+ def size(l: List): Int = (l match {
+ case Cons(_, tail) => sizeTail(tail, 1)
case Nil() => 0
- })) ensuring(_ >= 0)
+ }) ensuring(_ >= 0)
+ def sizeTail(l2: List, acc: Int): Int = l2 match {
+ case Cons(_, tail) => sizeTail(tail, acc+1)
+ case Nil() => acc
+ }
}
--
GitLab