From f7399f63292f0e3a5db16c747f895ed2fa9d60fc Mon Sep 17 00:00:00 2001 From: Philippe Suter <philippe.suter@gmail.com> Date: Mon, 16 Aug 2010 08:39:42 +0000 Subject: [PATCH] more examples in here --- testcases/ListWithSize.scala | 33 +++++++++++++++++++++++++++++++++ 1 file changed, 33 insertions(+) diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala index be9a7e234..31f315e6a 100644 --- a/testcases/ListWithSize.scala +++ b/testcases/ListWithSize.scala @@ -1,15 +1,48 @@ +import scala.collection.immutable.Set + object ListWithSize { sealed abstract class List case class Cons(head: Int, tail: List) extends List case class Nil() extends List + // proved with unrolling=0 def size(l: List) : Int = (l match { case Nil() => 0 case Cons(_, t) => 1 + size(t) }) ensuring(_ >= 0) + def content(l: List) : Set[Int] = l match { + case Nil() => Set.empty[Int] + case Cons(x, xs) => Set(x) ++ content(xs) + } + + // proved with unrolling=1 def append(x: Int, l: List) : List = (l match { case Nil() => Cons(x, Nil()) case c @ Cons(_,_) => Cons(x, c) }) ensuring(size(_) > 0) + + // proved with unrolling=2 + def reverse(l: List) : List = reverse0(l, Nil()) ensuring(content(_) == content(l)) + def reverse0(l1: List, l2: List) : List = l1 match { + case Nil() => l2 + case Cons(x, xs) => reverse0(xs, Cons(x, l2)) + } + + // proved with unrolling=4 + def concat(l1: List, l2: List) : List = concat0(l1, l2, Nil()) ensuring(content(_) == content(l1) ++ content(l2)) + def concat0(l1: List, l2: List, l3: List) : List = (l1 match { + case Nil() => l2 match { + case Nil() => reverse(l3) + case Cons(y, ys) => { + concat0(Nil(), ys, Cons(y, l3)) + } + } + case Cons(x, xs) => concat0(xs, l2, Cons(x, l3)) + }) //ensuring(content(_) == content(l1) ++ content(l2) ++ content(l3)) + + // proved with unrolling=2 ??? + def property1(l1: List, l2: List) : Boolean = { + reverse(concat(l1, l2)) == concat(reverse(l2), reverse(l1)) + } ensuring(_ == true) } -- GitLab