diff --git a/testcases/verification/datastructures/RedBlackTree.scala b/testcases/verification/datastructures/RedBlackTree.scala
index dec88b97b7bd23bcb726d1f3ccfa13e6409c26e3..43e4d6c9a28e4bc396c127bc0d217ca127fe2fd7 100644
--- a/testcases/verification/datastructures/RedBlackTree.scala
+++ b/testcases/verification/datastructures/RedBlackTree.scala
@@ -1,58 +1,122 @@
+import leon.annotation._
import leon.lang._
-object RedBlackTree {
+object RedBlackTree {
sealed abstract class Color
case class Red() extends Color
case class Black() extends Color
-
+
sealed abstract class Tree
case class Empty() extends Tree
case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
- def content(t : Tree) : Set[Int] = t match {
+ sealed abstract class OptionInt
+ case class Some(v : Int) extends OptionInt
+ case class None() extends OptionInt
+
+ def content(t: Tree) : Set[Int] = t match {
case Empty() => Set.empty
case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
}
- def size(t : Tree) : BigInt = t match {
- case Empty() => 0
+ def size(t: Tree) : BigInt = (t match {
+ case Empty() => BigInt(0)
case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }) ensuring(_ >= 0)
+
+ /* We consider leaves to be black by definition */
+ def isBlack(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(),_,_,_) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(), l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red(), l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(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 (res => (
- (content(res) == content(t) ++ Set(x))
- && (size(t) <= size(res) && size(res) < size(t) + 2)
- ))
+ def blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Empty() => true
+ }
+
+ def blackHeight(t : Tree) : BigInt = t match {
+ case Empty() => BigInt(1)
+ case Node(Black(), l, _, _) => blackHeight(l) + 1
+ case Node(Red(), l, _, _) => blackHeight(l)
+ }
+
+ // <<insert element x into the tree t>>
+ def ins(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ 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 (res => content(res) == content(t) ++ Set(x)
+ && size(t) <= size(res) && size(res) <= size(t) + 1
+ && redDescHaveBlackChildren(res)
+ && blackBalanced(res))
+
+ def makeBlack(n: Tree): Tree = {
+ require(redDescHaveBlackChildren(n) && blackBalanced(n))
+ n match {
+ case Node(Red(),l,v,r) => Node(Black(),l,v,r)
+ case _ => n
+ }
+ } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res))
def add(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
makeBlack(ins(x, t))
- } ensuring (content(_) == content(t) ++ Set(x))
-
- def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = (Node(c,a,x,b) match {
- case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(c,a,xV,b) => Node(c,a,xV,b)
- }) ensuring (res => content(res) == content(Node(c,a,x,b)))
-
- def makeBlack(n: Tree): Tree = n match {
- case Node(Red(),l,v,r) => Node(Black(),l,v,r)
- case _ => n
- }
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res))
+
+ def buggyAdd(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t))
+ ins(x, t)
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+
+ def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ Node(c,a,x,b) match {
+ case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
+
+ def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ Node(c,a,x,b) match {
+ case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ // case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
def flip(t : Tree) : Tree = t match {
case Empty() => Empty()
case Node(color,l,e,r) => Node(color,flip(r),e,flip(l))
}
+
}
diff --git a/testcases/verification/sas2011-testcases/InsertionSort.scala b/testcases/verification/list-algorithms/InsertionSort.scala
similarity index 100%
rename from testcases/verification/sas2011-testcases/InsertionSort.scala
rename to testcases/verification/list-algorithms/InsertionSort.scala
diff --git a/testcases/verification/sas2011-testcases/SearchLinkedList.scala b/testcases/verification/list-algorithms/SearchLinkedList.scala
similarity index 100%
rename from testcases/verification/sas2011-testcases/SearchLinkedList.scala
rename to testcases/verification/list-algorithms/SearchLinkedList.scala
diff --git a/testcases/verification/sas2011-testcases/AmortizedQueue.scala b/testcases/verification/sas2011-testcases/AmortizedQueue.scala
deleted file mode 100644
index d5caf37ec30ab6ce0f7d26f56da07e0a9b9dd441..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/AmortizedQueue.scala
+++ /dev/null
@@ -1,123 +0,0 @@
-import leon.lang._
-import leon.annotation._
-
-object AmortizedQueue {
- sealed abstract class List
- case class Cons(head : Int, tail : List) extends List
- case class Nil() extends List
-
- sealed abstract class AbsQueue
- case class Queue(front : List, rear : List) extends AbsQueue
-
- def size(list : List) : BigInt = (list match {
- case Nil() => BigInt(0)
- case Cons(_, xs) => 1 + size(xs)
- }) ensuring(_ >= 0)
-
- def content(l: List) : Set[Int] = l match {
- case Nil() => Set.empty[Int]
- case Cons(x, xs) => Set(x) ++ content(xs)
- }
-
- def asList(queue : AbsQueue) : List = queue match {
- case Queue(front, rear) => concat(front, reverse(rear))
- }
-
- def concat(l1 : List, l2 : List) : List = (l1 match {
- case Nil() => l2
- case Cons(x,xs) => Cons(x, concat(xs, l2))
- }) ensuring (res => size(res) == size(l1) + size(l2) && content(res) == content(l1) ++ content(l2))
-
- def isAmortized(queue : AbsQueue) : Boolean = queue match {
- case Queue(front, rear) => size(front) >= size(rear)
- }
-
- def isEmpty(queue : AbsQueue) : Boolean = queue match {
- case Queue(Nil(), Nil()) => true
- case _ => false
- }
-
- def reverse(l : List) : List = (l match {
- case Nil() => Nil()
- case Cons(x, xs) => concat(reverse(xs), Cons(x, Nil()))
- }) ensuring (content(_) == content(l))
-
- def amortizedQueue(front : List, rear : List) : AbsQueue = {
- if (size(rear) <= size(front))
- Queue(front, rear)
- else
- Queue(concat(front, reverse(rear)), Nil())
- } ensuring(isAmortized(_))
-
- def enqueue(queue : AbsQueue, elem : Int) : AbsQueue = (queue match {
- case Queue(front, rear) => amortizedQueue(front, Cons(elem, rear))
- }) ensuring(isAmortized(_))
-
- def tail(queue : AbsQueue) : AbsQueue = {
- require(isAmortized(queue) && !isEmpty(queue))
- queue match {
- case Queue(Cons(f, fs), rear) => amortizedQueue(fs, rear)
- }
- } ensuring (isAmortized(_))
-
- def front(queue : AbsQueue) : Int = {
- require(isAmortized(queue) && !isEmpty(queue))
- queue match {
- case Queue(Cons(f, _), _) => f
- }
- }
-
- // @induct
- // def propEnqueue(rear : List, front : List, list : List, elem : Int) : Boolean = {
- // require(isAmortized(Queue(front, rear)))
- // val queue = Queue(front, rear)
- // if (asList(queue) == list) {
- // asList(enqueue(queue, elem)) == concat(list, Cons(elem, Nil()))
- // } else
- // true
- // } holds
-
- @induct
- def propFront(queue : AbsQueue, list : List, elem : Int) : Boolean = {
- require(!isEmpty(queue) && isAmortized(queue))
- if (asList(queue) == list) {
- list match {
- case Cons(x, _) => front(queue) == x
- }
- } else
- true
- } holds
-
- @induct
- def propTail(rear : List, front : List, list : List, elem : Int) : Boolean = {
- require(!isEmpty(Queue(front, rear)) && isAmortized(Queue(front, rear)))
- if (asList(Queue(front, rear)) == list) {
- list match {
- case Cons(_, xs) => asList(tail(Queue(front, rear))) == xs
- }
- } else
- true
- } // holds
-
- def enqueueAndFront(queue : AbsQueue, elem : Int) : Boolean = {
- if (isEmpty(queue))
- front(enqueue(queue, elem)) == elem
- else
- true
- } holds
-
- def enqueueDequeueThrice(queue : AbsQueue, e1 : Int, e2 : Int, e3 : Int) : Boolean = {
- if (isEmpty(queue)) {
- val q1 = enqueue(queue, e1)
- val q2 = enqueue(q1, e2)
- val q3 = enqueue(q2, e3)
- val e1prime = front(q3)
- val q4 = tail(q3)
- val e2prime = front(q4)
- val q5 = tail(q4)
- val e3prime = front(q5)
- e1 == e1prime && e2 == e2prime && e3 == e3prime
- } else
- true
- } holds
-}
diff --git a/testcases/verification/sas2011-testcases/AssociativeList.scala b/testcases/verification/sas2011-testcases/AssociativeList.scala
deleted file mode 100644
index 3b4e954a87a07a7bfb128427d20454d36d4435eb..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/AssociativeList.scala
+++ /dev/null
@@ -1,49 +0,0 @@
-import leon.lang._
-import leon.annotation._
-
-object AssociativeList {
- sealed abstract class KeyValuePairAbs
- case class KeyValuePair(key: Int, value: Int) extends KeyValuePairAbs
-
- sealed abstract class List
- case class Cons(head: KeyValuePairAbs, tail: List) extends List
- case class Nil() extends List
-
- sealed abstract class OptionInt
- case class Some(i: Int) extends OptionInt
- case class None() extends OptionInt
-
- def domain(l: List): Set[Int] = l match {
- case Nil() => Set.empty[Int]
- case Cons(KeyValuePair(k,_), xs) => Set(k) ++ domain(xs)
- }
-
- def find(l: List, e: Int): OptionInt = l match {
- case Nil() => None()
- case Cons(KeyValuePair(k, v), xs) => if (k == e) Some(v) else find(xs, e)
- }
-
- def noDuplicates(l: List): Boolean = l match {
- case Nil() => true
- case Cons(KeyValuePair(k, v), xs) => find(xs, k) == None() && noDuplicates(xs)
- }
-
- def update(l1: List, l2: List): List = (l2 match {
- case Nil() => l1
- case Cons(x, xs) => update(updateElem(l1, x), xs)
- }) ensuring(domain(_) == domain(l1) ++ domain(l2))
-
- def updateElem(l: List, e: KeyValuePairAbs): List = (l match {
- case Nil() => Cons(e, Nil())
- case Cons(KeyValuePair(k, v), xs) => e match {
- case KeyValuePair(ek, ev) => if (ek == k) Cons(KeyValuePair(ek, ev), xs) else Cons(KeyValuePair(k, v), updateElem(xs, e))
- }
- }) ensuring(res => e match {
- case KeyValuePair(k, v) => domain(res) == domain(l) ++ Set[Int](k)
- })
-
- @induct
- def readOverWrite(l: List, k1: Int, k2: Int, e: Int) : Boolean = {
- find(updateElem(l, KeyValuePair(k2,e)), k1) == (if (k1 == k2) Some(e) else find(l, k1))
- } holds
-}
diff --git a/testcases/verification/sas2011-testcases/ListOperations.scala b/testcases/verification/sas2011-testcases/ListOperations.scala
deleted file mode 100644
index 991febc577600d9e3d960745e8cd1ab64488dd89..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/ListOperations.scala
+++ /dev/null
@@ -1,106 +0,0 @@
-import leon.annotation._
-import leon.lang._
-
-object ListOperations {
- sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
- case class Nil() extends List
-
- sealed abstract class IntPairList
- case class IPCons(head: IntPair, tail: IntPairList) extends IntPairList
- case class IPNil() extends IntPairList
-
- sealed abstract class IntPair
- case class IP(fst: Int, snd: Int) extends IntPair
-
- def size(l: List) : BigInt = (l match {
- case Nil() => BigInt(0)
- case Cons(_, t) => 1 + size(t)
- }) ensuring(res => res >= 0)
-
- def iplSize(l: IntPairList) : BigInt = (l match {
- case IPNil() => BigInt(0)
- case IPCons(_, xs) => 1 + iplSize(xs)
- }) ensuring(_ >= 0)
-
- def zip(l1: List, l2: List) : IntPairList = {
- // try to comment this and see how pattern-matching becomes
- // non-exhaustive and post-condition fails
- require(size(l1) == size(l2))
-
- l1 match {
- case Nil() => IPNil()
- case Cons(x, xs) => l2 match {
- case Cons(y, ys) => IPCons(IP(x, y), zip(xs, ys))
- }
- }
- } ensuring(iplSize(_) == size(l1))
-
- def sizeTailRec(l: List) : BigInt = sizeTailRecAcc(l, 0)
- def sizeTailRecAcc(l: List, acc: BigInt) : BigInt = {
- require(acc >= 0)
- l match {
- case Nil() => acc
- case Cons(_, xs) => sizeTailRecAcc(xs, acc+1)
- }
- } ensuring(res => res == size(l) + acc)
-
- def sizesAreEquiv(l: List) : Boolean = {
- size(l) == sizeTailRec(l)
- } holds
-
- def content(l: List) : Set[Int] = l match {
- case Nil() => Set.empty[Int]
- case Cons(x, xs) => Set(x) ++ content(xs)
- }
-
- def sizeAndContent(l: List) : Boolean = {
- size(l) == 0 || content(l) != Set.empty[Int]
- } holds
-
- 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))
-
- 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))
- }) ensuring(content(_) == content(l1) ++ content(l2))
-
- def append(l1 : List, l2 : List) : List = (l1 match {
- case Nil() => l2
- case Cons(x,xs) => Cons(x, append(xs, l2))
- }) ensuring(content(_) == content(l1) ++ content(l2))
-
- @induct
- def nilAppend(l : List) : Boolean = (append(l, Nil()) == l) holds
-
- @induct
- def appendAssoc(xs : List, ys : List, zs : List) : Boolean =
- (append(append(xs, ys), zs) == append(xs, append(ys, zs))) holds
-
- def revAuxBroken(l1 : List, e : Int, l2 : List) : Boolean = {
- (append(reverse(l1), Cons(e,l2)) == reverse0(l1, l2))
- } holds
-
- @induct
- def sizeAppend(l1 : List, l2 : List) : Boolean =
- (size(append(l1, l2)) == size(l1) + size(l2)) holds
-
- @induct
- def concat(l1: List, l2: List) : List =
- concat0(l1, l2, Nil()) ensuring(content(_) == content(l1) ++ content(l2))
-
- @induct
- 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))
-}
diff --git a/testcases/verification/sas2011-testcases/PropositionalLogic.scala b/testcases/verification/sas2011-testcases/PropositionalLogic.scala
deleted file mode 100644
index efc8f8f87b468b9b7a1283e3476a901e1cb32a2a..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/PropositionalLogic.scala
+++ /dev/null
@@ -1,85 +0,0 @@
-import leon.lang._
-import leon.annotation._
-
-object PropositionalLogic {
-
- sealed abstract class Formula
- case class And(lhs: Formula, rhs: Formula) extends Formula
- case class Or(lhs: Formula, rhs: Formula) extends Formula
- case class Implies(lhs: Formula, rhs: Formula) extends Formula
- case class Not(f: Formula) extends Formula
- case class Literal(id: Int) extends Formula
-
- def simplify(f: Formula): Formula = (f match {
- case And(lhs, rhs) => And(simplify(lhs), simplify(rhs))
- case Or(lhs, rhs) => Or(simplify(lhs), simplify(rhs))
- case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs))
- case Not(f) => Not(simplify(f))
- case Literal(_) => f
- }) ensuring(isSimplified(_))
-
- def isSimplified(f: Formula): Boolean = f match {
- case And(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
- case Or(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
- case Implies(_,_) => false
- case Not(f) => isSimplified(f)
- case Literal(_) => true
- }
-
- def nnf(formula: Formula): Formula = (formula match {
- case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
- case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
- case Implies(lhs, rhs) => Implies(nnf(lhs), nnf(rhs))
- case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
- case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
- case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
- case Not(Not(f)) => nnf(f)
- case Not(Literal(_)) => formula
- case Literal(_) => formula
- }) ensuring(isNNF(_))
-
- def isNNF(f: Formula): Boolean = f match {
- case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
- case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
- case Implies(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
- case Not(Literal(_)) => true
- case Not(_) => false
- case Literal(_) => true
- }
-
- def vars(f: Formula): Set[Int] = {
- require(isNNF(f))
- f match {
- case And(lhs, rhs) => vars(lhs) ++ vars(rhs)
- case Or(lhs, rhs) => vars(lhs) ++ vars(rhs)
- case Implies(lhs, rhs) => vars(lhs) ++ vars(rhs)
- case Not(Literal(i)) => Set[Int](i)
- case Literal(i) => Set[Int](i)
- }
- }
-
- def fv(f : Formula) = { vars(nnf(f)) }
-
- // @induct
- // def wrongCommutative(f: Formula) : Boolean = {
- // nnf(simplify(f)) == simplify(nnf(f))
- // } holds
-
- @induct
- def simplifyBreaksNNF(f: Formula) : Boolean = {
- require(isNNF(f))
- isNNF(simplify(f))
- } holds
-
- @induct
- def nnfIsStable(f: Formula) : Boolean = {
- require(isNNF(f))
- nnf(f) == f
- } holds
-
- @induct
- def simplifyIsStable(f: Formula) : Boolean = {
- require(isSimplified(f))
- simplify(f) == f
- } holds
-}
diff --git a/testcases/verification/sas2011-testcases/RedBlackTree.scala b/testcases/verification/sas2011-testcases/RedBlackTree.scala
deleted file mode 100644
index 0e6603209f079d23a95560bdb576e7ef719a426c..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/RedBlackTree.scala
+++ /dev/null
@@ -1,116 +0,0 @@
-import leon.annotation._
-import leon.lang._
-
-object RedBlackTree {
- sealed abstract class Color
- case class Red() extends Color
- case class Black() extends Color
-
- sealed abstract class Tree
- case class Empty() extends Tree
- case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
-
- sealed abstract class OptionInt
- case class Some(v : Int) extends OptionInt
- case class None() extends OptionInt
-
- def content(t: Tree) : Set[Int] = t match {
- case Empty() => Set.empty
- case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
- }
-
- def size(t: Tree) : BigInt = (t match {
- case Empty() => BigInt(0)
- case Node(_, l, v, r) => size(l) + 1 + size(r)
- }) ensuring(_ >= 0)
-
- /* We consider leaves to be black by definition */
- def isBlack(t: Tree) : Boolean = t match {
- case Empty() => true
- case Node(Black(),_,_,_) => true
- case _ => false
- }
-
- def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
- case Empty() => true
- case Node(Black(), l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
- case Node(Red(), l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
- }
-
- def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
- case Empty() => true
- case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
- }
-
- def blackBalanced(t : Tree) : Boolean = t match {
- case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
- case Empty() => true
- }
-
- def blackHeight(t : Tree) : BigInt = t match {
- case Empty() => BigInt(1)
- case Node(Black(), l, _, _) => blackHeight(l) + 1
- case Node(Red(), l, _, _) => blackHeight(l)
- }
-
- // <<insert element x into the tree t>>
- def ins(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t) && blackBalanced(t))
- 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 (res => content(res) == content(t) ++ Set(x)
- && size(t) <= size(res) && size(res) <= size(t) + 1
- && redDescHaveBlackChildren(res)
- && blackBalanced(res))
-
- def makeBlack(n: Tree): Tree = {
- require(redDescHaveBlackChildren(n) && blackBalanced(n))
- n match {
- case Node(Red(),l,v,r) => Node(Black(),l,v,r)
- case _ => n
- }
- } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res))
-
- def add(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t) && blackBalanced(t))
- makeBlack(ins(x, t))
- } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res))
-
- def buggyAdd(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t))
- ins(x, t)
- } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
-
- def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
- Node(c,a,x,b) match {
- case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(c,a,xV,b) => Node(c,a,xV,b)
- }
- } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
-
- def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
- Node(c,a,x,b) match {
- case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
- Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
- // case Node(c,a,xV,b) => Node(c,a,xV,b)
- }
- } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
-}
diff --git a/testcases/verification/sas2011-testcases/SumAndMax.scala b/testcases/verification/sas2011-testcases/SumAndMax.scala
deleted file mode 100644
index c9383e64c0108f2a9c23091a7c85fe54b5f0b007..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/SumAndMax.scala
+++ /dev/null
@@ -1,46 +0,0 @@
-import leon.lang._
-import leon.annotation._
-
-object SumAndMax {
- sealed abstract class List
- case class Cons(head : BigInt, tail : List) extends List
- case class Nil() extends List
-
- def max(list : List) : BigInt = {
- require(list != Nil())
- list match {
- case Cons(x, Nil()) => x
- case Cons(x, xs) => {
- val m2 = max(xs)
- if(m2 > x) m2 else x
- }
- }
- }
-
- def sum(list : List) : BigInt = list match {
- case Nil() => BigInt(0)
- case Cons(x, xs) => x + sum(xs)
- }
-
- def size(list : List) : BigInt = (list match {
- case Nil() => BigInt(0)
- case Cons(_, xs) => 1 + size(xs)
- }) ensuring(_ >= 0)
-
- def allPos(list : List) : Boolean = list match {
- case Nil() => true
- case Cons(x, xs) => x >= 0 && allPos(xs)
- }
-
- def prop0(list : List) : Boolean = {
- require(list != Nil())
- !allPos(list) || max(list) >= 0
- } holds
-
- @induct
- def property(list : List) : Boolean = {
- // This precondition was given in the problem but isn't actually useful :D
- // require(allPos(list))
- sum(list) <= size(list) * (if(list == Nil()) 0 else max(list))
- } holds
-}
diff --git a/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/AmortizedQueue-evaluation.txt b/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/AmortizedQueue-evaluation.txt
deleted file mode 100644
index 0207bd93034318af8090a46529807a538c5b4c6e..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/AmortizedQueue-evaluation.txt
+++ /dev/null
@@ -1,13 +0,0 @@
-without postcondition:
-front 0 1 ok 0.01
-propTail 2 1 ok 0.06
-with postcondition:
-size 0 0 ok 0.14
-concat 0 0 ok 0.04
-reverse 0 0 ok 0.20
-amortizedQueue 0 0 ok 0.05
-enqueue 0 0 ok < 0.01
-tail 0 1 ok 0.15
-propFront 1 1 ok 0.07
-enqueueAndFront 1 0 ok 0.21
-enqueueDequeueThrice 5 0 ok 2.48
diff --git a/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/AssociativeList-evaluation.txt b/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/AssociativeList-evaluation.txt
deleted file mode 100644
index 03b687030cecf005ae3633bb36a8108ca63816e0..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/AssociativeList-evaluation.txt
+++ /dev/null
@@ -1,8 +0,0 @@
-without postcondition:
-domain 0 1 ok 0.05
-find 0 1 ok < 0.01
-noDuplicates 0 1 ok < 0.01
-with postcondition:
-update 0 0 ok 0.03
-updateElem 0 1 ok 0.05
-readOverWrite 0 0 ok 0.10
diff --git a/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/InsertionSort-evaluation.txt b/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/InsertionSort-evaluation.txt
deleted file mode 100644
index 9c5e144f15c1f1b8f69224bf69731a085590f5f4..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/InsertionSort-evaluation.txt
+++ /dev/null
@@ -1,7 +0,0 @@
-without postcondition:
-isSorted 0 1 ok < 0.01
-with postcondition:
-size 0 0 ok 0.06
-sortedIns 1 0 ok 0.24
-buggySortedIns 0 0 err 0.08
-sort 1 0 ok 0.03
diff --git a/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/ListOperations-evaluation.txt b/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/ListOperations-evaluation.txt
deleted file mode 100644
index 90fbbeb4f3b61f87913f093385c921ab18ae4b03..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/ListOperations-evaluation.txt
+++ /dev/null
@@ -1,19 +0,0 @@
-without postcondition:
-sizeTailRec 1 0 ok < 0.01
-with postcondition:
-size 0 0 ok 0.12
-iplSize 0 0 ok < 0.01
-zip 1 1 ok 0.09
-sizeTailRecAcc 1 0 ok 0.01
-sizesAreEquiv 0 0 ok < 0.01
-sizeAndContent 0 0 ok < 0.01
-drunk 0 0 ok 0.02
-reverse 0 0 ok 0.02
-reverse0 0 0 ok 0.04
-append 0 0 ok 0.03
-nilAppend 0 0 ok 0.03
-appendAssoc 0 0 ok 0.03
-revAuxBroken 0 0 err 0.01
-sizeAppend 0 0 ok 0.04
-concat 0 0 ok 0.04
-concat0 0 0 ok 0.29
diff --git a/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/PropositionalLogic-evaluation.txt b/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/PropositionalLogic-evaluation.txt
deleted file mode 100644
index c30b5819adff827ecc49401dec01bd4bd80ef6b1..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/PropositionalLogic-evaluation.txt
+++ /dev/null
@@ -1,10 +0,0 @@
-without postcondition:
-isNNF 0 1 ok < 0.01
-vars 6 1 ok 0.13
-fv 1 0 ok 0.02
-with postcondition:
-simplify 0 0 ok 0.84
-nnf 0 1 ok 0.37
-simplifyBreaksNNF 0 0 err 0.28
-nnfIsStable 0 0 ok 0.17
-simplifyIsStable 0 0 ok 0.12
diff --git a/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/RedBlackTree-evaluation.txt b/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/RedBlackTree-evaluation.txt
deleted file mode 100644
index 787a94bafd7efc3f3602e46f2a6d114b5d471a24..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/RedBlackTree-evaluation.txt
+++ /dev/null
@@ -1,11 +0,0 @@
-without postcondition:
-redNodesHaveBlackChildren 0 1 ok < 0.01
-blackHeight 0 1 ok < 0.01
-with postcondition:
-size 0 0 ok 0.11
-ins 2 0 ok 2.88
-makeBlack 0 0 ok 0.02
-add 2 0 ok 0.19
-buggyAdd 1 0 err 0.26
-balance 0 1 ok 0.13
-buggyBalance 0 1 err 0.12
diff --git a/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/SearchLinkedList-evaluation.txt b/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/SearchLinkedList-evaluation.txt
deleted file mode 100644
index 4e0f49a724119dd787acf72d066b22a61255b0f9..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/SearchLinkedList-evaluation.txt
+++ /dev/null
@@ -1,4 +0,0 @@
-with postcondition:
-size 0 0 ok 0.11
-firstZero 0 0 ok 0.03
-goal 0 0 ok 0.01
diff --git a/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/SumAndMax-evaluation.txt b/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/SumAndMax-evaluation.txt
deleted file mode 100644
index e4895a210cca096556e8c3101fb0995904d5543f..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/camera-ready-eval-summaries/SumAndMax-evaluation.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-without postcondition:
-max 2 1 ok 0.13
-with postcondition:
-size 0 0 ok < 0.01
-prop0 1 0 ok 0.02
-property 2 0 ok 0.11
diff --git a/testcases/verification/sas2011-testcases/eval-summary/AmortizedQueue-evaluation.txt b/testcases/verification/sas2011-testcases/eval-summary/AmortizedQueue-evaluation.txt
deleted file mode 100644
index 5830ca49e5f98912bdc21ab8d84b2ec2472e8a2d..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/eval-summary/AmortizedQueue-evaluation.txt
+++ /dev/null
@@ -1,14 +0,0 @@
-size 0 1 ok 0.12
-content 0 1 ok < 0.01
-asList 0 1 ok < 0.01
-concat 0 1 ok 0.05
-isAmortized 0 1 ok < 0.01
-isEmpty 0 1 ok < 0.01
-reverse 0 1 ok 0.34
-amortizedQueue 0 0 ok < 0.01
-enqueue 0 1 ok 0.01
-front 0 1 ok 0.02
-tail 0 1 ok 0.04
-propFront 1 1 ok 0.13
-enqueueAndFront 1 0 ok 0.13
-enqueueDequeueThrice 5 0 ok 2.27
diff --git a/testcases/verification/sas2011-testcases/eval-summary/AssociativeList-evaluation.txt b/testcases/verification/sas2011-testcases/eval-summary/AssociativeList-evaluation.txt
deleted file mode 100644
index da29597252b6fc613f0d203ef67f564c85a0c33d..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/eval-summary/AssociativeList-evaluation.txt
+++ /dev/null
@@ -1,8 +0,0 @@
-with postcondition:
-update 0 0 ok 0.06
-updateElem 0 1 ok 0.03
-readOverWrite 0 0 ok 0.13
-without postcondition:
-domain 0 1 ok 0.12
-find 0 1 ok < 0.01
-noDuplicates 0 1 ok < 0.01
diff --git a/testcases/verification/sas2011-testcases/eval-summary/InsertionSort-evaluation.txt b/testcases/verification/sas2011-testcases/eval-summary/InsertionSort-evaluation.txt
deleted file mode 100644
index 9001a41a27d8be3f60c9ac1924e9c7e979f90b7d..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/eval-summary/InsertionSort-evaluation.txt
+++ /dev/null
@@ -1,7 +0,0 @@
-with postcondition:
-size 0 0 ok 0.08
-sortedIns 1 0 ok 0.12
-buggySortedIns 1 0 ok 0.08
-sort 1 0 ok 0.08
-without postcondition:
-isSorted 0 1 ok < 0.01
diff --git a/testcases/verification/sas2011-testcases/eval-summary/ListOperations-evaluation.txt b/testcases/verification/sas2011-testcases/eval-summary/ListOperations-evaluation.txt
deleted file mode 100644
index 38ce53439cbac7b225bc8fd98f90350810cdaff6..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/eval-summary/ListOperations-evaluation.txt
+++ /dev/null
@@ -1,19 +0,0 @@
-with postcondition:
-size 0 0 ok 0.13
-iplSize 0 0 ok < 0.01
-zip 1 1 ok 0.10
-sizeTailRecAcc 1 0 ok 0.02
-sizesAreEquiv 0 0 ok < 0.01
-sizeAndContent 0 0 ok < 0.01
-drunk 0 0 ok 0.04
-reverse 0 0 ok < 0.01
-reverse0 0 0 ok 0.05
-append 0 0 ok 0.04
-nilAppend 0 0 ok 0.05
-appendAssoc 0 0 ok 0.12
-revAuxBroken 0 0 err 0.06
-sizeAppend 0 0 ok 0.07
-concat 0 0 ok 0.05
-concat0 0 0 ok 0.15
-without postcondition:
-sizeTailRec 1 0 ok < 0.01
diff --git a/testcases/verification/sas2011-testcases/eval-summary/PropositionalLogic-evaluation-PLDI-100.txt b/testcases/verification/sas2011-testcases/eval-summary/PropositionalLogic-evaluation-PLDI-100.txt
deleted file mode 100644
index bc8081bd176ab93316aa2d9e1547b28107d1d061..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/eval-summary/PropositionalLogic-evaluation-PLDI-100.txt
+++ /dev/null
@@ -1,2 +0,0 @@
-with postcondition:
-wrongCommutative 0 0 err 0.44
diff --git a/testcases/verification/sas2011-testcases/eval-summary/PropositionalLogic-evaluation.txt b/testcases/verification/sas2011-testcases/eval-summary/PropositionalLogic-evaluation.txt
deleted file mode 100644
index d182caa39f3c670cd34cbdb82fde05ee0ce59c12..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/eval-summary/PropositionalLogic-evaluation.txt
+++ /dev/null
@@ -1,10 +0,0 @@
-with postcondition:
-simplify 0 0 ok 0.26
-nnf 0 1 ok 0.41
-simplifyBreaksNNF 0 0 err 0.53
-nnfIsStable 0 0 ok 0.25
-simplifyIsStable 0 0 ok 0.11
-without postcondition:
-isNNF 0 1 ok < 0.01
-vars 6 1 ok 0.20
-fv 1 0 ok 0.04
diff --git a/testcases/verification/sas2011-testcases/eval-summary/RedBlackTree-evaluation.txt b/testcases/verification/sas2011-testcases/eval-summary/RedBlackTree-evaluation.txt
deleted file mode 100644
index 2009c372fff1254d1c6ac4586b2db1de54aedfd4..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/eval-summary/RedBlackTree-evaluation.txt
+++ /dev/null
@@ -1,10 +0,0 @@
-with postcondition:
-ins 2 0 ok 1.64
-makeBlack 0 0 ok 0.02
-add 2 0 ok 0.08
-buggyAdd 1 0 err 0.24
-balance 0 1 ok 0.11
-buggyBalance 0 1 err 0.03
-without postcondition:
-redNodesHaveBlackChildren 0 1 ok 0.04
-blackHeight 0 1 ok < 0.01
diff --git a/testcases/verification/sas2011-testcases/eval-summary/SearchLinkedList-evaluation.txt b/testcases/verification/sas2011-testcases/eval-summary/SearchLinkedList-evaluation.txt
deleted file mode 100644
index 3df0215328e39b05772e45e00bb44216f77f1afc..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/eval-summary/SearchLinkedList-evaluation.txt
+++ /dev/null
@@ -1,5 +0,0 @@
-size 0 1 ok 0.07
-contains 0 1 ok < 0.01
-firstZero 0 1 ok 0.03
-firstZeroAtPos 0 1 ok < 0.01
-goal 0 0 ok < 0.01
diff --git a/testcases/verification/sas2011-testcases/eval-summary/SumAndMax-evaluation-pldi-100.txt b/testcases/verification/sas2011-testcases/eval-summary/SumAndMax-evaluation-pldi-100.txt
deleted file mode 100644
index 43ab8c385c8ac82c945949bad3ee78a1fea3a1d9..0000000000000000000000000000000000000000
--- a/testcases/verification/sas2011-testcases/eval-summary/SumAndMax-evaluation-pldi-100.txt
+++ /dev/null
@@ -1,6 +0,0 @@
-max 2 1 ok 0.08
-sum 0 1 ok < 0.01
-allPos 0 1 ok < 0.01
-size 0 1 ok 0.01
-prop0 1 0 ok < 0.01
-property 1 0 ok 0.22