From de5b5fb623eef8b909ce1894db79ceb318f2be06 Mon Sep 17 00:00:00 2001
From: "Emmanouil (Manos) Koukoutos" <emmanouil.koukoutos@epfl.ch>
Date: Thu, 22 Jan 2015 20:02:25 +0100
Subject: [PATCH] Add/Fix benchmarks
---
testcases/repair/Desugar/Desugar2.scala | 2 +-
testcases/repair/HeapSort/HeapSort5.scala | 4 +-
testcases/repair/HeapSort/HeapSort8.scala | 4 +-
testcases/repair/List/FirstIndexOf.scala | 31 --
testcases/repair/List/FirstIndexOf1.scala | 31 --
testcases/repair/List/FirstIndexOf2.scala | 31 --
testcases/repair/List/FirstIndexOf3.scala | 31 --
testcases/repair/List/FirstIndexOf4.scala | 31 --
testcases/repair/List/List.scala | 420 +++++++++++++++++
testcases/repair/List/List1.scala | 420 +++++++++++++++++
testcases/repair/List/List2.scala | 426 +++++++++++++++++
testcases/repair/List/List3.scala | 428 ++++++++++++++++++
testcases/repair/List/List4.scala | 420 +++++++++++++++++
testcases/repair/List/List5.scala | 417 +++++++++++++++++
testcases/repair/List/List6.scala | 423 +++++++++++++++++
testcases/repair/List/Size.scala | 19 -
testcases/repair/List/Size1.scala | 17 -
testcases/repair/List/Sum.scala | 19 -
testcases/repair/List/Sum1.scala | 19 -
.../RedBlackTree-old/RedBlackTree.scala | 101 +++++
.../RedBlackTree-old/RedBlackTree1.scala | 143 ++++++
.../RedBlackTree-old/RedBlackTree2.scala | 143 ++++++
.../RedBlackTree-old/RedBlackTree3.scala | 143 ++++++
.../RedBlackTree4.scala | 0
.../RedBlackTree5.scala | 0
.../RedBlackTree-old/RedBlackTree6.scala | 142 ++++++
.../RedBlackTree7.scala | 0
.../repair/RedBlackTree/RedBlackTree.scala | 154 +++++--
.../repair/RedBlackTree/RedBlackTree1.scala | 202 +++++----
.../repair/RedBlackTree/RedBlackTree2.scala | 188 ++++----
.../repair/RedBlackTree/RedBlackTree3.scala | 202 +++++----
.../repair/RedBlackTree/RedBlackTree6.scala | 191 ++++----
32 files changed, 4151 insertions(+), 651 deletions(-)
delete mode 100644 testcases/repair/List/FirstIndexOf.scala
delete mode 100644 testcases/repair/List/FirstIndexOf1.scala
delete mode 100644 testcases/repair/List/FirstIndexOf2.scala
delete mode 100644 testcases/repair/List/FirstIndexOf3.scala
delete mode 100644 testcases/repair/List/FirstIndexOf4.scala
create mode 100644 testcases/repair/List/List.scala
create mode 100644 testcases/repair/List/List1.scala
create mode 100644 testcases/repair/List/List2.scala
create mode 100644 testcases/repair/List/List3.scala
create mode 100644 testcases/repair/List/List4.scala
create mode 100644 testcases/repair/List/List5.scala
create mode 100644 testcases/repair/List/List6.scala
delete mode 100644 testcases/repair/List/Size.scala
delete mode 100644 testcases/repair/List/Size1.scala
delete mode 100644 testcases/repair/List/Sum.scala
delete mode 100644 testcases/repair/List/Sum1.scala
create mode 100644 testcases/repair/RedBlackTree-old/RedBlackTree.scala
create mode 100644 testcases/repair/RedBlackTree-old/RedBlackTree1.scala
create mode 100644 testcases/repair/RedBlackTree-old/RedBlackTree2.scala
create mode 100644 testcases/repair/RedBlackTree-old/RedBlackTree3.scala
rename testcases/repair/{RedBlackTree => RedBlackTree-old}/RedBlackTree4.scala (100%)
rename testcases/repair/{RedBlackTree => RedBlackTree-old}/RedBlackTree5.scala (100%)
create mode 100644 testcases/repair/RedBlackTree-old/RedBlackTree6.scala
rename testcases/repair/{RedBlackTree => RedBlackTree-old}/RedBlackTree7.scala (100%)
diff --git a/testcases/repair/Desugar/Desugar2.scala b/testcases/repair/Desugar/Desugar2.scala
index d070fc4a2..a068dadcb 100644
--- a/testcases/repair/Desugar/Desugar2.scala
+++ b/testcases/repair/Desugar/Desugar2.scala
@@ -146,7 +146,7 @@ object Desugar {
@induct
def desugar(e : Trees.Expr) : SimpleE = { e match {
case Trees.Plus (lhs, rhs) => Plus(desugar(lhs), desugar(rhs))
- case Trees.Minus(lhs, rhs) => Plus(desugar(lhs), desugar(rhs)) // FIXME forgot Neg
+ case Trees.Minus(lhs, rhs) => Literal(0)//Plus(desugar(lhs), desugar(rhs)) // FIXME forgot Neg
case Trees.LessThan(lhs, rhs) => LessThan(desugar(lhs), desugar(rhs))
case Trees.And (lhs, rhs) => Ite(desugar(lhs), desugar(rhs), Literal(0))
case Trees.Or (lhs, rhs) => Ite(desugar(lhs), Literal(1), desugar(rhs))
diff --git a/testcases/repair/HeapSort/HeapSort5.scala b/testcases/repair/HeapSort/HeapSort5.scala
index 83a75b7ae..33a3ff5aa 100644
--- a/testcases/repair/HeapSort/HeapSort5.scala
+++ b/testcases/repair/HeapSort/HeapSort5.scala
@@ -60,7 +60,7 @@ object HeapSort {
case (Leaf(), _) => h2
case (_, Leaf()) => h1
case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
- if(v1 >= v2)
+ if(v1 <= v2) // FIXME should be >=
makeN(v1, l1, merge(r1, h2))
else
makeN(v2, l2, merge(h1, r2))
@@ -85,7 +85,7 @@ object HeapSort {
def insert(element: Int, heap: Heap) : Heap = {
require(hasLeftistProperty(heap) && hasHeapProperty(heap))
- merge(Node(element + 1, Leaf(), Leaf()), heap) // FIXME lol.
+ merge(Node(element, Leaf(), Leaf()), heap)
} ensuring { res =>
hasLeftistProperty(res) && hasHeapProperty(res) &&
diff --git a/testcases/repair/HeapSort/HeapSort8.scala b/testcases/repair/HeapSort/HeapSort8.scala
index 33a3ff5aa..83a75b7ae 100644
--- a/testcases/repair/HeapSort/HeapSort8.scala
+++ b/testcases/repair/HeapSort/HeapSort8.scala
@@ -60,7 +60,7 @@ object HeapSort {
case (Leaf(), _) => h2
case (_, Leaf()) => h1
case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
- if(v1 <= v2) // FIXME should be >=
+ if(v1 >= v2)
makeN(v1, l1, merge(r1, h2))
else
makeN(v2, l2, merge(h1, r2))
@@ -85,7 +85,7 @@ object HeapSort {
def insert(element: Int, heap: Heap) : Heap = {
require(hasLeftistProperty(heap) && hasHeapProperty(heap))
- merge(Node(element, Leaf(), Leaf()), heap)
+ merge(Node(element + 1, Leaf(), Leaf()), heap) // FIXME lol.
} ensuring { res =>
hasLeftistProperty(res) && hasHeapProperty(res) &&
diff --git a/testcases/repair/List/FirstIndexOf.scala b/testcases/repair/List/FirstIndexOf.scala
deleted file mode 100644
index d59131506..000000000
--- a/testcases/repair/List/FirstIndexOf.scala
+++ /dev/null
@@ -1,31 +0,0 @@
-import leon.lang._
-import leon.collection._
-import leon.lang.synthesis._
-
-
-object FirstIndexOf {
- def firstIndexOf(l: List[Int], v: Int): Int = {
- l match {
- case Cons(h, t) if v == h => 0
- case Cons(h, t) =>
- if (firstIndexOf(t, v) >= 0) {
- firstIndexOf(t, v)+1
- } else {
- -1
- }
- case Nil() =>
- -1
- }
- } ensuring {
- (res: Int) => (if (l.content contains v) {
- l.size > res && l.apply(res) == v
- } else {
- res == -1
- }) && (((l,v), res) passes {
- case (Cons(0, Cons(1, Cons(2, Cons(3, Nil())))), 3) => 3
- case (Cons(0, Cons(2, Cons(3, Cons(1, Nil())))), 1) => 3
- case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 1) => 1
- case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 2) => -1
- })
- }
-}
diff --git a/testcases/repair/List/FirstIndexOf1.scala b/testcases/repair/List/FirstIndexOf1.scala
deleted file mode 100644
index 382e09a2f..000000000
--- a/testcases/repair/List/FirstIndexOf1.scala
+++ /dev/null
@@ -1,31 +0,0 @@
-import leon.lang._
-import leon.collection._
-import leon.lang.synthesis._
-
-
-object FirstIndexOf {
- def firstIndexOf(l: List[Int], v: Int): Int = {
- l match {
- case Cons(h, t) if v == h => 0
- case Cons(h, t) =>
- if (firstIndexOf(t, v) >= 0) {
- firstIndexOf(t, v) // Should be +1 (Solves with CEGIS)
- } else {
- -1
- }
- case Nil() =>
- -1
- }
- } ensuring {
- (res: Int) => (if (l.content contains v) {
- l.size > res && l.apply(res) == v
- } else {
- res == -1
- }) && (((l,v), res) passes {
- case (Cons(0, Cons(1, Cons(2, Cons(3, Nil())))), 3) => 3
- case (Cons(0, Cons(2, Cons(3, Cons(1, Nil())))), 1) => 3
- case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 1) => 1
- case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 2) => -1
- })
- }
-}
diff --git a/testcases/repair/List/FirstIndexOf2.scala b/testcases/repair/List/FirstIndexOf2.scala
deleted file mode 100644
index bf78b606f..000000000
--- a/testcases/repair/List/FirstIndexOf2.scala
+++ /dev/null
@@ -1,31 +0,0 @@
-import leon.lang._
-import leon.collection._
-import leon.lang.synthesis._
-
-
-object FirstIndexOf {
- def firstIndexOf(l: List[Int], v: Int): Int = {
- l match {
- case Cons(h, t) if v == h => 0
- case Cons(h, t) =>
- if (firstIndexOf(t, v) >= 0) {
- firstIndexOf(t, v)+2 // Should be +1
- } else {
- -1
- }
- case Nil() =>
- -1
- }
- } ensuring {
- (res: Int) => (if (l.content contains v) {
- l.size > res && l.apply(res) == v
- } else {
- res == -1
- }) && (((l,v), res) passes {
- case (Cons(0, Cons(1, Cons(2, Cons(3, Nil())))), 3) => 3
- case (Cons(0, Cons(2, Cons(3, Cons(1, Nil())))), 1) => 3
- case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 1) => 1
- case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 2) => -1
- })
- }
-}
diff --git a/testcases/repair/List/FirstIndexOf3.scala b/testcases/repair/List/FirstIndexOf3.scala
deleted file mode 100644
index 9904ef804..000000000
--- a/testcases/repair/List/FirstIndexOf3.scala
+++ /dev/null
@@ -1,31 +0,0 @@
-import leon.lang._
-import leon.collection._
-import leon.lang.synthesis._
-
-
-object FirstIndexOf {
- def firstIndexOf(l: List[Int], v: Int): Int = {
- l match {
- case Cons(h, t) if v == h => 0
- case Cons(h, t) =>
- if (firstIndexOf(t, v) > 0) { // FIXME: Should be >=
- firstIndexOf(t, v)+1
- } else {
- -1
- }
- case Nil() =>
- -1
- }
- } ensuring { (res: Int) =>
- (if (l.content contains v) {
- l.size > res && l.apply(res) == v
- } else {
- res == -1
- }) && (((l,v), res) passes {
- case (Cons(0, Cons(1, Cons(2, Cons(3, Nil())))), 3) => 3
- case (Cons(0, Cons(2, Cons(3, Cons(1, Nil())))), 1) => 3
- case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 1) => 1
- case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 2) => -1
- })
- }
-}
diff --git a/testcases/repair/List/FirstIndexOf4.scala b/testcases/repair/List/FirstIndexOf4.scala
deleted file mode 100644
index df3c90f78..000000000
--- a/testcases/repair/List/FirstIndexOf4.scala
+++ /dev/null
@@ -1,31 +0,0 @@
-import leon.lang._
-import leon.collection._
-import leon.lang.synthesis._
-
-
-object FirstIndexOf {
- def firstIndexOf(l: List[Int], v: Int): Int = {
- l match {
- case Cons(h, t) if v == h => 0
- case Cons(h, t) =>
- if (firstIndexOf(t,v) <= 0) { // FIXME: should be >= 0
- firstIndexOf(t, v)+1
- } else {
- -1
- }
- case Nil() =>
- -1
- }
- } ensuring { (res: Int) =>
- (if (l.content contains v) {
- l.size > res && l.apply(res) == v
- } else {
- res == -1
- }) && (((l,v), res) passes {
- case (Cons(0, Cons(1, Cons(2, Cons(3, Nil())))), 3) => 3
- case (Cons(0, Cons(2, Cons(3, Cons(1, Nil())))), 1) => 3
- case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 1) => 1
- case (Cons(0, Cons(1, Cons(3, Cons(1, Nil())))), 2) => -1
- })
- }
-}
diff --git a/testcases/repair/List/List.scala b/testcases/repair/List/List.scala
new file mode 100644
index 000000000..19cf5ed3f
--- /dev/null
+++ b/testcases/repair/List/List.scala
@@ -0,0 +1,420 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.custom
+
+import leon._
+import leon.lang._
+import leon.annotation._
+
+sealed abstract class List0[T] {
+ def size: Int = (this match {
+ case Nil0() => 0
+ case Cons0(h, t) => 1 + t.size
+ }) ensuring (_ >= 0)
+
+ def content: Set[T] = this match {
+ case Nil0() => Set()
+ case Cons0(h, t) => Set(h) ++ t.content
+ }
+
+ def contains(v: T): Boolean = (this match {
+ case Cons0(h, t) if h == v => true
+ case Cons0(_, t) => t.contains(v)
+ case Nil0() => false
+ }) ensuring { res => res == (content contains v) }
+
+ def ++(that: List0[T]): List0[T] = (this match {
+ case Nil0() => that
+ case Cons0(x, xs) => Cons0(x, xs ++ that)
+ }) ensuring { res => (res.content == this.content ++ that.content) && (res.size == this.size + that.size)}
+
+ def head: T = {
+ require(this != Nil0[T]())
+ this match {
+ case Cons0(h, t) => h
+ }
+ }
+
+ def tail: List0[T] = {
+ require(this != Nil0[T]())
+ this match {
+ case Cons0(h, t) => t
+ }
+ }
+
+ def apply(index: Int): T = {
+ require(0 <= index && index < size)
+ if (index == 0) {
+ head
+ } else {
+ tail(index-1)
+ }
+ }
+
+ def ::(t:T): List0[T] = Cons0(t, this)
+
+ def :+(t:T): List0[T] = {
+ this match {
+ case Nil0() => Cons0(t, this)
+ case Cons0(x, xs) => Cons0(x, xs :+ (t))
+ }
+ } ensuring(res => (res.size == size + 1) && (res.content == content ++ Set(t)))
+
+ def reverse: List0[T] = {
+ this match {
+ case Nil0() => this
+ case Cons0(x,xs) => xs.reverse :+ x
+ }
+ } ensuring (res => (res.size == size) && (res.content == content))
+
+ def take(i: Int): List0[T] = (this, i) match {
+ case (Nil0(), _) => Nil0()
+ case (Cons0(h, t), i) =>
+ if (i == 0) {
+ Nil0()
+ } else {
+ Cons0(h, t.take(i-1))
+ }
+ }
+
+ def drop(i: Int): List0[T] = (this, i) match {
+ case (Nil0(), _) => Nil0()
+ case (Cons0(h, t), i) =>
+ if (i == 0) {
+ Cons0(h, t)
+ } else {
+ t.drop(i-1)
+ }
+ }
+
+ def slice(from: Int, to: Int): List0[T] = {
+ require(from < to && to < size && from >= 0)
+ drop(from).take(to-from)
+ }
+
+ def replace(from: T, to: T): List0[T] = this match {
+ case Nil0() => Nil0()
+ case Cons0(h, t) =>
+ val r = t.replace(from, to)
+ if (h == from) {
+ Cons0(to, r)
+ } else {
+ Cons0(h, r)
+ }
+ }
+
+ private def chunk0(s: Int, l: List0[T], acc: List0[T], res: List0[List0[T]], s0: Int): List0[List0[T]] = l match {
+ case Nil0() =>
+ if (acc.size > 0) {
+ res :+ acc
+ } else {
+ res
+ }
+ case Cons0(h, t) =>
+ if (s0 == 0) {
+ chunk0(s, l, Nil0(), res :+ acc, s)
+ } else {
+ chunk0(s, t, acc :+ h, res, s0-1)
+ }
+ }
+
+ def chunks(s: Int): List0[List0[T]] = {
+ require(s > 0)
+
+ chunk0(s, this, Nil0(), Nil0(), s)
+ }
+
+ def zip[B](that: List0[B]): List0[(T, B)] = (this, that) match {
+ case (Cons0(h1, t1), Cons0(h2, t2)) =>
+ Cons0((h1, h2), t1.zip(t2))
+ case (_) =>
+ Nil0()
+ }
+
+ def -(e: T): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (e == h) {
+ t - e
+ } else {
+ Cons0(h, t - e)
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def --(that: List0[T]): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (that.contains(h)) {
+ t -- that
+ } else {
+ Cons0(h, t -- that)
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def &(that: List0[T]): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (that.contains(h)) {
+ Cons0(h, t & that)
+ } else {
+ t & that
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def pad(s: Int, e: T): List0[T] = { (this, s) match {
+ case (_, s) if s <= 0 =>
+ this
+ case (Nil0(), s) =>
+ Cons0(e, Nil0().pad(s-1, e))
+ case (Cons0(h, t), s) =>
+ Cons0(h, t.pad(s, e))
+ }} ensuring { res =>
+ ((this,s,e), res) passes {
+ case (Cons0(a,Nil0()), 2, x) => Cons0(a, Cons0(x, Cons0(x, Nil0())))
+ }
+ }
+
+ def find(e: T): Option[Int] = this match {
+ case Nil0() => None()
+ case Cons0(h, t) =>
+ if (h == e) {
+ Some(0)
+ } else {
+ t.find(e) match {
+ case None() => None()
+ case Some(i) => Some(i+1)
+ }
+ }
+ }
+
+ def init: List0[T] = (this match {
+ case Cons0(h, Nil0()) =>
+ Nil0[T]()
+ case Cons0(h, t) =>
+ Cons0[T](h, t.init)
+ case Nil0() =>
+ Nil0[T]()
+ }) ensuring ( (r: List0[T]) => ((r.size < this.size) || (this.size == 0)) )
+
+ def lastOption: Option[T] = this match {
+ case Cons0(h, t) =>
+ t.lastOption.orElse(Some(h))
+ case Nil0() =>
+ None()
+ }
+
+ def firstOption: Option[T] = this match {
+ case Cons0(h, t) =>
+ Some(h)
+ case Nil0() =>
+ None()
+ }
+
+ def unique: List0[T] = this match {
+ case Nil0() => Nil0()
+ case Cons0(h, t) =>
+ Cons0(h, t.unique - h)
+ }
+
+ def splitAt(e: T): List0[List0[T]] = split(Cons0(e, Nil0()))
+
+ def split(seps: List0[T]): List0[List0[T]] = this match {
+ case Cons0(h, t) =>
+ if (seps.contains(h)) {
+ Cons0(Nil0(), t.split(seps))
+ } else {
+ val r = t.split(seps)
+ Cons0(Cons0(h, r.head), r.tail)
+ }
+ case Nil0() =>
+ Cons0(Nil0(), Nil0())
+ }
+
+ def count(e: T): Int = this match {
+ case Cons0(h, t) =>
+ if (h == e) {
+ 1 + t.count(e)
+ } else {
+ t.count(e)
+ }
+ case Nil0() =>
+ 0
+ }
+
+ def evenSplit: (List0[T], List0[T]) = {
+ val c = size/2
+ (take(c), drop(c))
+ }
+
+ def insertAt(pos: Int, l: List0[T]): List0[T] = {
+ if(pos < 0) {
+ insertAt(size + pos, l)
+ } else if(pos == 0) {
+ l ++ this
+ } else {
+ this match {
+ case Cons0(h, t) =>
+ Cons0(h, t.insertAt(pos-1, l))
+ case Nil0() =>
+ l
+ }
+ }
+ }
+
+ def replaceAt(pos: Int, l: List0[T]): List0[T] = {
+ if(pos < 0) {
+ replaceAt(size + pos, l)
+ } else if(pos == 0) {
+ l ++ this.drop(l.size)
+ } else {
+ this match {
+ case Cons0(h, t) =>
+ Cons0(h, t.replaceAt(pos-1, l))
+ case Nil0() =>
+ l
+ }
+ }
+ }
+
+ def rotate(s: Int): List0[T] = {
+ if (s < 0) {
+ rotate(size+s)
+ } else {
+ val s2 = s % size
+ drop(s2) ++ take(s2)
+ }
+ }
+
+ def isEmpty = this match {
+ case Nil0() => true
+ case _ => false
+ }
+
+}
+
+@ignore
+object List0 {
+ def apply[T](elems: T*): List0[T] = ???
+}
+
+@library
+object List0Ops {
+ def flatten[T](ls: List0[List0[T]]): List0[T] = ls match {
+ case Cons0(h, t) => h ++ flatten(t)
+ case Nil0() => Nil0()
+ }
+
+ def isSorted(ls: List0[Int]): Boolean = ls match {
+ case Nil0() => true
+ case Cons0(_, Nil0()) => true
+ case Cons0(h1, Cons0(h2, _)) if(h1 > h2) => false
+ case Cons0(_, t) => isSorted(t)
+ }
+
+ def sorted(ls: List0[Int]): List0[Int] = ls match {
+ case Cons0(h, t) => insSort(sorted(t), h)
+ case Nil0() => Nil0()
+ }
+
+ def insSort(ls: List0[Int], v: Int): List0[Int] = ls match {
+ case Nil0() => Cons0(v, Nil0())
+ case Cons0(h, t) =>
+ if (v <= h) {
+ Cons0(v, t)
+ } else {
+ Cons0(h, insSort(t, v))
+ }
+ }
+}
+
+
+case class Cons0[T](h: T, t: List0[T]) extends List0[T]
+case class Nil0[T]() extends List0[T]
+
+@library
+object List0Specs {
+ def snocIndex[T](l : List0[T], t : T, i : Int) : Boolean = {
+ require(0 <= i && i < l.size + 1)
+ // proof:
+ (l match {
+ case Nil0() => true
+ case Cons0(x, xs) => if (i > 0) snocIndex[T](xs, t, i-1) else true
+ }) &&
+ // claim:
+ ((l :+ t).apply(i) == (if (i < l.size) l(i) else t))
+ }.holds
+
+ def reverseIndex[T](l : List0[T], i : Int) : Boolean = {
+ require(0 <= i && i < l.size)
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocIndex(l, x, i) && reverseIndex[T](l,i)
+ }) &&
+ (l.reverse.apply(i) == l.apply(l.size - 1 - i))
+ }.holds
+
+ def appendIndex[T](l1 : List0[T], l2 : List0[T], i : Int) : Boolean = {
+ require(0 <= i && i < l1.size + l2.size)
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => if (i==0) true else appendIndex[T](xs,l2,i-1)
+ }) &&
+ ((l1 ++ l2).apply(i) == (if (i < l1.size) l1(i) else l2(i - l1.size)))
+ }.holds
+
+ def appendAssoc[T](l1 : List0[T], l2 : List0[T], l3 : List0[T]) : Boolean = {
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => appendAssoc(xs,l2,l3)
+ }) &&
+ (((l1 ++ l2) ++ l3) == (l1 ++ (l2 ++ l3)))
+ }.holds
+
+ def snocIsAppend[T](l : List0[T], t : T) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocIsAppend(xs,t)
+ }) &&
+ ((l :+ t) == l ++ Cons0[T](t, Nil0()))
+ }.holds
+
+ def snocAfterAppend[T](l1 : List0[T], l2 : List0[T], t : T) : Boolean = {
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocAfterAppend(xs,l2,t)
+ }) &&
+ ((l1 ++ l2) :+ t == (l1 ++ (l2 :+ t)))
+ }.holds
+
+ def snocReverse[T](l : List0[T], t : T) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocReverse(xs,t)
+ }) &&
+ ((l :+ t).reverse == Cons0(t, l.reverse))
+ }.holds
+
+ def reverseReverse[T](l : List0[T]) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => reverseReverse[T](xs) && snocReverse[T](xs.reverse, x)
+ }) &&
+ (l.reverse.reverse == l)
+ }.holds
+
+ //// my hand calculation shows this should work, but it does not seem to be found
+ //def reverseAppend[T](l1 : List0[T], l2 : List0[T]) : Boolean = {
+ // (l1 match {
+ // case Nil0() => true
+ // case Cons0(x,xs) => {
+ // reverseAppend(xs,l2) &&
+ // snocAfterAppend[T](l2.reverse, xs.reverse, x) &&
+ // l1.reverse == (xs.reverse :+ x)
+ // }
+ // }) &&
+ // ((l1 ++ l2).reverse == (l2.reverse ++ l1.reverse))
+ //}.holds
+}
diff --git a/testcases/repair/List/List1.scala b/testcases/repair/List/List1.scala
new file mode 100644
index 000000000..1e18ca898
--- /dev/null
+++ b/testcases/repair/List/List1.scala
@@ -0,0 +1,420 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.custom
+
+import leon._
+import leon.lang._
+import leon.annotation._
+
+sealed abstract class List0[T] {
+ def size: Int = (this match {
+ case Nil0() => 0
+ case Cons0(h, t) => 1 + t.size
+ }) ensuring (_ >= 0)
+
+ def content: Set[T] = this match {
+ case Nil0() => Set()
+ case Cons0(h, t) => Set(h) ++ t.content
+ }
+
+ def contains(v: T): Boolean = (this match {
+ case Cons0(h, t) if h == v => true
+ case Cons0(_, t) => t.contains(v)
+ case Nil0() => false
+ }) ensuring { res => res == (content contains v) }
+
+ def ++(that: List0[T]): List0[T] = (this match {
+ case Nil0() => that
+ case Cons0(x, xs) => Cons0(x, xs ++ that)
+ }) ensuring { res => (res.content == this.content ++ that.content) && (res.size == this.size + that.size)}
+
+ def head: T = {
+ require(this != Nil0[T]())
+ this match {
+ case Cons0(h, t) => h
+ }
+ }
+
+ def tail: List0[T] = {
+ require(this != Nil0[T]())
+ this match {
+ case Cons0(h, t) => t
+ }
+ }
+
+ def apply(index: Int): T = {
+ require(0 <= index && index < size)
+ if (index == 0) {
+ head
+ } else {
+ tail(index-1)
+ }
+ }
+
+ def ::(t:T): List0[T] = Cons0(t, this)
+
+ def :+(t:T): List0[T] = {
+ this match {
+ case Nil0() => Cons0(t, this)
+ case Cons0(x, xs) => Cons0(x, xs :+ (t))
+ }
+ } ensuring(res => (res.size == size + 1) && (res.content == content ++ Set(t)))
+
+ def reverse: List0[T] = {
+ this match {
+ case Nil0() => this
+ case Cons0(x,xs) => xs.reverse :+ x
+ }
+ } ensuring (res => (res.size == size) && (res.content == content))
+
+ def take(i: Int): List0[T] = (this, i) match {
+ case (Nil0(), _) => Nil0()
+ case (Cons0(h, t), i) =>
+ if (i == 0) {
+ Nil0()
+ } else {
+ Cons0(h, t.take(i-1))
+ }
+ }
+
+ def drop(i: Int): List0[T] = (this, i) match {
+ case (Nil0(), _) => Nil0()
+ case (Cons0(h, t), i) =>
+ if (i == 0) {
+ Cons0(h, t)
+ } else {
+ t.drop(i-1)
+ }
+ }
+
+ def slice(from: Int, to: Int): List0[T] = {
+ require(from < to && to < size && from >= 0)
+ drop(from).take(to-from)
+ }
+
+ def replace(from: T, to: T): List0[T] = this match {
+ case Nil0() => Nil0()
+ case Cons0(h, t) =>
+ val r = t.replace(from, to)
+ if (h == from) {
+ Cons0(to, r)
+ } else {
+ Cons0(h, r)
+ }
+ }
+
+ private def chunk0(s: Int, l: List0[T], acc: List0[T], res: List0[List0[T]], s0: Int): List0[List0[T]] = l match {
+ case Nil0() =>
+ if (acc.size > 0) {
+ res :+ acc
+ } else {
+ res
+ }
+ case Cons0(h, t) =>
+ if (s0 == 0) {
+ chunk0(s, l, Nil0(), res :+ acc, s)
+ } else {
+ chunk0(s, t, acc :+ h, res, s0-1)
+ }
+ }
+
+ def chunks(s: Int): List0[List0[T]] = {
+ require(s > 0)
+
+ chunk0(s, this, Nil0(), Nil0(), s)
+ }
+
+ def zip[B](that: List0[B]): List0[(T, B)] = (this, that) match {
+ case (Cons0(h1, t1), Cons0(h2, t2)) =>
+ Cons0((h1, h2), t1.zip(t2))
+ case (_) =>
+ Nil0()
+ }
+
+ def -(e: T): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (e == h) {
+ t - e
+ } else {
+ Cons0(h, t - e)
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def --(that: List0[T]): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (that.contains(h)) {
+ t -- that
+ } else {
+ Cons0(h, t -- that)
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def &(that: List0[T]): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (that.contains(h)) {
+ Cons0(h, t & that)
+ } else {
+ t & that
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def pad(s: Int, e: T): List0[T] = { (this, s) match {
+ case (_, s) if s <= 0 =>
+ this
+ case (Nil0(), s) =>
+ Cons0(e, Nil0().pad(s-1, e))
+ case (Cons0(h, t), s) =>
+ Cons0(h, t.pad(s-1, e)) // FIXME should be s
+ }} ensuring { res =>
+ ((this,s,e), res) passes {
+ case (Cons0(a,Nil0()), 2, x) => Cons0(a, Cons0(x, Cons0(x, Nil0())))
+ }
+ }
+
+ def find(e: T): Option[Int] = this match {
+ case Nil0() => None()
+ case Cons0(h, t) =>
+ if (h == e) {
+ Some(0)
+ } else {
+ t.find(e) match {
+ case None() => None()
+ case Some(i) => Some(i+1)
+ }
+ }
+ }
+
+ def init: List0[T] = (this match {
+ case Cons0(h, Nil0()) =>
+ Nil0[T]()
+ case Cons0(h, t) =>
+ Cons0[T](h, t.init)
+ case Nil0() =>
+ Nil0[T]()
+ }) ensuring ( (r: List0[T]) => ((r.size < this.size) || (this.size == 0)) )
+
+ def lastOption: Option[T] = this match {
+ case Cons0(h, t) =>
+ t.lastOption.orElse(Some(h))
+ case Nil0() =>
+ None()
+ }
+
+ def firstOption: Option[T] = this match {
+ case Cons0(h, t) =>
+ Some(h)
+ case Nil0() =>
+ None()
+ }
+
+ def unique: List0[T] = this match {
+ case Nil0() => Nil0()
+ case Cons0(h, t) =>
+ Cons0(h, t.unique - h)
+ }
+
+ def splitAt(e: T): List0[List0[T]] = split(Cons0(e, Nil0()))
+
+ def split(seps: List0[T]): List0[List0[T]] = this match {
+ case Cons0(h, t) =>
+ if (seps.contains(h)) {
+ Cons0(Nil0(), t.split(seps))
+ } else {
+ val r = t.split(seps)
+ Cons0(Cons0(h, r.head), r.tail)
+ }
+ case Nil0() =>
+ Cons0(Nil0(), Nil0())
+ }
+
+ def count(e: T): Int = this match {
+ case Cons0(h, t) =>
+ if (h == e) {
+ 1 + t.count(e)
+ } else {
+ t.count(e)
+ }
+ case Nil0() =>
+ 0
+ }
+
+ def evenSplit: (List0[T], List0[T]) = {
+ val c = size/2
+ (take(c), drop(c))
+ }
+
+ def insertAt(pos: Int, l: List0[T]): List0[T] = {
+ if(pos < 0) {
+ insertAt(size + pos, l)
+ } else if(pos == 0) {
+ l ++ this
+ } else {
+ this match {
+ case Cons0(h, t) =>
+ Cons0(h, t.insertAt(pos-1, l))
+ case Nil0() =>
+ l
+ }
+ }
+ }
+
+ def replaceAt(pos: Int, l: List0[T]): List0[T] = {
+ if(pos < 0) {
+ replaceAt(size + pos, l)
+ } else if(pos == 0) {
+ l ++ this.drop(l.size)
+ } else {
+ this match {
+ case Cons0(h, t) =>
+ Cons0(h, t.replaceAt(pos-1, l))
+ case Nil0() =>
+ l
+ }
+ }
+ }
+
+ def rotate(s: Int): List0[T] = {
+ if (s < 0) {
+ rotate(size+s)
+ } else {
+ val s2 = s % size
+ drop(s2) ++ take(s2)
+ }
+ }
+
+ def isEmpty = this match {
+ case Nil0() => true
+ case _ => false
+ }
+
+}
+
+@ignore
+object List0 {
+ def apply[T](elems: T*): List0[T] = ???
+}
+
+@library
+object List0Ops {
+ def flatten[T](ls: List0[List0[T]]): List0[T] = ls match {
+ case Cons0(h, t) => h ++ flatten(t)
+ case Nil0() => Nil0()
+ }
+
+ def isSorted(ls: List0[Int]): Boolean = ls match {
+ case Nil0() => true
+ case Cons0(_, Nil0()) => true
+ case Cons0(h1, Cons0(h2, _)) if(h1 > h2) => false
+ case Cons0(_, t) => isSorted(t)
+ }
+
+ def sorted(ls: List0[Int]): List0[Int] = ls match {
+ case Cons0(h, t) => insSort(sorted(t), h)
+ case Nil0() => Nil0()
+ }
+
+ def insSort(ls: List0[Int], v: Int): List0[Int] = ls match {
+ case Nil0() => Cons0(v, Nil0())
+ case Cons0(h, t) =>
+ if (v <= h) {
+ Cons0(v, t)
+ } else {
+ Cons0(h, insSort(t, v))
+ }
+ }
+}
+
+
+case class Cons0[T](h: T, t: List0[T]) extends List0[T]
+case class Nil0[T]() extends List0[T]
+
+@library
+object List0Specs {
+ def snocIndex[T](l : List0[T], t : T, i : Int) : Boolean = {
+ require(0 <= i && i < l.size + 1)
+ // proof:
+ (l match {
+ case Nil0() => true
+ case Cons0(x, xs) => if (i > 0) snocIndex[T](xs, t, i-1) else true
+ }) &&
+ // claim:
+ ((l :+ t).apply(i) == (if (i < l.size) l(i) else t))
+ }.holds
+
+ def reverseIndex[T](l : List0[T], i : Int) : Boolean = {
+ require(0 <= i && i < l.size)
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocIndex(l, x, i) && reverseIndex[T](l,i)
+ }) &&
+ (l.reverse.apply(i) == l.apply(l.size - 1 - i))
+ }.holds
+
+ def appendIndex[T](l1 : List0[T], l2 : List0[T], i : Int) : Boolean = {
+ require(0 <= i && i < l1.size + l2.size)
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => if (i==0) true else appendIndex[T](xs,l2,i-1)
+ }) &&
+ ((l1 ++ l2).apply(i) == (if (i < l1.size) l1(i) else l2(i - l1.size)))
+ }.holds
+
+ def appendAssoc[T](l1 : List0[T], l2 : List0[T], l3 : List0[T]) : Boolean = {
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => appendAssoc(xs,l2,l3)
+ }) &&
+ (((l1 ++ l2) ++ l3) == (l1 ++ (l2 ++ l3)))
+ }.holds
+
+ def snocIsAppend[T](l : List0[T], t : T) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocIsAppend(xs,t)
+ }) &&
+ ((l :+ t) == l ++ Cons0[T](t, Nil0()))
+ }.holds
+
+ def snocAfterAppend[T](l1 : List0[T], l2 : List0[T], t : T) : Boolean = {
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocAfterAppend(xs,l2,t)
+ }) &&
+ ((l1 ++ l2) :+ t == (l1 ++ (l2 :+ t)))
+ }.holds
+
+ def snocReverse[T](l : List0[T], t : T) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocReverse(xs,t)
+ }) &&
+ ((l :+ t).reverse == Cons0(t, l.reverse))
+ }.holds
+
+ def reverseReverse[T](l : List0[T]) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => reverseReverse[T](xs) && snocReverse[T](xs.reverse, x)
+ }) &&
+ (l.reverse.reverse == l)
+ }.holds
+
+ //// my hand calculation shows this should work, but it does not seem to be found
+ //def reverseAppend[T](l1 : List0[T], l2 : List0[T]) : Boolean = {
+ // (l1 match {
+ // case Nil0() => true
+ // case Cons0(x,xs) => {
+ // reverseAppend(xs,l2) &&
+ // snocAfterAppend[T](l2.reverse, xs.reverse, x) &&
+ // l1.reverse == (xs.reverse :+ x)
+ // }
+ // }) &&
+ // ((l1 ++ l2).reverse == (l2.reverse ++ l1.reverse))
+ //}.holds
+}
diff --git a/testcases/repair/List/List2.scala b/testcases/repair/List/List2.scala
new file mode 100644
index 000000000..e3246d5e8
--- /dev/null
+++ b/testcases/repair/List/List2.scala
@@ -0,0 +1,426 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.custom
+
+import leon._
+import leon.lang._
+import leon.annotation._
+
+sealed abstract class List0[T] {
+ def size: Int = (this match {
+ case Nil0() => 0
+ case Cons0(h, t) => 1 + t.size
+ }) ensuring (_ >= 0)
+
+ def content: Set[T] = this match {
+ case Nil0() => Set()
+ case Cons0(h, t) => Set(h) ++ t.content
+ }
+
+ def contains(v: T): Boolean = (this match {
+ case Cons0(h, t) if h == v => true
+ case Cons0(_, t) => t.contains(v)
+ case Nil0() => false
+ }) ensuring { res => res == (content contains v) }
+
+ def ++(that: List0[T]): List0[T] = (this match {
+ case Nil0() => that
+ case Cons0(x, xs) => xs ++ that // FIXME did not Cons
+ }) ensuring { res =>
+ res.content == this.content ++ that.content &&
+ res.size == this.size + that.size &&
+ (((this, that), res) passes {
+ case ( x@Cons0(x1, Cons0(x2, Nil0())), y) => x
+ })
+ }
+
+ def head: T = {
+ require(this != Nil0[T]())
+ this match {
+ case Cons0(h, t) => h
+ }
+ }
+
+ def tail: List0[T] = {
+ require(this != Nil0[T]())
+ this match {
+ case Cons0(h, t) => t
+ }
+ }
+
+ def apply(index: Int): T = {
+ require(0 <= index && index < size)
+ if (index == 0) {
+ head
+ } else {
+ tail(index-1)
+ }
+ }
+
+ def ::(t:T): List0[T] = Cons0(t, this)
+
+ def :+(t:T): List0[T] = {
+ this match {
+ case Nil0() => Cons0(t, this)
+ case Cons0(x, xs) => Cons0(x, xs :+ (t))
+ }
+ } ensuring(res => (res.size == size + 1) && (res.content == content ++ Set(t)))
+
+ def reverse: List0[T] = {
+ this match {
+ case Nil0() => this
+ case Cons0(x,xs) => xs.reverse :+ x
+ }
+ } ensuring (res => (res.size == size) && (res.content == content))
+
+ def take(i: Int): List0[T] = (this, i) match {
+ case (Nil0(), _) => Nil0()
+ case (Cons0(h, t), i) =>
+ if (i == 0) {
+ Nil0()
+ } else {
+ Cons0(h, t.take(i-1))
+ }
+ }
+
+ def drop(i: Int): List0[T] = (this, i) match {
+ case (Nil0(), _) => Nil0()
+ case (Cons0(h, t), i) =>
+ if (i == 0) {
+ Cons0(h, t)
+ } else {
+ t.drop(i-1)
+ }
+ }
+
+ def slice(from: Int, to: Int): List0[T] = {
+ require(from < to && to < size && from >= 0)
+ drop(from).take(to-from)
+ }
+
+ def replace(from: T, to: T): List0[T] = this match {
+ case Nil0() => Nil0()
+ case Cons0(h, t) =>
+ val r = t.replace(from, to)
+ if (h == from) {
+ Cons0(to, r)
+ } else {
+ Cons0(h, r)
+ }
+ }
+
+ private def chunk0(s: Int, l: List0[T], acc: List0[T], res: List0[List0[T]], s0: Int): List0[List0[T]] = l match {
+ case Nil0() =>
+ if (acc.size > 0) {
+ res :+ acc
+ } else {
+ res
+ }
+ case Cons0(h, t) =>
+ if (s0 == 0) {
+ chunk0(s, l, Nil0(), res :+ acc, s)
+ } else {
+ chunk0(s, t, acc :+ h, res, s0-1)
+ }
+ }
+
+ def chunks(s: Int): List0[List0[T]] = {
+ require(s > 0)
+
+ chunk0(s, this, Nil0(), Nil0(), s)
+ }
+
+ def zip[B](that: List0[B]): List0[(T, B)] = (this, that) match {
+ case (Cons0(h1, t1), Cons0(h2, t2)) =>
+ Cons0((h1, h2), t1.zip(t2))
+ case (_) =>
+ Nil0()
+ }
+
+ def -(e: T): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (e == h) {
+ t - e
+ } else {
+ Cons0(h, t - e)
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def --(that: List0[T]): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (that.contains(h)) {
+ t -- that
+ } else {
+ Cons0(h, t -- that)
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def &(that: List0[T]): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (that.contains(h)) {
+ Cons0(h, t & that)
+ } else {
+ t & that
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def pad(s: Int, e: T): List0[T] = { (this, s) match {
+ case (_, s) if s <= 0 =>
+ this
+ case (Nil0(), s) =>
+ Cons0(e, Nil0().pad(s-1, e))
+ case (Cons0(h, t), s) =>
+ Cons0(h, t.pad(s, e))
+ }} ensuring { res =>
+ ((this,s,e), res) passes {
+ case (Cons0(a,Nil0()), 2, x) => Cons0(a, Cons0(x, Cons0(x, Nil0())))
+ }
+ }
+
+ def find(e: T): Option[Int] = this match {
+ case Nil0() => None()
+ case Cons0(h, t) =>
+ if (h == e) {
+ Some(0)
+ } else {
+ t.find(e) match {
+ case None() => None()
+ case Some(i) => Some(i+1)
+ }
+ }
+ }
+
+ def init: List0[T] = (this match {
+ case Cons0(h, Nil0()) =>
+ Nil0[T]()
+ case Cons0(h, t) =>
+ Cons0[T](h, t.init)
+ case Nil0() =>
+ Nil0[T]()
+ }) ensuring ( (r: List0[T]) => ((r.size < this.size) || (this.size == 0)) )
+
+ def lastOption: Option[T] = this match {
+ case Cons0(h, t) =>
+ t.lastOption.orElse(Some(h))
+ case Nil0() =>
+ None()
+ }
+
+ def firstOption: Option[T] = this match {
+ case Cons0(h, t) =>
+ Some(h)
+ case Nil0() =>
+ None()
+ }
+
+ def unique: List0[T] = this match {
+ case Nil0() => Nil0()
+ case Cons0(h, t) =>
+ Cons0(h, t.unique - h)
+ }
+
+ def splitAt(e: T): List0[List0[T]] = split(Cons0(e, Nil0()))
+
+ def split(seps: List0[T]): List0[List0[T]] = this match {
+ case Cons0(h, t) =>
+ if (seps.contains(h)) {
+ Cons0(Nil0(), t.split(seps))
+ } else {
+ val r = t.split(seps)
+ Cons0(Cons0(h, r.head), r.tail)
+ }
+ case Nil0() =>
+ Cons0(Nil0(), Nil0())
+ }
+
+ def count(e: T): Int = this match {
+ case Cons0(h, t) =>
+ if (h == e) {
+ 1 + t.count(e)
+ } else {
+ t.count(e)
+ }
+ case Nil0() =>
+ 0
+ }
+
+ def evenSplit: (List0[T], List0[T]) = {
+ val c = size/2
+ (take(c), drop(c))
+ }
+
+ def insertAt(pos: Int, l: List0[T]): List0[T] = {
+ if(pos < 0) {
+ insertAt(size + pos, l)
+ } else if(pos == 0) {
+ l ++ this
+ } else {
+ this match {
+ case Cons0(h, t) =>
+ Cons0(h, t.insertAt(pos-1, l))
+ case Nil0() =>
+ l
+ }
+ }
+ }
+
+ def replaceAt(pos: Int, l: List0[T]): List0[T] = {
+ if(pos < 0) {
+ replaceAt(size + pos, l)
+ } else if(pos == 0) {
+ l ++ this.drop(l.size)
+ } else {
+ this match {
+ case Cons0(h, t) =>
+ Cons0(h, t.replaceAt(pos-1, l))
+ case Nil0() =>
+ l
+ }
+ }
+ }
+
+ def rotate(s: Int): List0[T] = {
+ if (s < 0) {
+ rotate(size+s)
+ } else {
+ val s2 = s % size
+ drop(s2) ++ take(s2)
+ }
+ }
+
+ def isEmpty = this match {
+ case Nil0() => true
+ case _ => false
+ }
+
+}
+
+@ignore
+object List0 {
+ def apply[T](elems: T*): List0[T] = ???
+}
+
+@library
+object List0Ops {
+ def flatten[T](ls: List0[List0[T]]): List0[T] = ls match {
+ case Cons0(h, t) => h ++ flatten(t)
+ case Nil0() => Nil0()
+ }
+
+ def isSorted(ls: List0[Int]): Boolean = ls match {
+ case Nil0() => true
+ case Cons0(_, Nil0()) => true
+ case Cons0(h1, Cons0(h2, _)) if(h1 > h2) => false
+ case Cons0(_, t) => isSorted(t)
+ }
+
+ def sorted(ls: List0[Int]): List0[Int] = ls match {
+ case Cons0(h, t) => insSort(sorted(t), h)
+ case Nil0() => Nil0()
+ }
+
+ def insSort(ls: List0[Int], v: Int): List0[Int] = ls match {
+ case Nil0() => Cons0(v, Nil0())
+ case Cons0(h, t) =>
+ if (v <= h) {
+ Cons0(v, t)
+ } else {
+ Cons0(h, insSort(t, v))
+ }
+ }
+}
+
+
+case class Cons0[T](h: T, t: List0[T]) extends List0[T]
+case class Nil0[T]() extends List0[T]
+
+@library
+object List0Specs {
+ def snocIndex[T](l : List0[T], t : T, i : Int) : Boolean = {
+ require(0 <= i && i < l.size + 1)
+ // proof:
+ (l match {
+ case Nil0() => true
+ case Cons0(x, xs) => if (i > 0) snocIndex[T](xs, t, i-1) else true
+ }) &&
+ // claim:
+ ((l :+ t).apply(i) == (if (i < l.size) l(i) else t))
+ }.holds
+
+ def reverseIndex[T](l : List0[T], i : Int) : Boolean = {
+ require(0 <= i && i < l.size)
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocIndex(l, x, i) && reverseIndex[T](l,i)
+ }) &&
+ (l.reverse.apply(i) == l.apply(l.size - 1 - i))
+ }.holds
+
+ def appendIndex[T](l1 : List0[T], l2 : List0[T], i : Int) : Boolean = {
+ require(0 <= i && i < l1.size + l2.size)
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => if (i==0) true else appendIndex[T](xs,l2,i-1)
+ }) &&
+ ((l1 ++ l2).apply(i) == (if (i < l1.size) l1(i) else l2(i - l1.size)))
+ }.holds
+
+ def appendAssoc[T](l1 : List0[T], l2 : List0[T], l3 : List0[T]) : Boolean = {
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => appendAssoc(xs,l2,l3)
+ }) &&
+ (((l1 ++ l2) ++ l3) == (l1 ++ (l2 ++ l3)))
+ }.holds
+
+ def snocIsAppend[T](l : List0[T], t : T) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocIsAppend(xs,t)
+ }) &&
+ ((l :+ t) == l ++ Cons0[T](t, Nil0()))
+ }.holds
+
+ def snocAfterAppend[T](l1 : List0[T], l2 : List0[T], t : T) : Boolean = {
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocAfterAppend(xs,l2,t)
+ }) &&
+ ((l1 ++ l2) :+ t == (l1 ++ (l2 :+ t)))
+ }.holds
+
+ def snocReverse[T](l : List0[T], t : T) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocReverse(xs,t)
+ }) &&
+ ((l :+ t).reverse == Cons0(t, l.reverse))
+ }.holds
+
+ def reverseReverse[T](l : List0[T]) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => reverseReverse[T](xs) && snocReverse[T](xs.reverse, x)
+ }) &&
+ (l.reverse.reverse == l)
+ }.holds
+
+ //// my hand calculation shows this should work, but it does not seem to be found
+ //def reverseAppend[T](l1 : List0[T], l2 : List0[T]) : Boolean = {
+ // (l1 match {
+ // case Nil0() => true
+ // case Cons0(x,xs) => {
+ // reverseAppend(xs,l2) &&
+ // snocAfterAppend[T](l2.reverse, xs.reverse, x) &&
+ // l1.reverse == (xs.reverse :+ x)
+ // }
+ // }) &&
+ // ((l1 ++ l2).reverse == (l2.reverse ++ l1.reverse))
+ //}.holds
+}
diff --git a/testcases/repair/List/List3.scala b/testcases/repair/List/List3.scala
new file mode 100644
index 000000000..87a1214c7
--- /dev/null
+++ b/testcases/repair/List/List3.scala
@@ -0,0 +1,428 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.custom
+
+import leon._
+import leon.lang._
+import leon.annotation._
+
+sealed abstract class List0[T] {
+ def size: Int = (this match {
+ case Nil0() => 0
+ case Cons0(h, t) => 1 + t.size
+ }) ensuring (_ >= 0)
+
+ def content: Set[T] = this match {
+ case Nil0() => Set()
+ case Cons0(h, t) => Set(h) ++ t.content
+ }
+
+ def contains(v: T): Boolean = (this match {
+ case Cons0(h, t) if h == v => true
+ case Cons0(_, t) => t.contains(v)
+ case Nil0() => false
+ }) ensuring { res => res == (content contains v) }
+
+ def ++(that: List0[T]): List0[T] = (this match {
+ case Nil0() => that
+ case Cons0(x, xs) => Cons0(x, xs ++ that)
+ }) ensuring { res => (res.content == this.content ++ that.content) && (res.size == this.size + that.size)}
+
+ def head: T = {
+ require(this != Nil0[T]())
+ this match {
+ case Cons0(h, t) => h
+ }
+ }
+
+ def tail: List0[T] = {
+ require(this != Nil0[T]())
+ this match {
+ case Cons0(h, t) => t
+ }
+ }
+
+ def apply(index: Int): T = {
+ require(0 <= index && index < size)
+ if (index == 0) {
+ head
+ } else {
+ tail(index-1)
+ }
+ }
+
+ def ::(t:T): List0[T] = Cons0(t, this)
+
+ def ap(t:T): List0[T] = {
+ this match {
+ case Nil0() => Nil0() // FIXME did not add element
+ case Cons0(x, xs) => Cons0(x, xs ap (t))
+ }
+ } ensuring(res => (res.size == size + 1) && (res.content == content ++ Set(t)))
+
+
+ def :+(t:T) = this ap t
+
+ def reverse: List0[T] = {
+ this match {
+ case Nil0() => this
+ case Cons0(x,xs) => xs.reverse :+ x
+ }
+ } ensuring (res => (res.size == size) && (res.content == content))
+
+ def take(i: Int): List0[T] = (this, i) match {
+ case (Nil0(), _) => Nil0()
+ case (Cons0(h, t), i) =>
+ if (i == 0) {
+ Nil0()
+ } else {
+ Cons0(h, t.take(i-1))
+ }
+ }
+
+ def drop(i: Int): List0[T] = (this, i) match {
+ case (Nil0(), _) => Nil0()
+ case (Cons0(h, t), i) =>
+ if (i == 0) {
+ Cons0(h, t)
+ } else {
+ t.drop(i-1)
+ }
+ }
+
+ def slice(from: Int, to: Int): List0[T] = {
+ require(from < to && to < size && from >= 0)
+ drop(from).take(to-from)
+ }
+
+ def replace(from: T, to: T): List0[T] = this match {
+ case Nil0() => Nil0()
+ case Cons0(h, t) =>
+ val r = t.replace(from, to)
+ if (h == from) {
+ Cons0(to, r)
+ } else {
+ Cons0(h, r)
+ }
+ }
+
+ private def chunk0(s: Int, l: List0[T], acc: List0[T], res: List0[List0[T]], s0: Int): List0[List0[T]] = l match {
+ case Nil0() =>
+ if (acc.size > 0) {
+ res :+ acc
+ } else {
+ res
+ }
+ case Cons0(h, t) =>
+ if (s0 == 0) {
+ chunk0(s, l, Nil0(), res :+ acc, s)
+ } else {
+ chunk0(s, t, acc :+ h, res, s0-1)
+ }
+ }
+
+ def chunks(s: Int): List0[List0[T]] = {
+ require(s > 0)
+
+ chunk0(s, this, Nil0(), Nil0(), s)
+ }
+
+ def zip[B](that: List0[B]): List0[(T, B)] = (this, that) match {
+ case (Cons0(h1, t1), Cons0(h2, t2)) =>
+ Cons0((h1, h2), t1.zip(t2))
+ case (_) =>
+ Nil0()
+ }
+
+ def -(e: T): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (e == h) {
+ t - e
+ } else {
+ Cons0(h, t - e)
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def --(that: List0[T]): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (that.contains(h)) {
+ t -- that
+ } else {
+ Cons0(h, t -- that)
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def &(that: List0[T]): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (that.contains(h)) {
+ Cons0(h, t & that)
+ } else {
+ t & that
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def pad(s: Int, e: T): List0[T] = { (this, s) match {
+ case (_, s) if s <= 0 =>
+ this
+ case (Nil0(), s) =>
+ Cons0(e, Nil0().pad(s-1, e))
+ case (Cons0(h, t), s) =>
+ Cons0(h, t.pad(s, e))
+ }} ensuring { res =>
+ ((this,s,e), res) passes {
+ case (Cons0(a,Nil0()), 2, x) => Cons0(a, Cons0(x, Cons0(x, Nil0())))
+ }
+ }
+
+ def find(e: T): Option[Int] = this match {
+ case Nil0() => None()
+ case Cons0(h, t) =>
+ if (h == e) {
+ Some(0)
+ } else {
+ t.find(e) match {
+ case None() => None()
+ case Some(i) => Some(i+1)
+ }
+ }
+ }
+
+ def init: List0[T] = (this match {
+ case Cons0(h, Nil0()) =>
+ Nil0[T]()
+ //case Cons0(h, t) =>
+ // Cons0[T](h, t.init)
+ case Nil0() =>
+ Nil0[T]()
+ }) ensuring ( (r: List0[T]) =>
+ ((r.size < this.size) || (this.size == 0)) &&
+ ((this, r) passes {
+ case Cons0(a, Cons0(b, Cons0(c, Nil0()))) => Cons0(a, Cons0(b, Nil0()))
+ })
+ )
+
+ def lastOption: Option[T] = this match {
+ case Cons0(h, t) =>
+ t.lastOption.orElse(Some(h))
+ case Nil0() =>
+ None()
+ }
+
+ def firstOption: Option[T] = this match {
+ case Cons0(h, t) =>
+ Some(h)
+ case Nil0() =>
+ None()
+ }
+
+ def unique: List0[T] = this match {
+ case Nil0() => Nil0()
+ case Cons0(h, t) =>
+ Cons0(h, t.unique - h)
+ }
+
+ def splitAt(e: T): List0[List0[T]] = split(Cons0(e, Nil0()))
+
+ def split(seps: List0[T]): List0[List0[T]] = this match {
+ case Cons0(h, t) =>
+ if (seps.contains(h)) {
+ Cons0(Nil0(), t.split(seps))
+ } else {
+ val r = t.split(seps)
+ Cons0(Cons0(h, r.head), r.tail)
+ }
+ case Nil0() =>
+ Cons0(Nil0(), Nil0())
+ }
+
+ def count(e: T): Int = this match {
+ case Cons0(h, t) =>
+ if (h == e) {
+ 1 + t.count(e)
+ } else {
+ t.count(e)
+ }
+ case Nil0() =>
+ 0
+ }
+
+ def evenSplit: (List0[T], List0[T]) = {
+ val c = size/2
+ (take(c), drop(c))
+ }
+
+ def insertAt(pos: Int, l: List0[T]): List0[T] = {
+ if(pos < 0) {
+ insertAt(size + pos, l)
+ } else if(pos == 0) {
+ l ++ this
+ } else {
+ this match {
+ case Cons0(h, t) =>
+ Cons0(h, t.insertAt(pos-1, l))
+ case Nil0() =>
+ l
+ }
+ }
+ }
+
+ def replaceAt(pos: Int, l: List0[T]): List0[T] = {
+ if(pos < 0) {
+ replaceAt(size + pos, l)
+ } else if(pos == 0) {
+ l ++ this.drop(l.size)
+ } else {
+ this match {
+ case Cons0(h, t) =>
+ Cons0(h, t.replaceAt(pos-1, l))
+ case Nil0() =>
+ l
+ }
+ }
+ }
+
+ def rotate(s: Int): List0[T] = {
+ if (s < 0) {
+ rotate(size+s)
+ } else {
+ val s2 = s % size
+ drop(s2) ++ take(s2)
+ }
+ }
+
+ def isEmpty = this match {
+ case Nil0() => true
+ case _ => false
+ }
+
+}
+
+@ignore
+object List0 {
+ def apply[T](elems: T*): List0[T] = ???
+}
+
+@library
+object List0Ops {
+ def flatten[T](ls: List0[List0[T]]): List0[T] = ls match {
+ case Cons0(h, t) => h ++ flatten(t)
+ case Nil0() => Nil0()
+ }
+
+ def isSorted(ls: List0[Int]): Boolean = ls match {
+ case Nil0() => true
+ case Cons0(_, Nil0()) => true
+ case Cons0(h1, Cons0(h2, _)) if(h1 > h2) => false
+ case Cons0(_, t) => isSorted(t)
+ }
+
+ def sorted(ls: List0[Int]): List0[Int] = ls match {
+ case Cons0(h, t) => insSort(sorted(t), h)
+ case Nil0() => Nil0()
+ }
+
+ def insSort(ls: List0[Int], v: Int): List0[Int] = ls match {
+ case Nil0() => Cons0(v, Nil0())
+ case Cons0(h, t) =>
+ if (v <= h) {
+ Cons0(v, t)
+ } else {
+ Cons0(h, insSort(t, v))
+ }
+ }
+}
+
+
+case class Cons0[T](h: T, t: List0[T]) extends List0[T]
+case class Nil0[T]() extends List0[T]
+
+@library
+object List0Specs {
+ def snocIndex[T](l : List0[T], t : T, i : Int) : Boolean = {
+ require(0 <= i && i < l.size + 1)
+ // proof:
+ (l match {
+ case Nil0() => true
+ case Cons0(x, xs) => if (i > 0) snocIndex[T](xs, t, i-1) else true
+ }) &&
+ // claim:
+ ((l :+ t).apply(i) == (if (i < l.size) l(i) else t))
+ }.holds
+
+ def reverseIndex[T](l : List0[T], i : Int) : Boolean = {
+ require(0 <= i && i < l.size)
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocIndex(l, x, i) && reverseIndex[T](l,i)
+ }) &&
+ (l.reverse.apply(i) == l.apply(l.size - 1 - i))
+ }.holds
+
+ def appendIndex[T](l1 : List0[T], l2 : List0[T], i : Int) : Boolean = {
+ require(0 <= i && i < l1.size + l2.size)
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => if (i==0) true else appendIndex[T](xs,l2,i-1)
+ }) &&
+ ((l1 ++ l2).apply(i) == (if (i < l1.size) l1(i) else l2(i - l1.size)))
+ }.holds
+
+ def appendAssoc[T](l1 : List0[T], l2 : List0[T], l3 : List0[T]) : Boolean = {
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => appendAssoc(xs,l2,l3)
+ }) &&
+ (((l1 ++ l2) ++ l3) == (l1 ++ (l2 ++ l3)))
+ }.holds
+
+ def snocIsAppend[T](l : List0[T], t : T) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocIsAppend(xs,t)
+ }) &&
+ ((l :+ t) == l ++ Cons0[T](t, Nil0()))
+ }.holds
+
+ def snocAfterAppend[T](l1 : List0[T], l2 : List0[T], t : T) : Boolean = {
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocAfterAppend(xs,l2,t)
+ }) &&
+ ((l1 ++ l2) :+ t == (l1 ++ (l2 :+ t)))
+ }.holds
+
+ def snocReverse[T](l : List0[T], t : T) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocReverse(xs,t)
+ }) &&
+ ((l :+ t).reverse == Cons0(t, l.reverse))
+ }.holds
+
+ def reverseReverse[T](l : List0[T]) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => reverseReverse[T](xs) && snocReverse[T](xs.reverse, x)
+ }) &&
+ (l.reverse.reverse == l)
+ }.holds
+
+ //// my hand calculation shows this should work, but it does not seem to be found
+ //def reverseAppend[T](l1 : List0[T], l2 : List0[T]) : Boolean = {
+ // (l1 match {
+ // case Nil0() => true
+ // case Cons0(x,xs) => {
+ // reverseAppend(xs,l2) &&
+ // snocAfterAppend[T](l2.reverse, xs.reverse, x) &&
+ // l1.reverse == (xs.reverse :+ x)
+ // }
+ // }) &&
+ // ((l1 ++ l2).reverse == (l2.reverse ++ l1.reverse))
+ //}.holds
+}
diff --git a/testcases/repair/List/List4.scala b/testcases/repair/List/List4.scala
new file mode 100644
index 000000000..210a5544b
--- /dev/null
+++ b/testcases/repair/List/List4.scala
@@ -0,0 +1,420 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.custom
+
+import leon._
+import leon.lang._
+import leon.annotation._
+
+sealed abstract class List0[T] {
+ def size: Int = (this match {
+ case Nil0() => 0
+ case Cons0(h, t) => 1 + t.size
+ }) ensuring (_ >= 0)
+
+ def content: Set[T] = this match {
+ case Nil0() => Set()
+ case Cons0(h, t) => Set(h) ++ t.content
+ }
+
+ def contains(v: T): Boolean = (this match {
+ case Cons0(h, t) if h == v => true
+ case Cons0(_, t) => t.contains(v)
+ case Nil0() => false
+ }) ensuring { res => res == (content contains v) }
+
+ def ++(that: List0[T]): List0[T] = (this match {
+ case Nil0() => that
+ case Cons0(x, xs) => Cons0(x, xs ++ that)
+ }) ensuring { res => (res.content == this.content ++ that.content) && (res.size == this.size + that.size)}
+
+ def head: T = {
+ require(this != Nil0[T]())
+ this match {
+ case Cons0(h, t) => h
+ }
+ }
+
+ def tail: List0[T] = {
+ require(this != Nil0[T]())
+ this match {
+ case Cons0(h, t) => t
+ }
+ }
+
+ def apply(index: Int): T = {
+ require(0 <= index && index < size)
+ if (index == 0) {
+ head
+ } else {
+ tail(index-1)
+ }
+ }
+
+ def ::(t:T): List0[T] = Cons0(t, this)
+
+ def :+(t:T): List0[T] = {
+ this match {
+ case Nil0() => Cons0(t, this)
+ case Cons0(x, xs) => Cons0(x, xs :+ (t))
+ }
+ } ensuring(res => (res.size == size + 1) && (res.content == content ++ Set(t)))
+
+ def reverse: List0[T] = {
+ this match {
+ case Nil0() => this
+ case Cons0(x,xs) => xs.reverse :+ x
+ }
+ } ensuring (res => (res.size == size) && (res.content == content))
+
+ def take(i: Int): List0[T] = (this, i) match {
+ case (Nil0(), _) => Nil0()
+ case (Cons0(h, t), i) =>
+ if (i == 0) {
+ Nil0()
+ } else {
+ Cons0(h, t.take(i-1))
+ }
+ }
+
+ def drop(i: Int): List0[T] = { (this, i) match {
+ case (Nil0(), _) => Nil0()
+ case (Cons0(h, t), i) =>
+ t.drop(i-1) //FIXME missing if-split
+ }} ensuring { res => ((this, i), res) passes {
+ case (l@Cons0(_, Nil0()), 42) => l
+ case (Cons0(a, t), 0) => t
+ case (Cons0(a, Cons0(b, Nil0())), 1) => Cons0(a, Nil0())
+ }}
+
+ def slice(from: Int, to: Int): List0[T] = {
+ require(from < to && to < size && from >= 0)
+ drop(from).take(to-from)
+ }
+
+ def replace(from: T, to: T): List0[T] = this match {
+ case Nil0() => Nil0()
+ case Cons0(h, t) =>
+ val r = t.replace(from, to)
+ if (h == from) {
+ Cons0(to, r)
+ } else {
+ Cons0(h, r)
+ }
+ }
+
+ private def chunk0(s: Int, l: List0[T], acc: List0[T], res: List0[List0[T]], s0: Int): List0[List0[T]] = l match {
+ case Nil0() =>
+ if (acc.size > 0) {
+ res :+ acc
+ } else {
+ res
+ }
+ case Cons0(h, t) =>
+ if (s0 == 0) {
+ chunk0(s, l, Nil0(), res :+ acc, s)
+ } else {
+ chunk0(s, t, acc :+ h, res, s0-1)
+ }
+ }
+
+ def chunks(s: Int): List0[List0[T]] = {
+ require(s > 0)
+
+ chunk0(s, this, Nil0(), Nil0(), s)
+ }
+
+ def zip[B](that: List0[B]): List0[(T, B)] = (this, that) match {
+ case (Cons0(h1, t1), Cons0(h2, t2)) =>
+ Cons0((h1, h2), t1.zip(t2))
+ case (_) =>
+ Nil0()
+ }
+
+ def -(e: T): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (e == h) {
+ t - e
+ } else {
+ Cons0(h, t - e)
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def --(that: List0[T]): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (that.contains(h)) {
+ t -- that
+ } else {
+ Cons0(h, t -- that)
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def &(that: List0[T]): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (that.contains(h)) {
+ Cons0(h, t & that)
+ } else {
+ t & that
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def pad(s: Int, e: T): List0[T] = { (this, s) match {
+ case (_, s) if s <= 0 =>
+ this
+ case (Nil0(), s) =>
+ Cons0(e, Nil0().pad(s-1, e))
+ case (Cons0(h, t), s) =>
+ Cons0(h, t.pad(s, e))
+ }} ensuring { res =>
+ ((this,s,e), res) passes {
+ case (Cons0(a,Nil0()), 2, x) => Cons0(a, Cons0(x, Cons0(x, Nil0())))
+ }
+ }
+
+ def find(e: T): Option[Int] = this match {
+ case Nil0() => None()
+ case Cons0(h, t) =>
+ if (h == e) {
+ Some(0)
+ } else {
+ t.find(e) match {
+ case None() => None()
+ case Some(i) => Some(i+1)
+ }
+ }
+ }
+
+ def init: List0[T] = (this match {
+ case Cons0(h, Nil0()) =>
+ Nil0[T]()
+ case Cons0(h, t) =>
+ Cons0[T](h, t.init)
+ case Nil0() =>
+ Nil0[T]()
+ }) ensuring ( (r: List0[T]) => ((r.size < this.size) || (this.size == 0)) )
+
+ def lastOption: Option[T] = this match {
+ case Cons0(h, t) =>
+ t.lastOption.orElse(Some(h))
+ case Nil0() =>
+ None()
+ }
+
+ def firstOption: Option[T] = this match {
+ case Cons0(h, t) =>
+ Some(h)
+ case Nil0() =>
+ None()
+ }
+
+ def unique: List0[T] = this match {
+ case Nil0() => Nil0()
+ case Cons0(h, t) =>
+ Cons0(h, t.unique - h)
+ }
+
+ def splitAt(e: T): List0[List0[T]] = split(Cons0(e, Nil0()))
+
+ def split(seps: List0[T]): List0[List0[T]] = this match {
+ case Cons0(h, t) =>
+ if (seps.contains(h)) {
+ Cons0(Nil0(), t.split(seps))
+ } else {
+ val r = t.split(seps)
+ Cons0(Cons0(h, r.head), r.tail)
+ }
+ case Nil0() =>
+ Cons0(Nil0(), Nil0())
+ }
+
+ def count(e: T): Int = this match {
+ case Cons0(h, t) =>
+ if (h == e) {
+ 1 + t.count(e)
+ } else {
+ t.count(e)
+ }
+ case Nil0() =>
+ 0
+ }
+
+ def evenSplit: (List0[T], List0[T]) = {
+ val c = size/2
+ (take(c), drop(c))
+ }
+
+ def insertAt(pos: Int, l: List0[T]): List0[T] = {
+ if(pos < 0) {
+ insertAt(size + pos, l)
+ } else if(pos == 0) {
+ l ++ this
+ } else {
+ this match {
+ case Cons0(h, t) =>
+ Cons0(h, t.insertAt(pos-1, l))
+ case Nil0() =>
+ l
+ }
+ }
+ }
+
+ def replaceAt(pos: Int, l: List0[T]): List0[T] = {
+ if(pos < 0) {
+ replaceAt(size + pos, l)
+ } else if(pos == 0) {
+ l ++ this.drop(l.size)
+ } else {
+ this match {
+ case Cons0(h, t) =>
+ Cons0(h, t.replaceAt(pos-1, l))
+ case Nil0() =>
+ l
+ }
+ }
+ }
+
+ def rotate(s: Int): List0[T] = {
+ if (s < 0) {
+ rotate(size+s)
+ } else {
+ val s2 = s % size
+ drop(s2) ++ take(s2)
+ }
+ }
+
+ def isEmpty = this match {
+ case Nil0() => true
+ case _ => false
+ }
+
+}
+
+@ignore
+object List0 {
+ def apply[T](elems: T*): List0[T] = ???
+}
+
+@library
+object List0Ops {
+ def flatten[T](ls: List0[List0[T]]): List0[T] = ls match {
+ case Cons0(h, t) => h ++ flatten(t)
+ case Nil0() => Nil0()
+ }
+
+ def isSorted(ls: List0[Int]): Boolean = ls match {
+ case Nil0() => true
+ case Cons0(_, Nil0()) => true
+ case Cons0(h1, Cons0(h2, _)) if(h1 > h2) => false
+ case Cons0(_, t) => isSorted(t)
+ }
+
+ def sorted(ls: List0[Int]): List0[Int] = ls match {
+ case Cons0(h, t) => insSort(sorted(t), h)
+ case Nil0() => Nil0()
+ }
+
+ def insSort(ls: List0[Int], v: Int): List0[Int] = ls match {
+ case Nil0() => Cons0(v, Nil0())
+ case Cons0(h, t) =>
+ if (v <= h) {
+ Cons0(v, t)
+ } else {
+ Cons0(h, insSort(t, v))
+ }
+ }
+}
+
+
+case class Cons0[T](h: T, t: List0[T]) extends List0[T]
+case class Nil0[T]() extends List0[T]
+
+@library
+object List0Specs {
+ def snocIndex[T](l : List0[T], t : T, i : Int) : Boolean = {
+ require(0 <= i && i < l.size + 1)
+ // proof:
+ (l match {
+ case Nil0() => true
+ case Cons0(x, xs) => if (i > 0) snocIndex[T](xs, t, i-1) else true
+ }) &&
+ // claim:
+ ((l :+ t).apply(i) == (if (i < l.size) l(i) else t))
+ }.holds
+
+ def reverseIndex[T](l : List0[T], i : Int) : Boolean = {
+ require(0 <= i && i < l.size)
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocIndex(l, x, i) && reverseIndex[T](l,i)
+ }) &&
+ (l.reverse.apply(i) == l.apply(l.size - 1 - i))
+ }.holds
+
+ def appendIndex[T](l1 : List0[T], l2 : List0[T], i : Int) : Boolean = {
+ require(0 <= i && i < l1.size + l2.size)
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => if (i==0) true else appendIndex[T](xs,l2,i-1)
+ }) &&
+ ((l1 ++ l2).apply(i) == (if (i < l1.size) l1(i) else l2(i - l1.size)))
+ }.holds
+
+ def appendAssoc[T](l1 : List0[T], l2 : List0[T], l3 : List0[T]) : Boolean = {
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => appendAssoc(xs,l2,l3)
+ }) &&
+ (((l1 ++ l2) ++ l3) == (l1 ++ (l2 ++ l3)))
+ }.holds
+
+ def snocIsAppend[T](l : List0[T], t : T) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocIsAppend(xs,t)
+ }) &&
+ ((l :+ t) == l ++ Cons0[T](t, Nil0()))
+ }.holds
+
+ def snocAfterAppend[T](l1 : List0[T], l2 : List0[T], t : T) : Boolean = {
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocAfterAppend(xs,l2,t)
+ }) &&
+ ((l1 ++ l2) :+ t == (l1 ++ (l2 :+ t)))
+ }.holds
+
+ def snocReverse[T](l : List0[T], t : T) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocReverse(xs,t)
+ }) &&
+ ((l :+ t).reverse == Cons0(t, l.reverse))
+ }.holds
+
+ def reverseReverse[T](l : List0[T]) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => reverseReverse[T](xs) && snocReverse[T](xs.reverse, x)
+ }) &&
+ (l.reverse.reverse == l)
+ }.holds
+
+ //// my hand calculation shows this should work, but it does not seem to be found
+ //def reverseAppend[T](l1 : List0[T], l2 : List0[T]) : Boolean = {
+ // (l1 match {
+ // case Nil0() => true
+ // case Cons0(x,xs) => {
+ // reverseAppend(xs,l2) &&
+ // snocAfterAppend[T](l2.reverse, xs.reverse, x) &&
+ // l1.reverse == (xs.reverse :+ x)
+ // }
+ // }) &&
+ // ((l1 ++ l2).reverse == (l2.reverse ++ l1.reverse))
+ //}.holds
+}
diff --git a/testcases/repair/List/List5.scala b/testcases/repair/List/List5.scala
new file mode 100644
index 000000000..266f4037f
--- /dev/null
+++ b/testcases/repair/List/List5.scala
@@ -0,0 +1,417 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.custom
+
+import leon._
+import leon.lang._
+import leon.annotation._
+
+sealed abstract class List0[T] {
+ def size: Int = (this match {
+ case Nil0() => 0
+ case Cons0(h, t) => 1 + t.size
+ }) ensuring (_ >= 0)
+
+ def content: Set[T] = this match {
+ case Nil0() => Set()
+ case Cons0(h, t) => Set(h) ++ t.content
+ }
+
+ def contains(v: T): Boolean = (this match {
+ case Cons0(h, t) if h == v => true
+ case Cons0(_, t) => t.contains(v)
+ case Nil0() => false
+ }) ensuring { res => res == (content contains v) }
+
+ def ++(that: List0[T]): List0[T] = (this match {
+ case Nil0() => that
+ case Cons0(x, xs) => Cons0(x, xs ++ that)
+ }) ensuring { res => (res.content == this.content ++ that.content) && (res.size == this.size + that.size)}
+
+ def head: T = {
+ require(this != Nil0[T]())
+ this match {
+ case Cons0(h, t) => h
+ }
+ }
+
+ def tail: List0[T] = {
+ require(this != Nil0[T]())
+ this match {
+ case Cons0(h, t) => t
+ }
+ }
+
+ def apply(index: Int): T = {
+ require(0 <= index && index < size)
+ if (index == 0) {
+ head
+ } else {
+ tail(index-1)
+ }
+ }
+
+ def ::(t:T): List0[T] = Cons0(t, this)
+
+ def :+(t:T): List0[T] = {
+ this match {
+ case Nil0() => Cons0(t, this)
+ case Cons0(x, xs) => Cons0(x, xs :+ (t))
+ }
+ } ensuring(res => (res.size == size + 1) && (res.content == content ++ Set(t)))
+
+ def reverse: List0[T] = {
+ this match {
+ case Nil0() => this
+ case Cons0(x,xs) => xs.reverse :+ x
+ }
+ } ensuring (res => (res.size == size) && (res.content == content))
+
+ def take(i: Int): List0[T] = (this, i) match {
+ case (Nil0(), _) => Nil0()
+ case (Cons0(h, t), i) =>
+ if (i == 0) {
+ Nil0()
+ } else {
+ Cons0(h, t.take(i-1))
+ }
+ }
+
+ def drop(i: Int): List0[T] = (this, i) match {
+ case (Nil0(), _) => Nil0()
+ case (Cons0(h, t), i) =>
+ if (i == 0) {
+ Cons0(h, t)
+ } else {
+ t.drop(i-1)
+ }
+ }
+
+ def slice(from: Int, to: Int): List0[T] = {
+ require(from < to && to < size && from >= 0)
+ drop(from).take(to-from)
+ }
+
+ def replace(from: T, to: T): List0[T] = { this match {
+ case Nil0() => Nil0()
+ case Cons0(h, t) =>
+ val r = t.replace(from, to)
+ Cons0(to, r) // FIXME
+ }} ensuring { res => (res.content == this.content -- Set(from) ++ Set(to)) && res.size == this.size
+ }
+
+ private def chunk0(s: Int, l: List0[T], acc: List0[T], res: List0[List0[T]], s0: Int): List0[List0[T]] = l match {
+ case Nil0() =>
+ if (acc.size > 0) {
+ res :+ acc
+ } else {
+ res
+ }
+ case Cons0(h, t) =>
+ if (s0 == 0) {
+ chunk0(s, l, Nil0(), res :+ acc, s)
+ } else {
+ chunk0(s, t, acc :+ h, res, s0-1)
+ }
+ }
+
+ def chunks(s: Int): List0[List0[T]] = {
+ require(s > 0)
+
+ chunk0(s, this, Nil0(), Nil0(), s)
+ }
+
+ def zip[B](that: List0[B]): List0[(T, B)] = (this, that) match {
+ case (Cons0(h1, t1), Cons0(h2, t2)) =>
+ Cons0((h1, h2), t1.zip(t2))
+ case (_) =>
+ Nil0()
+ }
+
+ def -(e: T): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (e == h) {
+ t - e
+ } else {
+ Cons0(h, t - e)
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def --(that: List0[T]): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (that.contains(h)) {
+ t -- that
+ } else {
+ Cons0(h, t -- that)
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def &(that: List0[T]): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (that.contains(h)) {
+ Cons0(h, t & that)
+ } else {
+ t & that
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def pad(s: Int, e: T): List0[T] = { (this, s) match {
+ case (_, s) if s <= 0 =>
+ this
+ case (Nil0(), s) =>
+ Cons0(e, Nil0().pad(s-1, e))
+ case (Cons0(h, t), s) =>
+ Cons0(h, t.pad(s, e))
+ }} ensuring { res =>
+ ((this,s,e), res) passes {
+ case (Cons0(a,Nil0()), 2, x) => Cons0(a, Cons0(x, Cons0(x, Nil0())))
+ }
+ }
+
+ def find(e: T): Option[Int] = this match {
+ case Nil0() => None()
+ case Cons0(h, t) =>
+ if (h == e) {
+ Some(0)
+ } else {
+ t.find(e) match {
+ case None() => None()
+ case Some(i) => Some(i+1)
+ }
+ }
+ }
+
+ def init: List0[T] = (this match {
+ case Cons0(h, Nil0()) =>
+ Nil0[T]()
+ case Cons0(h, t) =>
+ Cons0[T](h, t.init)
+ case Nil0() =>
+ Nil0[T]()
+ }) ensuring ( (r: List0[T]) => ((r.size < this.size) || (this.size == 0)) )
+
+ def lastOption: Option[T] = this match {
+ case Cons0(h, t) =>
+ t.lastOption.orElse(Some(h))
+ case Nil0() =>
+ None()
+ }
+
+ def firstOption: Option[T] = this match {
+ case Cons0(h, t) =>
+ Some(h)
+ case Nil0() =>
+ None()
+ }
+
+ def unique: List0[T] = this match {
+ case Nil0() => Nil0()
+ case Cons0(h, t) =>
+ Cons0(h, t.unique - h)
+ }
+
+ def splitAt(e: T): List0[List0[T]] = split(Cons0(e, Nil0()))
+
+ def split(seps: List0[T]): List0[List0[T]] = this match {
+ case Cons0(h, t) =>
+ if (seps.contains(h)) {
+ Cons0(Nil0(), t.split(seps))
+ } else {
+ val r = t.split(seps)
+ Cons0(Cons0(h, r.head), r.tail)
+ }
+ case Nil0() =>
+ Cons0(Nil0(), Nil0())
+ }
+
+ def count(e: T): Int = this match {
+ case Cons0(h, t) =>
+ if (h == e) {
+ 1 + t.count(e)
+ } else {
+ t.count(e)
+ }
+ case Nil0() =>
+ 0
+ }
+
+ def evenSplit: (List0[T], List0[T]) = {
+ val c = size/2
+ (take(c), drop(c))
+ }
+
+ def insertAt(pos: Int, l: List0[T]): List0[T] = {
+ if(pos < 0) {
+ insertAt(size + pos, l)
+ } else if(pos == 0) {
+ l ++ this
+ } else {
+ this match {
+ case Cons0(h, t) =>
+ Cons0(h, t.insertAt(pos-1, l))
+ case Nil0() =>
+ l
+ }
+ }
+ }
+
+ def replaceAt(pos: Int, l: List0[T]): List0[T] = {
+ if(pos < 0) {
+ replaceAt(size + pos, l)
+ } else if(pos == 0) {
+ l ++ this.drop(l.size)
+ } else {
+ this match {
+ case Cons0(h, t) =>
+ Cons0(h, t.replaceAt(pos-1, l))
+ case Nil0() =>
+ l
+ }
+ }
+ }
+
+ def rotate(s: Int): List0[T] = {
+ if (s < 0) {
+ rotate(size+s)
+ } else {
+ val s2 = s % size
+ drop(s2) ++ take(s2)
+ }
+ }
+
+ def isEmpty = this match {
+ case Nil0() => true
+ case _ => false
+ }
+
+}
+
+@ignore
+object List0 {
+ def apply[T](elems: T*): List0[T] = ???
+}
+
+@library
+object List0Ops {
+ def flatten[T](ls: List0[List0[T]]): List0[T] = ls match {
+ case Cons0(h, t) => h ++ flatten(t)
+ case Nil0() => Nil0()
+ }
+
+ def isSorted(ls: List0[Int]): Boolean = ls match {
+ case Nil0() => true
+ case Cons0(_, Nil0()) => true
+ case Cons0(h1, Cons0(h2, _)) if(h1 > h2) => false
+ case Cons0(_, t) => isSorted(t)
+ }
+
+ def sorted(ls: List0[Int]): List0[Int] = ls match {
+ case Cons0(h, t) => insSort(sorted(t), h)
+ case Nil0() => Nil0()
+ }
+
+ def insSort(ls: List0[Int], v: Int): List0[Int] = ls match {
+ case Nil0() => Cons0(v, Nil0())
+ case Cons0(h, t) =>
+ if (v <= h) {
+ Cons0(v, t)
+ } else {
+ Cons0(h, insSort(t, v))
+ }
+ }
+}
+
+
+case class Cons0[T](h: T, t: List0[T]) extends List0[T]
+case class Nil0[T]() extends List0[T]
+
+@library
+object List0Specs {
+ def snocIndex[T](l : List0[T], t : T, i : Int) : Boolean = {
+ require(0 <= i && i < l.size + 1)
+ // proof:
+ (l match {
+ case Nil0() => true
+ case Cons0(x, xs) => if (i > 0) snocIndex[T](xs, t, i-1) else true
+ }) &&
+ // claim:
+ ((l :+ t).apply(i) == (if (i < l.size) l(i) else t))
+ }.holds
+
+ def reverseIndex[T](l : List0[T], i : Int) : Boolean = {
+ require(0 <= i && i < l.size)
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocIndex(l, x, i) && reverseIndex[T](l,i)
+ }) &&
+ (l.reverse.apply(i) == l.apply(l.size - 1 - i))
+ }.holds
+
+ def appendIndex[T](l1 : List0[T], l2 : List0[T], i : Int) : Boolean = {
+ require(0 <= i && i < l1.size + l2.size)
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => if (i==0) true else appendIndex[T](xs,l2,i-1)
+ }) &&
+ ((l1 ++ l2).apply(i) == (if (i < l1.size) l1(i) else l2(i - l1.size)))
+ }.holds
+
+ def appendAssoc[T](l1 : List0[T], l2 : List0[T], l3 : List0[T]) : Boolean = {
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => appendAssoc(xs,l2,l3)
+ }) &&
+ (((l1 ++ l2) ++ l3) == (l1 ++ (l2 ++ l3)))
+ }.holds
+
+ def snocIsAppend[T](l : List0[T], t : T) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocIsAppend(xs,t)
+ }) &&
+ ((l :+ t) == l ++ Cons0[T](t, Nil0()))
+ }.holds
+
+ def snocAfterAppend[T](l1 : List0[T], l2 : List0[T], t : T) : Boolean = {
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocAfterAppend(xs,l2,t)
+ }) &&
+ ((l1 ++ l2) :+ t == (l1 ++ (l2 :+ t)))
+ }.holds
+
+ def snocReverse[T](l : List0[T], t : T) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocReverse(xs,t)
+ }) &&
+ ((l :+ t).reverse == Cons0(t, l.reverse))
+ }.holds
+
+ def reverseReverse[T](l : List0[T]) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => reverseReverse[T](xs) && snocReverse[T](xs.reverse, x)
+ }) &&
+ (l.reverse.reverse == l)
+ }.holds
+
+ //// my hand calculation shows this should work, but it does not seem to be found
+ //def reverseAppend[T](l1 : List0[T], l2 : List0[T]) : Boolean = {
+ // (l1 match {
+ // case Nil0() => true
+ // case Cons0(x,xs) => {
+ // reverseAppend(xs,l2) &&
+ // snocAfterAppend[T](l2.reverse, xs.reverse, x) &&
+ // l1.reverse == (xs.reverse :+ x)
+ // }
+ // }) &&
+ // ((l1 ++ l2).reverse == (l2.reverse ++ l1.reverse))
+ //}.holds
+}
diff --git a/testcases/repair/List/List6.scala b/testcases/repair/List/List6.scala
new file mode 100644
index 000000000..028f94109
--- /dev/null
+++ b/testcases/repair/List/List6.scala
@@ -0,0 +1,423 @@
+/* Copyright 2009-2014 EPFL, Lausanne */
+
+package leon.custom
+
+import leon._
+import leon.lang._
+import leon.annotation._
+
+sealed abstract class List0[T] {
+ def size: Int = (this match {
+ case Nil0() => 0
+ case Cons0(h, t) => 1 + t.size
+ }) ensuring (_ >= 0)
+
+ def content: Set[T] = this match {
+ case Nil0() => Set()
+ case Cons0(h, t) => Set(h) ++ t.content
+ }
+
+ def contains(v: T): Boolean = (this match {
+ case Cons0(h, t) if h == v => true
+ case Cons0(_, t) => t.contains(v)
+ case Nil0() => false
+ }) ensuring { res => res == (content contains v) }
+
+ def ++(that: List0[T]): List0[T] = (this match {
+ case Nil0() => that
+ case Cons0(x, xs) => Cons0(x, xs ++ that)
+ }) ensuring { res => (res.content == this.content ++ that.content) && (res.size == this.size + that.size)}
+
+ def head: T = {
+ require(this != Nil0[T]())
+ this match {
+ case Cons0(h, t) => h
+ }
+ }
+
+ def tail: List0[T] = {
+ require(this != Nil0[T]())
+ this match {
+ case Cons0(h, t) => t
+ }
+ }
+
+ def apply(index: Int): T = {
+ require(0 <= index && index < size)
+ if (index == 0) {
+ head
+ } else {
+ tail(index-1)
+ }
+ }
+
+ def ::(t:T): List0[T] = Cons0(t, this)
+
+ def :+(t:T): List0[T] = {
+ this match {
+ case Nil0() => Cons0(t, this)
+ case Cons0(x, xs) => Cons0(x, xs :+ (t))
+ }
+ } ensuring(res => (res.size == size + 1) && (res.content == content ++ Set(t)))
+
+ def reverse: List0[T] = {
+ this match {
+ case Nil0() => this
+ case Cons0(x,xs) => xs.reverse :+ x
+ }
+ } ensuring (res => (res.size == size) && (res.content == content))
+
+ def take(i: Int): List0[T] = (this, i) match {
+ case (Nil0(), _) => Nil0()
+ case (Cons0(h, t), i) =>
+ if (i == 0) {
+ Nil0()
+ } else {
+ Cons0(h, t.take(i-1))
+ }
+ }
+
+ def drop(i: Int): List0[T] = (this, i) match {
+ case (Nil0(), _) => Nil0()
+ case (Cons0(h, t), i) =>
+ if (i == 0) {
+ Cons0(h, t)
+ } else {
+ t.drop(i-1)
+ }
+ }
+
+ def slice(from: Int, to: Int): List0[T] = {
+ require(from < to && to < size && from >= 0)
+ drop(from).take(to-from)
+ }
+
+ def replace(from: T, to: T): List0[T] = this match {
+ case Nil0() => Nil0()
+ case Cons0(h, t) =>
+ val r = t.replace(from, to)
+ if (h == from) {
+ Cons0(to, r)
+ } else {
+ Cons0(h, r)
+ }
+ }
+
+ private def chunk0(s: Int, l: List0[T], acc: List0[T], res: List0[List0[T]], s0: Int): List0[List0[T]] = l match {
+ case Nil0() =>
+ if (acc.size > 0) {
+ res :+ acc
+ } else {
+ res
+ }
+ case Cons0(h, t) =>
+ if (s0 == 0) {
+ chunk0(s, l, Nil0(), res :+ acc, s)
+ } else {
+ chunk0(s, t, acc :+ h, res, s0-1)
+ }
+ }
+
+ def chunks(s: Int): List0[List0[T]] = {
+ require(s > 0)
+
+ chunk0(s, this, Nil0(), Nil0(), s)
+ }
+
+ def zip[B](that: List0[B]): List0[(T, B)] = (this, that) match {
+ case (Cons0(h1, t1), Cons0(h2, t2)) =>
+ Cons0((h1, h2), t1.zip(t2))
+ case (_) =>
+ Nil0()
+ }
+
+ def -(e: T): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (e == h) {
+ t - e
+ } else {
+ Cons0(h, t - e)
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def --(that: List0[T]): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (that.contains(h)) {
+ t -- that
+ } else {
+ Cons0(h, t -- that)
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def &(that: List0[T]): List0[T] = this match {
+ case Cons0(h, t) =>
+ if (that.contains(h)) {
+ Cons0(h, t & that)
+ } else {
+ t & that
+ }
+ case Nil0() =>
+ Nil0()
+ }
+
+ def pad(s: Int, e: T): List0[T] = { (this, s) match {
+ case (_, s) if s <= 0 =>
+ this
+ case (Nil0(), s) =>
+ Cons0(e, Nil0().pad(s-1, e))
+ case (Cons0(h, t), s) =>
+ Cons0(h, t.pad(s, e))
+ }} ensuring { res =>
+ ((this,s,e), res) passes {
+ case (Cons0(a,Nil0()), 2, x) => Cons0(a, Cons0(x, Cons0(x, Nil0())))
+ }
+ }
+
+ def find(e: T): Option[Int] = this match {
+ case Nil0() => None()
+ case Cons0(h, t) =>
+ if (h == e) {
+ Some(0)
+ } else {
+ t.find(e) match {
+ case None() => None()
+ case Some(i) => Some(i+1)
+ }
+ }
+ }
+
+ def init: List0[T] = (this match {
+ case Cons0(h, Nil0()) =>
+ Nil0[T]()
+ case Cons0(h, t) =>
+ Cons0[T](h, t.init)
+ case Nil0() =>
+ Nil0[T]()
+ }) ensuring ( (r: List0[T]) => ((r.size < this.size) || (this.size == 0)) )
+
+ def lastOption: Option[T] = this match {
+ case Cons0(h, t) =>
+ t.lastOption.orElse(Some(h))
+ case Nil0() =>
+ None()
+ }
+
+ def firstOption: Option[T] = this match {
+ case Cons0(h, t) =>
+ Some(h)
+ case Nil0() =>
+ None()
+ }
+
+ def unique: List0[T] = this match {
+ case Nil0() => Nil0()
+ case Cons0(h, t) =>
+ Cons0(h, t.unique - h)
+ }
+
+ def splitAt(e: T): List0[List0[T]] = split(Cons0(e, Nil0()))
+
+ def split(seps: List0[T]): List0[List0[T]] = this match {
+ case Cons0(h, t) =>
+ if (seps.contains(h)) {
+ Cons0(Nil0(), t.split(seps))
+ } else {
+ val r = t.split(seps)
+ Cons0(Cons0(h, r.head), r.tail)
+ }
+ case Nil0() =>
+ Cons0(Nil0(), Nil0())
+ }
+
+ def count(e: T): Int = { this match {
+ case Cons0(h, t) =>
+ if (h == e) {
+ t.count(e) // FIXME +1
+ } else {
+ t.count(e)
+ }
+ case Nil0() =>
+ 0
+ }} ensuring {((this, e), _) passes {
+ case (Cons0(a, Cons0(b, Cons0(a1, Cons0(b2, Nil0())))), a2) if a == a1 && a == a2 && b != a2 && b2 != a2 => 2
+ case (Cons0(a, Cons0(b, Nil0())), c) if a != c && b != c => 0
+ }}
+
+ def evenSplit: (List0[T], List0[T]) = {
+ val c = size/2
+ (take(c), drop(c))
+ }
+
+ def insertAt(pos: Int, l: List0[T]): List0[T] = {
+ if(pos < 0) {
+ insertAt(size + pos, l)
+ } else if(pos == 0) {
+ l ++ this
+ } else {
+ this match {
+ case Cons0(h, t) =>
+ Cons0(h, t.insertAt(pos-1, l))
+ case Nil0() =>
+ l
+ }
+ }
+ }
+
+ def replaceAt(pos: Int, l: List0[T]): List0[T] = {
+ if(pos < 0) {
+ replaceAt(size + pos, l)
+ } else if(pos == 0) {
+ l ++ this.drop(l.size)
+ } else {
+ this match {
+ case Cons0(h, t) =>
+ Cons0(h, t.replaceAt(pos-1, l))
+ case Nil0() =>
+ l
+ }
+ }
+ }
+
+ def rotate(s: Int): List0[T] = {
+ if (s < 0) {
+ rotate(size+s)
+ } else {
+ val s2 = s % size
+ drop(s2) ++ take(s2)
+ }
+ }
+
+ def isEmpty = this match {
+ case Nil0() => true
+ case _ => false
+ }
+
+}
+
+@ignore
+object List0 {
+ def apply[T](elems: T*): List0[T] = ???
+}
+
+@library
+object List0Ops {
+ def flatten[T](ls: List0[List0[T]]): List0[T] = ls match {
+ case Cons0(h, t) => h ++ flatten(t)
+ case Nil0() => Nil0()
+ }
+
+ def isSorted(ls: List0[Int]): Boolean = ls match {
+ case Nil0() => true
+ case Cons0(_, Nil0()) => true
+ case Cons0(h1, Cons0(h2, _)) if(h1 > h2) => false
+ case Cons0(_, t) => isSorted(t)
+ }
+
+ def sorted(ls: List0[Int]): List0[Int] = ls match {
+ case Cons0(h, t) => insSort(sorted(t), h)
+ case Nil0() => Nil0()
+ }
+
+ def insSort(ls: List0[Int], v: Int): List0[Int] = ls match {
+ case Nil0() => Cons0(v, Nil0())
+ case Cons0(h, t) =>
+ if (v <= h) {
+ Cons0(v, t)
+ } else {
+ Cons0(h, insSort(t, v))
+ }
+ }
+}
+
+
+case class Cons0[T](h: T, t: List0[T]) extends List0[T]
+case class Nil0[T]() extends List0[T]
+
+@library
+object List0Specs {
+ def snocIndex[T](l : List0[T], t : T, i : Int) : Boolean = {
+ require(0 <= i && i < l.size + 1)
+ // proof:
+ (l match {
+ case Nil0() => true
+ case Cons0(x, xs) => if (i > 0) snocIndex[T](xs, t, i-1) else true
+ }) &&
+ // claim:
+ ((l :+ t).apply(i) == (if (i < l.size) l(i) else t))
+ }.holds
+
+ def reverseIndex[T](l : List0[T], i : Int) : Boolean = {
+ require(0 <= i && i < l.size)
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocIndex(l, x, i) && reverseIndex[T](l,i)
+ }) &&
+ (l.reverse.apply(i) == l.apply(l.size - 1 - i))
+ }.holds
+
+ def appendIndex[T](l1 : List0[T], l2 : List0[T], i : Int) : Boolean = {
+ require(0 <= i && i < l1.size + l2.size)
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => if (i==0) true else appendIndex[T](xs,l2,i-1)
+ }) &&
+ ((l1 ++ l2).apply(i) == (if (i < l1.size) l1(i) else l2(i - l1.size)))
+ }.holds
+
+ def appendAssoc[T](l1 : List0[T], l2 : List0[T], l3 : List0[T]) : Boolean = {
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => appendAssoc(xs,l2,l3)
+ }) &&
+ (((l1 ++ l2) ++ l3) == (l1 ++ (l2 ++ l3)))
+ }.holds
+
+ def snocIsAppend[T](l : List0[T], t : T) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocIsAppend(xs,t)
+ }) &&
+ ((l :+ t) == l ++ Cons0[T](t, Nil0()))
+ }.holds
+
+ def snocAfterAppend[T](l1 : List0[T], l2 : List0[T], t : T) : Boolean = {
+ (l1 match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocAfterAppend(xs,l2,t)
+ }) &&
+ ((l1 ++ l2) :+ t == (l1 ++ (l2 :+ t)))
+ }.holds
+
+ def snocReverse[T](l : List0[T], t : T) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => snocReverse(xs,t)
+ }) &&
+ ((l :+ t).reverse == Cons0(t, l.reverse))
+ }.holds
+
+ def reverseReverse[T](l : List0[T]) : Boolean = {
+ (l match {
+ case Nil0() => true
+ case Cons0(x,xs) => reverseReverse[T](xs) && snocReverse[T](xs.reverse, x)
+ }) &&
+ (l.reverse.reverse == l)
+ }.holds
+
+ //// my hand calculation shows this should work, but it does not seem to be found
+ //def reverseAppend[T](l1 : List0[T], l2 : List0[T]) : Boolean = {
+ // (l1 match {
+ // case Nil0() => true
+ // case Cons0(x,xs) => {
+ // reverseAppend(xs,l2) &&
+ // snocAfterAppend[T](l2.reverse, xs.reverse, x) &&
+ // l1.reverse == (xs.reverse :+ x)
+ // }
+ // }) &&
+ // ((l1 ++ l2).reverse == (l2.reverse ++ l1.reverse))
+ //}.holds
+}
diff --git a/testcases/repair/List/Size.scala b/testcases/repair/List/Size.scala
deleted file mode 100644
index 8e36fc6ab..000000000
--- a/testcases/repair/List/Size.scala
+++ /dev/null
@@ -1,19 +0,0 @@
-import leon._
-import leon.lang._
-import leon.collection._
-import leon.lang.synthesis._
-
-object List {
- def size(l: List[Int]): Int = (l match {
- case Nil() => 1
- case Cons(h, t) => 1 + size(t)
- }) ensuring {
- (res: Int) =>
- ((l, res) passes {
- case Cons(a, Nil()) => 1
- case Cons(a, Cons(b, Nil())) => 2
- case Cons(a, Cons(b, Cons(c, Nil()))) => 3
- case Nil() => 0
- })
- }
-}
diff --git a/testcases/repair/List/Size1.scala b/testcases/repair/List/Size1.scala
deleted file mode 100644
index e6aa4e37d..000000000
--- a/testcases/repair/List/Size1.scala
+++ /dev/null
@@ -1,17 +0,0 @@
-import leon._
-import leon.lang._
-import leon.collection._
-import leon.lang.synthesis._
-
-object List {
- def size(l: List[Int]): Int = (l match {
- case Cons(h, t) => 3 + size(t) // FIXME: 1 + ...
- }) ensuring {
- (res: Int) =>
- ((l, res) passes {
- case Cons(a, Nil()) => 1
- case Nil() => 0
- })
- }
-
-}
diff --git a/testcases/repair/List/Sum.scala b/testcases/repair/List/Sum.scala
deleted file mode 100644
index df8ea2e25..000000000
--- a/testcases/repair/List/Sum.scala
+++ /dev/null
@@ -1,19 +0,0 @@
-import leon._
-import leon.lang._
-import leon.collection._
-import leon.lang.synthesis._
-
-object List {
- def sum(l: List[Int]): Int = (l match {
- case Nil() => 0
- case Cons(h, t) => h + sum(t)
- }) ensuring {
- (res: Int) =>
- ((l, res) passes {
- case Cons(a, Nil()) => a
- case Cons(a, Cons(b, Nil())) => a+b
- case Cons(a, Cons(b, Cons(c, Nil()))) => a+b+c
- case Nil() => 0
- })
- }
-}
diff --git a/testcases/repair/List/Sum1.scala b/testcases/repair/List/Sum1.scala
deleted file mode 100644
index b809f5c71..000000000
--- a/testcases/repair/List/Sum1.scala
+++ /dev/null
@@ -1,19 +0,0 @@
-import leon._
-import leon.lang._
-import leon.collection._
-import leon.lang.synthesis._
-
-object List {
- def sum(l: List[Int]): Int = (l match {
- case Nil() => 0
- case Cons(h, t) => 1 + sum(t) // FIXME: 1 instead of h
- }) ensuring {
- (res: Int) =>
- ((l, res) passes {
- case Cons(a, Nil()) => a
- case Cons(a, Cons(b, Nil())) => a+b
- case Cons(a, Cons(b, Cons(c, Nil()))) => a+b+c
- case Nil() => 0
- })
- }
-}
diff --git a/testcases/repair/RedBlackTree-old/RedBlackTree.scala b/testcases/repair/RedBlackTree-old/RedBlackTree.scala
new file mode 100644
index 000000000..8f88abf28
--- /dev/null
+++ b/testcases/repair/RedBlackTree-old/RedBlackTree.scala
@@ -0,0 +1,101 @@
+import leon._
+import lang._
+import annotation._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case object Red extends Color
+ case object Black extends Color
+
+ sealed abstract class Tree
+ case object Empty extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ 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) : Int = t match {
+ case Empty => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* 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) : Int = t match {
+ case Empty => 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 balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+
+ (c,a,x,b) match {
+ case (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 (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 (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 (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 (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/repair/RedBlackTree-old/RedBlackTree1.scala b/testcases/repair/RedBlackTree-old/RedBlackTree1.scala
new file mode 100644
index 000000000..93d5b61e9
--- /dev/null
+++ b/testcases/repair/RedBlackTree-old/RedBlackTree1.scala
@@ -0,0 +1,143 @@
+import leon._
+import lang._
+import annotation._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case object Red extends Color
+ case object Black extends Color
+
+ sealed abstract class Tree
+ case object Empty extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ 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) : Int = t match {
+ case Empty => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* 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) : Int = t match {
+ case Empty => 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))
+// // makeBlack(ins(x, 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 = {
+ // require(
+ // Node(c,a,x,b) match {
+ // case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case t => redDescHaveBlackChildren(t)
+ // }
+ // )
+ 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,xV,d)) // FIXME: xV instead of zV in right node
+ 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,xV,d)) // FIXME: xV instead of zV in right node
+ 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))
+ // }
+ // } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+
+}
diff --git a/testcases/repair/RedBlackTree-old/RedBlackTree2.scala b/testcases/repair/RedBlackTree-old/RedBlackTree2.scala
new file mode 100644
index 000000000..d4675cadb
--- /dev/null
+++ b/testcases/repair/RedBlackTree-old/RedBlackTree2.scala
@@ -0,0 +1,143 @@
+import leon._
+import lang._
+import annotation._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case object Red extends Color
+ case object Black extends Color
+
+ sealed abstract class Tree
+ case object Empty extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ 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) : Int = t match {
+ case Empty => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* 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) : Int = t match {
+ case Empty => 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) Node(c, ins(x, a), y, b) // FIXME : forgot to balance
+ 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))
+// // makeBlack(ins(x, 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 = {
+ // require(
+ // Node(c,a,x,b) match {
+ // case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case t => redDescHaveBlackChildren(t)
+ // }
+ // )
+ 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))
+ // }
+ // } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+
+}
diff --git a/testcases/repair/RedBlackTree-old/RedBlackTree3.scala b/testcases/repair/RedBlackTree-old/RedBlackTree3.scala
new file mode 100644
index 000000000..4d8e1f39d
--- /dev/null
+++ b/testcases/repair/RedBlackTree-old/RedBlackTree3.scala
@@ -0,0 +1,143 @@
+import leon._
+import lang._
+import annotation._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case object Red extends Color
+ case object Black extends Color
+
+ sealed abstract class Tree
+ case object Empty extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ 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) : Int = t match {
+ case Empty => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* 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) : Int = t match {
+ case Empty => 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))
+// // makeBlack(ins(x, 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 = {
+ // require(
+ // Node(c,a,x,b) match {
+ // case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case t => redDescHaveBlackChildren(t)
+ // }
+ // )
+ 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,xV,d)) // FIXME: xV instead of zV in right node
+ 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))
+ // }
+ // } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+
+}
diff --git a/testcases/repair/RedBlackTree/RedBlackTree4.scala b/testcases/repair/RedBlackTree-old/RedBlackTree4.scala
similarity index 100%
rename from testcases/repair/RedBlackTree/RedBlackTree4.scala
rename to testcases/repair/RedBlackTree-old/RedBlackTree4.scala
diff --git a/testcases/repair/RedBlackTree/RedBlackTree5.scala b/testcases/repair/RedBlackTree-old/RedBlackTree5.scala
similarity index 100%
rename from testcases/repair/RedBlackTree/RedBlackTree5.scala
rename to testcases/repair/RedBlackTree-old/RedBlackTree5.scala
diff --git a/testcases/repair/RedBlackTree-old/RedBlackTree6.scala b/testcases/repair/RedBlackTree-old/RedBlackTree6.scala
new file mode 100644
index 000000000..36cfb692b
--- /dev/null
+++ b/testcases/repair/RedBlackTree-old/RedBlackTree6.scala
@@ -0,0 +1,142 @@
+import leon._
+import lang._
+import annotation._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case object Red extends Color
+ case object Black extends Color
+
+ sealed abstract class Tree
+ case object Empty extends Tree
+ case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+
+ 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) : Int = t match {
+ case Empty => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* 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) : Int = t match {
+ case Empty => 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 add(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
+ ins(x, t) // FIXME: makeBlack(ins(x, t))
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res) )
+
+ def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
+ // require(
+ // Node(c,a,x,b) match {
+ // case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) =>
+ // redNodesHaveBlackChildren(a) &&
+ // redNodesHaveBlackChildren(b) &&
+ // redNodesHaveBlackChildren(c) &&
+ // redNodesHaveBlackChildren(d)
+ // case t => redDescHaveBlackChildren(t)
+ // }
+ // )
+ 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))
+ // }
+ // } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+
+}
diff --git a/testcases/repair/RedBlackTree/RedBlackTree7.scala b/testcases/repair/RedBlackTree-old/RedBlackTree7.scala
similarity index 100%
rename from testcases/repair/RedBlackTree/RedBlackTree7.scala
rename to testcases/repair/RedBlackTree-old/RedBlackTree7.scala
diff --git a/testcases/repair/RedBlackTree/RedBlackTree.scala b/testcases/repair/RedBlackTree/RedBlackTree.scala
index 8f88abf28..d80fafc08 100644
--- a/testcases/repair/RedBlackTree/RedBlackTree.scala
+++ b/testcases/repair/RedBlackTree/RedBlackTree.scala
@@ -1,4 +1,4 @@
-import leon._
+import leon._
import lang._
import annotation._
@@ -7,31 +7,67 @@ object RedBlackTree {
case object Red extends Color
case object Black extends Color
- sealed abstract class Tree
- case object Empty extends Tree
- case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+ sealed abstract class Tree {
+ /* We consider leaves to be black by definition */
+ def color = this match {
+ case Empty => Black
+ case Node(c,_,_,_) => c
+ }
- def content(t: Tree) : Set[Int] = t match {
- case Empty => Set.empty
- case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
- }
+ def content : Set[Int] = this match {
+ case Empty => Set.empty
+ case Node(_, l, v, r) => l.content ++ Set(v) ++ r.content
+ }
- def size(t: Tree) : Int = t match {
- case Empty => 0
- case Node(_, l, v, r) => size(l) + 1 + size(r)
- }
+ def size : Int = this match {
+ case Empty => 0
+ case Node(_, l, v, r) => l.size + 1 + r.size
+ }
- /* 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 isBlack = color == Black
+
+ def blackHeight : Int = this match {
+ case Empty => 1
+ case Node(Black, l, _, _) => l.blackHeight + 1
+ case Node(Red, l, _, _) => l.blackHeight
+ }
+
+ def max : Option[Int] = this match {
+ case Empty => None()
+ case Node(_, l, v, r) =>
+ maxOption(Some(v), maxOption(l.max, r.max))
+ }
+
+ def min : Option[Int] = this match {
+ case Empty => None()
+ case Node(_, l, v, r) =>
+ minOption(Some(v), minOption(l.max, r.max))
+ }
+
+ }
+
+ def minOption(i1 : Option[Int], i2 : Option[Int]) : Option[Int] = (i1, i2) match {
+ case (Some(i1), Some(i2)) => Some(if (i1 < i2) i1 else i2)
+ case _ => i1 orElse i2
+ }
+
+ def maxOption(i1 : Option[Int], i2 : Option[Int]) : Option[Int] = (i1, i2) match {
+ case (Some(i1), Some(i2)) => Some(if (i1 > i2) i1 else i2)
+ case _ => i1 orElse i2
}
+ case object Empty extends Tree
+ case class Node(color_ : Color, left: Tree, value: Int, right: Tree) extends Tree
+
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)
+ case Node(Black, l, _, r) =>
+ redNodesHaveBlackChildren(l) &&
+ redNodesHaveBlackChildren(r)
+ case Node(Red, l, _, r) =>
+ l.isBlack && r.isBlack &&
+ redNodesHaveBlackChildren(l) &&
+ redNodesHaveBlackChildren(r)
}
def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
@@ -40,62 +76,84 @@ object RedBlackTree {
}
def blackBalanced(t : Tree) : Boolean = t match {
- case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && l.blackHeight == r.blackHeight
case Empty => true
}
-
- def blackHeight(t : Tree) : Int = t match {
- case Empty => 1
- case Node(Black, l, _, _) => blackHeight(l) + 1
- case Node(Red, l, _, _) => blackHeight(l)
+
+ def keysSorted(t : Tree) : Boolean = t match {
+ case Empty => true
+ case Node(_, l, v, r) =>
+ keysSorted(l) && keysSorted(r) &&
+ (l.max.getOrElse (v-1) < v) &&
+ (r.min.getOrElse (v+1) > v)
}
-
-
+
+
// <<insert element x into the tree t>>
def ins(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) && keysSorted(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))
+ case n@Node(c,a,y,b) =>
+ if (x < y) balance(Node(c, ins(x, a), y, b))
+ else if (x == y) n
+ else balance(Node(c, a, y, ins(x, b)))
}
} ensuring (res =>
- content(res) == content(t) ++ Set(x) &&
- size(t) <= size(res) &&
- size(res) <= size(t) + 1 &&
+ res.content == t.content ++ Set(x) &&
+ t.size <= res.size &&
+ res.size <= t.size + 1 &&
+ keysSorted(res) &&
redDescHaveBlackChildren(res) &&
blackBalanced(res)
)
def makeBlack(n: Tree): Tree = {
- require(redDescHaveBlackChildren(n) && blackBalanced(n) )
+ require(
+ redDescHaveBlackChildren(n) &&
+ blackBalanced(n) &&
+ keysSorted(n)
+ )
n match {
case Node(Red,l,v,r) => Node(Black,l,v,r)
case _ => n
}
- } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res) )
+ } ensuring { res =>
+ res.isBlack &&
+ redNodesHaveBlackChildren(res) &&
+ blackBalanced(res) &&
+ keysSorted(res)
+ }
def add(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) && keysSorted(t))
makeBlack(ins(x, t))
- } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res) )
+ } ensuring { res =>
+ res.content == t.content ++ Set(x) &&
+ redNodesHaveBlackChildren(res) &&
+ blackBalanced(res) &&
+ keysSorted(res)
+ }
- def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
-
- (c,a,x,b) match {
- case (Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) =>
+ def balance(t : Tree) : Tree = {
+ require(keysSorted(t))
+ t match {
+ case Empty => Empty
+ 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 (Black,Node(Red,a,xV,Node(Red,b,yV,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 (Black,a,xV,Node(Red,Node(Red,b,yV,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 (Black,a,xV,Node(Red,b,yV,Node(Red,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 (c,a,xV,b) => Node(c,a,xV,b)
+ case other => other
}
- } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
+ } ensuring { res =>
+ res.content == t.content &&
+ keysSorted(res)
+ }
+
}
diff --git a/testcases/repair/RedBlackTree/RedBlackTree1.scala b/testcases/repair/RedBlackTree/RedBlackTree1.scala
index 93d5b61e9..d219c0094 100644
--- a/testcases/repair/RedBlackTree/RedBlackTree1.scala
+++ b/testcases/repair/RedBlackTree/RedBlackTree1.scala
@@ -1,4 +1,4 @@
-import leon._
+import leon._
import lang._
import annotation._
@@ -7,31 +7,67 @@ object RedBlackTree {
case object Red extends Color
case object Black extends Color
- sealed abstract class Tree
- case object Empty extends Tree
- case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+ sealed abstract class Tree {
+ /* We consider leaves to be black by definition */
+ def color = this match {
+ case Empty => Black
+ case Node(c,_,_,_) => c
+ }
- def content(t: Tree) : Set[Int] = t match {
- case Empty => Set.empty
- case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
- }
+ def content : Set[Int] = this match {
+ case Empty => Set.empty
+ case Node(_, l, v, r) => l.content ++ Set(v) ++ r.content
+ }
- def size(t: Tree) : Int = t match {
- case Empty => 0
- case Node(_, l, v, r) => size(l) + 1 + size(r)
- }
+ def size : Int = this match {
+ case Empty => 0
+ case Node(_, l, v, r) => l.size + 1 + r.size
+ }
- /* 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 isBlack = color == Black
+
+ def blackHeight : Int = this match {
+ case Empty => 1
+ case Node(Black, l, _, _) => l.blackHeight + 1
+ case Node(Red, l, _, _) => l.blackHeight
+ }
+
+ def max : Option[Int] = this match {
+ case Empty => None()
+ case Node(_, l, v, r) =>
+ maxOption(Some(v), maxOption(l.max, r.max))
+ }
+
+ def min : Option[Int] = this match {
+ case Empty => None()
+ case Node(_, l, v, r) =>
+ minOption(Some(v), minOption(l.max, r.max))
+ }
+
+ }
+
+ def minOption(i1 : Option[Int], i2 : Option[Int]) : Option[Int] = (i1, i2) match {
+ case (Some(i1), Some(i2)) => Some(if (i1 < i2) i1 else i2)
+ case _ => i1 orElse i2
+ }
+
+ def maxOption(i1 : Option[Int], i2 : Option[Int]) : Option[Int] = (i1, i2) match {
+ case (Some(i1), Some(i2)) => Some(if (i1 > i2) i1 else i2)
+ case _ => i1 orElse i2
}
+ case object Empty extends Tree
+ case class Node(color_ : Color, left: Tree, value: Int, right: Tree) extends Tree
+
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)
+ case Node(Black, l, _, r) =>
+ redNodesHaveBlackChildren(l) &&
+ redNodesHaveBlackChildren(r)
+ case Node(Red, l, _, r) =>
+ l.isBlack && r.isBlack &&
+ redNodesHaveBlackChildren(l) &&
+ redNodesHaveBlackChildren(r)
}
def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
@@ -40,104 +76,74 @@ object RedBlackTree {
}
def blackBalanced(t : Tree) : Boolean = t match {
- case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && l.blackHeight == r.blackHeight
case Empty => true
}
-
- def blackHeight(t : Tree) : Int = t match {
- case Empty => 1
- case Node(Black, l, _, _) => blackHeight(l) + 1
- case Node(Red, l, _, _) => blackHeight(l)
+
+ def keysSorted(t : Tree) : Boolean = t match {
+ case Empty => true
+ case Node(_, l, v, r) =>
+ keysSorted(l) && keysSorted(r) &&
+ (l.max.getOrElse (v-1) < v) &&
+ (r.min.getOrElse (v+1) > v)
}
-
-
+
+
// <<insert element x into the tree t>>
def ins(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t) && blackBalanced(t))
- t match {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) && keysSorted(t))
+ val newT = 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))
+ case n@Node(c,a,y,b) =>
+ if (x < y) Node(c, ins(x, a), y, b)
+ else if (x == y) n
+ else Node(c, a, y, ins(x, b))
+ }
+ newT 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,xV,d)) // FIXME: second xV -> zV
+ 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,xV,d)) // FIXME: same
+ 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 other => other
}
} ensuring (res =>
- content(res) == content(t) ++ Set(x) &&
- size(t) <= size(res) &&
- size(res) <= size(t) + 1 &&
+ res.content == t.content ++ Set(x) &&
+ t.size <= res.size &&
+ res.size <= t.size + 1 &&
+ keysSorted(res) &&
redDescHaveBlackChildren(res) &&
blackBalanced(res)
)
def makeBlack(n: Tree): Tree = {
- require(redDescHaveBlackChildren(n) && blackBalanced(n) )
+ require(
+ redDescHaveBlackChildren(n) &&
+ blackBalanced(n) &&
+ keysSorted(n)
+ )
n match {
case Node(Red,l,v,r) => Node(Black,l,v,r)
case _ => n
}
- } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res) )
+ } ensuring { res =>
+ res.isBlack &&
+ redNodesHaveBlackChildren(res) &&
+ blackBalanced(res) &&
+ keysSorted(res)
+ }
def add(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) && keysSorted(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))
-// // makeBlack(ins(x, t))
-// ins(x, t)
-// } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+ } ensuring { res =>
+ res.content == t.content ++ Set(x) &&
+ redNodesHaveBlackChildren(res) &&
+ blackBalanced(res) &&
+ keysSorted(res)
+ }
- def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
- // require(
- // Node(c,a,x,b) match {
- // case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
- // redNodesHaveBlackChildren(a) &&
- // redNodesHaveBlackChildren(b) &&
- // redNodesHaveBlackChildren(c) &&
- // redNodesHaveBlackChildren(d)
- // case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
- // redNodesHaveBlackChildren(a) &&
- // redNodesHaveBlackChildren(b) &&
- // redNodesHaveBlackChildren(c) &&
- // redNodesHaveBlackChildren(d)
- // case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) =>
- // redNodesHaveBlackChildren(a) &&
- // redNodesHaveBlackChildren(b) &&
- // redNodesHaveBlackChildren(c) &&
- // redNodesHaveBlackChildren(d)
- // case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) =>
- // redNodesHaveBlackChildren(a) &&
- // redNodesHaveBlackChildren(b) &&
- // redNodesHaveBlackChildren(c) &&
- // redNodesHaveBlackChildren(d)
- // case t => redDescHaveBlackChildren(t)
- // }
- // )
- 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,xV,d)) // FIXME: xV instead of zV in right node
- 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,xV,d)) // FIXME: xV instead of zV in right node
- 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))
- // }
- // } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
-
}
diff --git a/testcases/repair/RedBlackTree/RedBlackTree2.scala b/testcases/repair/RedBlackTree/RedBlackTree2.scala
index d4675cadb..7f0c029c8 100644
--- a/testcases/repair/RedBlackTree/RedBlackTree2.scala
+++ b/testcases/repair/RedBlackTree/RedBlackTree2.scala
@@ -1,4 +1,4 @@
-import leon._
+import leon._
import lang._
import annotation._
@@ -7,31 +7,67 @@ object RedBlackTree {
case object Red extends Color
case object Black extends Color
- sealed abstract class Tree
- case object Empty extends Tree
- case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+ sealed abstract class Tree {
+ /* We consider leaves to be black by definition */
+ def color = this match {
+ case Empty => Black
+ case Node(c,_,_,_) => c
+ }
- def content(t: Tree) : Set[Int] = t match {
- case Empty => Set.empty
- case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
- }
+ def content : Set[Int] = this match {
+ case Empty => Set.empty
+ case Node(_, l, v, r) => l.content ++ Set(v) ++ r.content
+ }
- def size(t: Tree) : Int = t match {
- case Empty => 0
- case Node(_, l, v, r) => size(l) + 1 + size(r)
- }
+ def size : Int = this match {
+ case Empty => 0
+ case Node(_, l, v, r) => l.size + 1 + r.size
+ }
- /* 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 isBlack = color == Black
+
+ def blackHeight : Int = this match {
+ case Empty => 1
+ case Node(Black, l, _, _) => l.blackHeight + 1
+ case Node(Red, l, _, _) => l.blackHeight
+ }
+
+ def max : Option[Int] = this match {
+ case Empty => None()
+ case Node(_, l, v, r) =>
+ maxOption(Some(v), maxOption(l.max, r.max))
+ }
+
+ def min : Option[Int] = this match {
+ case Empty => None()
+ case Node(_, l, v, r) =>
+ minOption(Some(v), minOption(l.max, r.max))
+ }
+
+ }
+
+ def minOption(i1 : Option[Int], i2 : Option[Int]) : Option[Int] = (i1, i2) match {
+ case (Some(i1), Some(i2)) => Some(if (i1 < i2) i1 else i2)
+ case _ => i1 orElse i2
+ }
+
+ def maxOption(i1 : Option[Int], i2 : Option[Int]) : Option[Int] = (i1, i2) match {
+ case (Some(i1), Some(i2)) => Some(if (i1 > i2) i1 else i2)
+ case _ => i1 orElse i2
}
+ case object Empty extends Tree
+ case class Node(color_ : Color, left: Tree, value: Int, right: Tree) extends Tree
+
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)
+ case Node(Black, l, _, r) =>
+ redNodesHaveBlackChildren(l) &&
+ redNodesHaveBlackChildren(r)
+ case Node(Red, l, _, r) =>
+ l.isBlack && r.isBlack &&
+ redNodesHaveBlackChildren(l) &&
+ redNodesHaveBlackChildren(r)
}
def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
@@ -40,81 +76,70 @@ object RedBlackTree {
}
def blackBalanced(t : Tree) : Boolean = t match {
- case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && l.blackHeight == r.blackHeight
case Empty => true
}
-
- def blackHeight(t : Tree) : Int = t match {
- case Empty => 1
- case Node(Black, l, _, _) => blackHeight(l) + 1
- case Node(Red, l, _, _) => blackHeight(l)
+
+ def keysSorted(t : Tree) : Boolean = t match {
+ case Empty => true
+ case Node(_, l, v, r) =>
+ keysSorted(l) && keysSorted(r) &&
+ (l.max.getOrElse (v-1) < v) &&
+ (r.min.getOrElse (v+1) > v)
}
-
-
+
+
// <<insert element x into the tree t>>
def ins(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) && keysSorted(t))
t match {
case Empty => Node(Red,Empty,x,Empty)
- case Node(c,a,y,b) =>
- if (x < y) Node(c, ins(x, a), y, b) // FIXME : forgot to balance
- else if (x == y) Node(c,a,y,b)
- else balance(c,a,y,ins(x, b))
+ case n@Node(c,a,y,b) =>
+ if (x < y) Node(c, ins(x, a), y, b) // FIXME forgot to balance
+ else if (x == y) n
+ else balance(Node(c, a, y, ins(x, b)))
}
} ensuring (res =>
- content(res) == content(t) ++ Set(x) &&
- size(t) <= size(res) &&
- size(res) <= size(t) + 1 &&
+ res.content == t.content ++ Set(x) &&
+ t.size <= res.size &&
+ res.size <= t.size + 1 &&
+ keysSorted(res) &&
redDescHaveBlackChildren(res) &&
blackBalanced(res)
)
def makeBlack(n: Tree): Tree = {
- require(redDescHaveBlackChildren(n) && blackBalanced(n) )
+ require(
+ redDescHaveBlackChildren(n) &&
+ blackBalanced(n) &&
+ keysSorted(n)
+ )
n match {
case Node(Red,l,v,r) => Node(Black,l,v,r)
case _ => n
}
- } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res) )
+ } ensuring { res =>
+ res.isBlack &&
+ redNodesHaveBlackChildren(res) &&
+ blackBalanced(res) &&
+ keysSorted(res)
+ }
def add(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) && keysSorted(t))
makeBlack(ins(x, t))
- } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res) )
+ } ensuring { res =>
+ res.content == t.content ++ Set(x) &&
+ redNodesHaveBlackChildren(res) &&
+ blackBalanced(res) &&
+ keysSorted(res)
+ }
-// def buggyAdd(x: Int, t: Tree): Tree = {
-// require(redNodesHaveBlackChildren(t))
-// // makeBlack(ins(x, 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 = {
- // require(
- // Node(c,a,x,b) match {
- // case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
- // redNodesHaveBlackChildren(a) &&
- // redNodesHaveBlackChildren(b) &&
- // redNodesHaveBlackChildren(c) &&
- // redNodesHaveBlackChildren(d)
- // case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
- // redNodesHaveBlackChildren(a) &&
- // redNodesHaveBlackChildren(b) &&
- // redNodesHaveBlackChildren(c) &&
- // redNodesHaveBlackChildren(d)
- // case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) =>
- // redNodesHaveBlackChildren(a) &&
- // redNodesHaveBlackChildren(b) &&
- // redNodesHaveBlackChildren(c) &&
- // redNodesHaveBlackChildren(d)
- // case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) =>
- // redNodesHaveBlackChildren(a) &&
- // redNodesHaveBlackChildren(b) &&
- // redNodesHaveBlackChildren(c) &&
- // redNodesHaveBlackChildren(d)
- // case t => redDescHaveBlackChildren(t)
- // }
- // )
- Node(c,a,x,b) match {
+ def balance(t : Tree) : Tree = {
+ require(keysSorted(t))
+ t match {
+ case Empty => Empty
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) =>
@@ -123,21 +148,12 @@ object RedBlackTree {
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)
+ case other => other
}
- } 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))
- // }
- // } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+ } ensuring { res =>
+ res.content == t.content &&
+ keysSorted(res)
+ }
+
}
diff --git a/testcases/repair/RedBlackTree/RedBlackTree3.scala b/testcases/repair/RedBlackTree/RedBlackTree3.scala
index 4d8e1f39d..a5d561985 100644
--- a/testcases/repair/RedBlackTree/RedBlackTree3.scala
+++ b/testcases/repair/RedBlackTree/RedBlackTree3.scala
@@ -1,4 +1,4 @@
-import leon._
+import leon._
import lang._
import annotation._
@@ -7,31 +7,67 @@ object RedBlackTree {
case object Red extends Color
case object Black extends Color
- sealed abstract class Tree
- case object Empty extends Tree
- case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+ sealed abstract class Tree {
+ /* We consider leaves to be black by definition */
+ def color = this match {
+ case Empty => Black
+ case Node(c,_,_,_) => c
+ }
- def content(t: Tree) : Set[Int] = t match {
- case Empty => Set.empty
- case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
- }
+ def content : Set[Int] = this match {
+ case Empty => Set.empty
+ case Node(_, l, v, r) => l.content ++ Set(v) ++ r.content
+ }
- def size(t: Tree) : Int = t match {
- case Empty => 0
- case Node(_, l, v, r) => size(l) + 1 + size(r)
- }
+ def size : Int = this match {
+ case Empty => 0
+ case Node(_, l, v, r) => l.size + 1 + r.size
+ }
- /* 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 isBlack = color == Black
+
+ def blackHeight : Int = this match {
+ case Empty => 1
+ case Node(Black, l, _, _) => l.blackHeight + 1
+ case Node(Red, l, _, _) => l.blackHeight
+ }
+
+ def max : Option[Int] = this match {
+ case Empty => None()
+ case Node(_, l, v, r) =>
+ maxOption(Some(v), maxOption(l.max, r.max))
+ }
+
+ def min : Option[Int] = this match {
+ case Empty => None()
+ case Node(_, l, v, r) =>
+ minOption(Some(v), minOption(l.max, r.max))
+ }
+
+ }
+
+ def minOption(i1 : Option[Int], i2 : Option[Int]) : Option[Int] = (i1, i2) match {
+ case (Some(i1), Some(i2)) => Some(if (i1 < i2) i1 else i2)
+ case _ => i1 orElse i2
+ }
+
+ def maxOption(i1 : Option[Int], i2 : Option[Int]) : Option[Int] = (i1, i2) match {
+ case (Some(i1), Some(i2)) => Some(if (i1 > i2) i1 else i2)
+ case _ => i1 orElse i2
}
+ case object Empty extends Tree
+ case class Node(color_ : Color, left: Tree, value: Int, right: Tree) extends Tree
+
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)
+ case Node(Black, l, _, r) =>
+ redNodesHaveBlackChildren(l) &&
+ redNodesHaveBlackChildren(r)
+ case Node(Red, l, _, r) =>
+ l.isBlack && r.isBlack &&
+ redNodesHaveBlackChildren(l) &&
+ redNodesHaveBlackChildren(r)
}
def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
@@ -40,104 +76,74 @@ object RedBlackTree {
}
def blackBalanced(t : Tree) : Boolean = t match {
- case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && l.blackHeight == r.blackHeight
case Empty => true
}
-
- def blackHeight(t : Tree) : Int = t match {
- case Empty => 1
- case Node(Black, l, _, _) => blackHeight(l) + 1
- case Node(Red, l, _, _) => blackHeight(l)
+
+ def keysSorted(t : Tree) : Boolean = t match {
+ case Empty => true
+ case Node(_, l, v, r) =>
+ keysSorted(l) && keysSorted(r) &&
+ (l.max.getOrElse (v-1) < v) &&
+ (r.min.getOrElse (v+1) > v)
}
-
-
+
+
// <<insert element x into the tree t>>
def ins(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t) && blackBalanced(t))
- t match {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) && keysSorted(t))
+ val newT = 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))
+ case n@Node(c,a,y,b) =>
+ if (x < y) Node(c, ins(x, a), y, b)
+ else if (x == y) n
+ else Node(c, a, y, ins(x, b))
+ }
+ newT 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,xV,d)) // FIXME: second xV -> zV
+ 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 other => other
}
} ensuring (res =>
- content(res) == content(t) ++ Set(x) &&
- size(t) <= size(res) &&
- size(res) <= size(t) + 1 &&
+ res.content == t.content ++ Set(x) &&
+ t.size <= res.size &&
+ res.size <= t.size + 1 &&
+ keysSorted(res) &&
redDescHaveBlackChildren(res) &&
blackBalanced(res)
)
def makeBlack(n: Tree): Tree = {
- require(redDescHaveBlackChildren(n) && blackBalanced(n) )
+ require(
+ redDescHaveBlackChildren(n) &&
+ blackBalanced(n) &&
+ keysSorted(n)
+ )
n match {
case Node(Red,l,v,r) => Node(Black,l,v,r)
case _ => n
}
- } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res) )
+ } ensuring { res =>
+ res.isBlack &&
+ redNodesHaveBlackChildren(res) &&
+ blackBalanced(res) &&
+ keysSorted(res)
+ }
def add(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) && keysSorted(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))
-// // makeBlack(ins(x, t))
-// ins(x, t)
-// } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+ } ensuring { res =>
+ res.content == t.content ++ Set(x) &&
+ redNodesHaveBlackChildren(res) &&
+ blackBalanced(res) &&
+ keysSorted(res)
+ }
- def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
- // require(
- // Node(c,a,x,b) match {
- // case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
- // redNodesHaveBlackChildren(a) &&
- // redNodesHaveBlackChildren(b) &&
- // redNodesHaveBlackChildren(c) &&
- // redNodesHaveBlackChildren(d)
- // case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
- // redNodesHaveBlackChildren(a) &&
- // redNodesHaveBlackChildren(b) &&
- // redNodesHaveBlackChildren(c) &&
- // redNodesHaveBlackChildren(d)
- // case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) =>
- // redNodesHaveBlackChildren(a) &&
- // redNodesHaveBlackChildren(b) &&
- // redNodesHaveBlackChildren(c) &&
- // redNodesHaveBlackChildren(d)
- // case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) =>
- // redNodesHaveBlackChildren(a) &&
- // redNodesHaveBlackChildren(b) &&
- // redNodesHaveBlackChildren(c) &&
- // redNodesHaveBlackChildren(d)
- // case t => redDescHaveBlackChildren(t)
- // }
- // )
- 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,xV,d)) // FIXME: xV instead of zV in right node
- 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))
- // }
- // } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
-
}
diff --git a/testcases/repair/RedBlackTree/RedBlackTree6.scala b/testcases/repair/RedBlackTree/RedBlackTree6.scala
index 36cfb692b..9eed1ac3a 100644
--- a/testcases/repair/RedBlackTree/RedBlackTree6.scala
+++ b/testcases/repair/RedBlackTree/RedBlackTree6.scala
@@ -1,4 +1,4 @@
-import leon._
+import leon._
import lang._
import annotation._
@@ -7,31 +7,67 @@ object RedBlackTree {
case object Red extends Color
case object Black extends Color
- sealed abstract class Tree
- case object Empty extends Tree
- case class Node(color: Color, left: Tree, value: Int, right: Tree) extends Tree
+ sealed abstract class Tree {
+ /* We consider leaves to be black by definition */
+ def color = this match {
+ case Empty => Black
+ case Node(c,_,_,_) => c
+ }
- def content(t: Tree) : Set[Int] = t match {
- case Empty => Set.empty
- case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
- }
+ def content : Set[Int] = this match {
+ case Empty => Set.empty
+ case Node(_, l, v, r) => l.content ++ Set(v) ++ r.content
+ }
- def size(t: Tree) : Int = t match {
- case Empty => 0
- case Node(_, l, v, r) => size(l) + 1 + size(r)
- }
+ def size : Int = this match {
+ case Empty => 0
+ case Node(_, l, v, r) => l.size + 1 + r.size
+ }
- /* 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 isBlack = color == Black
+
+ def blackHeight : Int = this match {
+ case Empty => 1
+ case Node(Black, l, _, _) => l.blackHeight + 1
+ case Node(Red, l, _, _) => l.blackHeight
+ }
+
+ def max : Option[Int] = this match {
+ case Empty => None()
+ case Node(_, l, v, r) =>
+ maxOption(Some(v), maxOption(l.max, r.max))
+ }
+
+ def min : Option[Int] = this match {
+ case Empty => None()
+ case Node(_, l, v, r) =>
+ minOption(Some(v), minOption(l.max, r.max))
+ }
+
+ }
+
+ def minOption(i1 : Option[Int], i2 : Option[Int]) : Option[Int] = (i1, i2) match {
+ case (Some(i1), Some(i2)) => Some(if (i1 < i2) i1 else i2)
+ case _ => i1 orElse i2
+ }
+
+ def maxOption(i1 : Option[Int], i2 : Option[Int]) : Option[Int] = (i1, i2) match {
+ case (Some(i1), Some(i2)) => Some(if (i1 > i2) i1 else i2)
+ case _ => i1 orElse i2
}
+ case object Empty extends Tree
+ case class Node(color_ : Color, left: Tree, value: Int, right: Tree) extends Tree
+
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)
+ case Node(Black, l, _, r) =>
+ redNodesHaveBlackChildren(l) &&
+ redNodesHaveBlackChildren(r)
+ case Node(Red, l, _, r) =>
+ l.isBlack && r.isBlack &&
+ redNodesHaveBlackChildren(l) &&
+ redNodesHaveBlackChildren(r)
}
def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
@@ -40,80 +76,70 @@ object RedBlackTree {
}
def blackBalanced(t : Tree) : Boolean = t match {
- case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && l.blackHeight == r.blackHeight
case Empty => true
}
-
- def blackHeight(t : Tree) : Int = t match {
- case Empty => 1
- case Node(Black, l, _, _) => blackHeight(l) + 1
- case Node(Red, l, _, _) => blackHeight(l)
+
+ def keysSorted(t : Tree) : Boolean = t match {
+ case Empty => true
+ case Node(_, l, v, r) =>
+ keysSorted(l) && keysSorted(r) &&
+ (l.max.getOrElse (v-1) < v) &&
+ (r.min.getOrElse (v+1) > v)
}
-
-
+
+
// <<insert element x into the tree t>>
def ins(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) && keysSorted(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))
+ case n@Node(c,a,y,b) =>
+ if (x < y) balance(Node(c, ins(x, a), y, b))
+ else if (x == y) n
+ else balance(Node(c, a, y, ins(x, b)))
}
} ensuring (res =>
- content(res) == content(t) ++ Set(x) &&
- size(t) <= size(res) &&
- size(res) <= size(t) + 1 &&
+ res.content == t.content ++ Set(x) &&
+ t.size <= res.size &&
+ res.size <= t.size + 1 &&
+ keysSorted(res) &&
redDescHaveBlackChildren(res) &&
blackBalanced(res)
)
def makeBlack(n: Tree): Tree = {
- require(redDescHaveBlackChildren(n) && blackBalanced(n) )
+ require(
+ redDescHaveBlackChildren(n) &&
+ blackBalanced(n) &&
+ keysSorted(n)
+ )
n match {
case Node(Red,l,v,r) => Node(Black,l,v,r)
case _ => n
}
- } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res) )
+ } ensuring { res =>
+ res.isBlack &&
+ redNodesHaveBlackChildren(res) &&
+ blackBalanced(res) &&
+ keysSorted(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 add(x: Int, t: Tree): Tree = {
- require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
- ins(x, t) // FIXME: makeBlack(ins(x, t))
- } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res) )
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t) && keysSorted(t))
+ ins(x, t) // FIXME forgot makeBlack
+ } ensuring { res =>
+ res.content == t.content ++ Set(x) &&
+ redNodesHaveBlackChildren(res) &&
+ blackBalanced(res) &&
+ keysSorted(res)
+ }
- def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
- // require(
- // Node(c,a,x,b) match {
- // case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
- // redNodesHaveBlackChildren(a) &&
- // redNodesHaveBlackChildren(b) &&
- // redNodesHaveBlackChildren(c) &&
- // redNodesHaveBlackChildren(d)
- // case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
- // redNodesHaveBlackChildren(a) &&
- // redNodesHaveBlackChildren(b) &&
- // redNodesHaveBlackChildren(c) &&
- // redNodesHaveBlackChildren(d)
- // case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) =>
- // redNodesHaveBlackChildren(a) &&
- // redNodesHaveBlackChildren(b) &&
- // redNodesHaveBlackChildren(c) &&
- // redNodesHaveBlackChildren(d)
- // case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) =>
- // redNodesHaveBlackChildren(a) &&
- // redNodesHaveBlackChildren(b) &&
- // redNodesHaveBlackChildren(c) &&
- // redNodesHaveBlackChildren(d)
- // case t => redDescHaveBlackChildren(t)
- // }
- // )
- Node(c,a,x,b) match {
+
+ def balance(t : Tree) : Tree = {
+ require(keysSorted(t))
+ t match {
+ case Empty => Empty
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) =>
@@ -122,21 +148,12 @@ object RedBlackTree {
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)
+ case other => other
}
- } 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))
- // }
- // } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+ } ensuring { res =>
+ res.content == t.content &&
+ keysSorted(res)
+ }
+
}
--
GitLab