diff --git a/pldi2011-testcases/AssociativeList.scala b/pldi2011-testcases/AssociativeList.scala
index 551d404507f2010244bccb5ef7278db62f25d38e..ed18a6bba8619fd38aa3d38d9fcea7808a5eedaf 100644
--- a/pldi2011-testcases/AssociativeList.scala
+++ b/pldi2011-testcases/AssociativeList.scala
@@ -37,7 +37,7 @@ object AssociativeList {
def updateElem(l: List, e: KeyValuePairAbs): List = (l match {
case Nil() => Cons(e, Nil())
case Cons(KeyValuePair(k, v), xs) => e match {
- case KeyValuePair(ek, ev) => if (ek == k) updateElem(xs, e) else Cons(KeyValuePair(k, v), updateElem(xs, e))
+ case KeyValuePair(ek, ev) => if (ek == k) Cons(KeyValuePair(ek, ev), xs) else Cons(KeyValuePair(k, v), updateElem(xs, e))
}
}) ensuring(res => e match {
case KeyValuePair(k, v) => domain(res) == domain(l) ++ Set[Int](k)
diff --git a/pldi2011-testcases/InsertionSort.scala b/pldi2011-testcases/InsertionSort.scala
index 339fc28ffcd16dc59772110725ad801d3c55ee07..7d5e0eb62bdee12ef332efba6498dd6695063ed8 100644
--- a/pldi2011-testcases/InsertionSort.scala
+++ b/pldi2011-testcases/InsertionSort.scala
@@ -67,6 +67,19 @@ object InsertionSort {
&& size(res) == size(l) + 1
)
+ /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+ * the expected content and size */
+ def buggySortedIns(e: Int, l: List): List = {
+ // require(isSorted(l))
+ l match {
+ case Nil() => Cons(e,Nil())
+ case Cons(x,xs) => if (x <= e) Cons(x,buggySortedIns(e, xs)) else Cons(e, l)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ && isSorted(res)
+ && size(res) == size(l) + 1
+ )
+
/* Insertion sort yields a sorted list of same size and content as the input
* list */
def sort(l: List): List = (l match {
diff --git a/pldi2011-testcases/PropositionalLogic.scala b/pldi2011-testcases/PropositionalLogic.scala
index 5c35713afafdba77a78a4ef08721b8266e579975..dbdf6e3eeee1ec244fe446eb44f785e8129a7763 100644
--- a/pldi2011-testcases/PropositionalLogic.scala
+++ b/pldi2011-testcases/PropositionalLogic.scala
@@ -48,18 +48,18 @@ object PropositionalLogic {
case Literal(_) => true
}
- def freeVars(f: Formula): Set[Int] = {
+ def vars(f: Formula): Set[Int] = {
require(isNNF(f))
f match {
- case And(lhs, rhs) => freeVars(lhs) ++ freeVars(rhs)
- case Or(lhs, rhs) => freeVars(lhs) ++ freeVars(rhs)
- case Implies(lhs, rhs) => freeVars(lhs) ++ freeVars(rhs)
+ case And(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Or(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Implies(lhs, rhs) => vars(lhs) ++ vars(rhs)
case Not(Literal(i)) => Set[Int](i)
case Literal(i) => Set[Int](i)
}
}
- def fv(f : Formula) = { freeVars(nnf(f)) }
+ def fv(f : Formula) = { vars(nnf(f)) }
@induct
def wrongCommutative(f: Formula) : Boolean = {
diff --git a/pldi2011-testcases/RedBlackTree.scala b/pldi2011-testcases/RedBlackTree.scala
index b2f6bb691f84b7311879162aed0be17ace362fd5..ed076c09192a3e0c50d383a35b3d0d02e3c40816 100644
--- a/pldi2011-testcases/RedBlackTree.scala
+++ b/pldi2011-testcases/RedBlackTree.scala
@@ -65,6 +65,12 @@ object RedBlackTree {
makeBlack(ins(x, t))
} ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(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 {
diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala
index 08f93d8b495525d5165c4129fd60f794ab0ce238..df2522cb88aee9dd8ba7137c355fc65064f02f59 100644
--- a/testcases/ListWithSize.scala
+++ b/testcases/ListWithSize.scala
@@ -7,12 +7,37 @@ object ListWithSize {
case class Cons(head: Int, tail: List) extends List
case class Nil() extends List
+ sealed abstract class IntPairList
+ case class IPCons(head: IntPair, tail: IntPairList) extends IntPairList
+ case class IPNil() extends IntPairList
+
+ sealed abstract class IntPair
+ case class IP(fst: Int, snd: Int) extends IntPair
+
// proved with unrolling=0
def size(l: List) : Int = (l match {
case Nil() => 0
case Cons(_, t) => 1 + size(t)
}) ensuring(_ >= 0)
+ def iplSize(l: IntPairList) : Int = (l match {
+ case IPNil() => 0
+ case IPCons(_, xs) => 1 + iplSize(xs)
+ }) ensuring(_ >= 0)
+
+ def zip(l1: List, l2: List) : IntPairList = {
+ // try to comment this and see how pattern-matching becomes
+ // non-exhaustive and post-condition fails
+ require(size(l1) == size(l2))
+
+ l1 match {
+ case Nil() => IPNil()
+ case Cons(x, xs) => l2 match {
+ case Cons(y, ys) => IPCons(IP(x, y), zip(xs, ys))
+ }
+ }
+ } ensuring(iplSize(_) == size(l1))
+
def sizeTailRec(l: List) : Int = sizeTailRecAcc(l, 0)
def sizeTailRecAcc(l: List, acc: Int) : Int = {
require(acc >= 0)
@@ -34,7 +59,7 @@ object ListWithSize {
def sizeAndContent(l: List) : Boolean = {
size(l) == 0 || content(l) != Set.empty[Int]
} holds
-
+
def drunk(l : List) : List = (l match {
case Nil() => Nil()
case Cons(x,l1) => Cons(x,Cons(x,drunk(l1)))
@@ -53,30 +78,6 @@ object ListWithSize {
case Cons(x, xs) => reverse0(xs, Cons(x, l2))
}) ensuring(content(_) == content(l1) ++ content(l2))
-
-
- /*** revAppend cannot use appendAssoc ***/
- /*
- @induct
- def revSimple(l: List) : List = (l match {
- case Nil() => Nil()
- case Cons(x, xs) => append(revSimple(xs), Cons(x, Nil()))
- }) ensuring(content(_) == content(l))
-
- @induct
- def revAppend(l1: List, l2: List) : Boolean = {
- require(l1 match {
- case Nil() => true
- case Cons(x, xs) => appendAssoc(revSimple(l2), revSimple(xs), Cons(x, Nil()))
- })
- revSimple(append(l1, l2)) == append(revSimple(l2), revSimple(l1))
- } holds
-
- @induct
- def reverseTwice(l: List): Boolean =
- (revSimple(revSimple(l)) == l) holds */
- /***************************************/
-
def append(l1 : List, l2 : List) : List = (l1 match {
case Nil() => l2
case Cons(x,xs) => Cons(x, append(xs, l2))