From e8fa850aa0ba1f2b2a5078e22d396e8122dacf24 Mon Sep 17 00:00:00 2001
From: Swen Jacobs <swen.jacobs@epfl.ch>
Date: Thu, 8 Jul 2010 16:47:47 +0000
Subject: [PATCH] modified testcases
---
testcases/InsertionSort.scala | 2 +-
testcases/RedBlack.scala | 71 +++++++++++++++++++++++------------
2 files changed, 47 insertions(+), 26 deletions(-)
diff --git a/testcases/InsertionSort.scala b/testcases/InsertionSort.scala
index 68be171bb..02031140b 100644
--- a/testcases/InsertionSort.scala
+++ b/testcases/InsertionSort.scala
@@ -26,7 +26,7 @@ object InsertionSort {
def sorted(l: List): List = (l match {
case Nil() => Nil()
case Cons(x,xs) => sortedIns(x, sorted(xs))
- }) ensuring(res => contents(res) == contents(l) && isSorted(res))
+ }) ensuring(res => contents(res) == contents(l))// && isSorted(res))
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
diff --git a/testcases/RedBlack.scala b/testcases/RedBlack.scala
index d2f1a1f8e..97b0b6247 100644
--- a/testcases/RedBlack.scala
+++ b/testcases/RedBlack.scala
@@ -1,3 +1,6 @@
+//SJ: I tried to modify this so that funcheck doesn't give Z3 translation
+// warnings, but didn't manage quite yet
+
import scala.collection.immutable.Set
object RedBlack {
@@ -13,10 +16,26 @@ object RedBlack {
// Invariant 1. No red node has a red parent
def invariant1(t: Tree): Boolean = t match {
case EmptyTree() => true
- case Node(Black(), left, _, right) => invariant1(left) && invariant1(right)
- case Node(Red(), Node(Red(), _, _, _), _, _) => false
- case Node(Red(), _, _, Node(Red(), _, _, _)) => false
- case Node(Red(), left, _, right) => invariant1(left) && invariant1(right)
+ case Node(color, left, _, right) => color match {
+ case Black() => invariant1(left) && invariant1(right)
+ case Red() => left match {
+ case Node(col2, _, _, _) => col2 match {
+ case Red() => false
+ case _ => right match {
+ case Node(col3, _, _, _) => col3 match {
+ case Red() => false
+ case _ => invariant1(left) && invariant1(right)
+ }
+ }
+ }
+ case _ => right match {
+ case Node(col3, _, _, _) => col3 match {
+ case Red() => false
+ case _ => invariant1(left) && invariant1(right)
+ }
+ }
+ }
+ }
}
/// Invariant 1 END
@@ -26,24 +45,27 @@ object RedBlack {
def countBlackNodes(t: Tree): Int = t match {
case EmptyTree() => 1
- case Node(Red(), left, _, _) => countBlackNodes(left)
- case Node(Black(), left, _, _) => countBlackNodes(left) + 1
+ case Node(color, left, _, _) => color match {
+ case Red() => countBlackNodes(left)
+ case Black() => countBlackNodes(left) + 1
+ }
}
def invariant2(t: Tree, n: Int): Boolean = t match {
- case EmptyTree() if n == 1 => true
- case EmptyTree() => false
- case Node(Red(), left, _, right) => invariant2(left, n) && invariant2(right, n)
- case Node(Black(), left, _, right) => invariant2(left, n-1) && invariant2(right, n-1)
+ case EmptyTree() => if (n == 1) true else false
+ case Node(color, left, _, right) => color match {
+ case Red() => invariant2(left, n) && invariant2(right, n)
+ case Black() => invariant2(left, n-1) && invariant2(right, n-1)
+ }
}
/// Invariant 2 END
def member(t: Tree, e: Int): Boolean = t match {
case EmptyTree() => false
- case Node(_, _, x, _) if x == e => true
- case Node(_, left, x, _) if e < x => member( left, e)
- case Node(_, _, _, right) => member(right, e)
+ case Node(_, left, x, right) => if (x == e) true
+ else if (e < x) member( left, e)
+ else member(right, e)
}
def contents(t: Tree): Set[Int] = t match {
@@ -51,33 +73,32 @@ object RedBlack {
case Node(_, left, x, right) => contents(left) ++ contents(right) ++ Set(x)
}
- def makeBlack(t: Tree) = {
- require(t != EmptyTree())
+ def makeBlack(t: Node) = {
+ //require(t != EmptyTree())
//val Node(_, left, x, right) = t
//Node(Black(), left, x, right)
t match {
- case Node(_, left, x, right) => Node(Black(), left, x, right)
+ case Node(color, left, x, right) => Node(Black(), left, x, right)
}
} ensuring ((x:Tree) => x match {case Node(Black(), _, _, _) => true; case _ => false})
- def ins_(t: Tree, e: Int): Tree = t match {
+ def ins_(t: Tree, e: Int): Node = t match {
case EmptyTree() => Node(Red(), EmptyTree(), e, EmptyTree())
- case Node(color, left, x, right) if x < e => balance(Node(color, ins_(left, e), x, right))
- case Node(color, left, x, right) if x > e => balance(Node(color, left, x, ins_(right, e)))
- // Element already exists
- case t => t
+ case n@Node(color, left, x, right) => if (x<e) balance(Node(color, ins_(left, e), x, right))
+ else if (x > e) balance(Node(color, left, x, ins_(right, e)))
+ else n //Element already exists
}
- def balance(t: Tree) : Tree = {
- require(t != EmptyTree())
+ def balance(t: Node) : Node = {
+ //require(t != EmptyTree())
t match {
case Node(Black(), Node(Red(), Node(Red(), a, x, b), y, c), z, d) => Node(Red(), Node(Black(), a, x, b), y, Node(Black(), c, z, d))
case Node(Black(), Node(Red(), a, x, Node(Red(), b, y, c)), z, d) => Node(Red(), Node(Black(), a, x, b), y, Node(Black(), c, z, d))
case Node(Black(), a, x, Node(Red(), Node(Red(), b, y, c), z, d)) => Node(Red(), Node(Black(), a, x, b), y, Node(Black(), c, z, d))
case Node(Black(), a, x, Node(Red(), b, y, Node(Red(), c, z, d))) => Node(Red(), Node(Black(), a, x, b), y, Node(Black(), c, z, d))
- case t => t
+ case n@Node(_,_,_,_) => n
}
- } ensuring (_ => true)
+ } //ensuring (_ => true)
def insert(t: Tree, e: Int): Tree = makeBlack( ins_(t, e) ) ensuring {res => invariant1(res) && invariant2(res, countBlackNodes(res))}
--
GitLab