From cc6344e805237f66b98820107c0b8560d07fdfef Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <vkuncak@gmail.com>
Date: Mon, 25 Oct 2010 17:20:32 +0000
Subject: [PATCH] drunk function in lists example set
---
testcases/ListWithSize.scala | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala
index ee86f0979..904fb2eb8 100644
--- a/testcases/ListWithSize.scala
+++ b/testcases/ListWithSize.scala
@@ -21,6 +21,11 @@ object ListWithSize {
size(l) == 0 || content(l) != Set.empty[Int]
} ensuring(_ == true)
+ def drunk(l : List) : List = (l match {
+ case Nil() => Nil()
+ case Cons(x,l1) => Cons(x,Cons(x,drunk(l1)))
+ }) ensuring (size(_) == 2 * size(l))
+
// proved with unrolling=1
def funnyCons(x: Int, l: List) : List = (l match {
case Nil() => Cons(x, Nil())
--
GitLab