examples

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)

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 {

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 = {

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 {

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))