diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala index ee86f09792923f489ded2a30c7f06debd8f7f68e..904fb2eb8a3a04269eda88000fd33d6d94924f4a 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())