From b95e12e913184a6bd79c254e5faa9ca938541e6c Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <vkuncak@gmail.com>
Date: Mon, 25 Oct 2010 17:15:11 +0000
Subject: [PATCH] redblack with size
---
testcases/ListWithSize.scala | 5 +++++
testcases/RedBlackTree.scala | 9 ++++++++-
2 files changed, 13 insertions(+), 1 deletion(-)
diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala
index fc1eac3a1..ee86f0979 100644
--- a/testcases/ListWithSize.scala
+++ b/testcases/ListWithSize.scala
@@ -44,6 +44,11 @@ object ListWithSize {
append(l, Nil()) == l
} ensuring(_ == true)
+ @induct
+ def allListsAreEmpty(l : List) : Boolean = {
+ allListsAreEmpty(l) && (l == Nil())
+ } ensuring (_ == true)
+
def propAppend2(l : List) : Boolean = (l match {
case Nil() => propAppend1(l)
case Cons(x,xs) => (!propAppend1(xs) || propAppend1(l))
diff --git a/testcases/RedBlackTree.scala b/testcases/RedBlackTree.scala
index 0edbb64f9..9cb55c574 100644
--- a/testcases/RedBlackTree.scala
+++ b/testcases/RedBlackTree.scala
@@ -15,13 +15,20 @@ object RedBlackTree {
case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
}
+ def size(t : Tree) : Int = t match {
+ case Empty() => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
def ins(x : Int, t: Tree): Tree = (t match {
case Empty() => Node(Red(),Empty(),x,Empty())
case Node(c,a,y,b) =>
if (x < y) balance(c, ins(x, a), y, b)
else if (x == y) Node(c,a,y,b)
else balance(c,a,y,ins(x, b))
- }) ensuring (content(_) == content(t) ++ Set(x))
+ }) ensuring (res =>
+ content(res) == content(t) ++ Set(x) &&
+ size(t) <= size(res) && size(res) < size(t) + 2)
def add(x: Int, t: Tree): Tree = {
makeBlack(ins(x, t))
--
GitLab