diff --git a/pldi2011-testcases/LambdaEval.scala b/pldi2011-testcases/LambdaEval.scala
index 33512b7f7909bc3ef873adfcb1426978456beb94..9cdcb161f9b19337ab9f684e137bb7ec96c1a6ca 100644
--- a/pldi2011-testcases/LambdaEval.scala
+++ b/pldi2011-testcases/LambdaEval.scala
@@ -13,10 +13,10 @@ object LambdaEval {
case class Snd(e: Expr) extends Expr
// Checks whether the expression is a value
- def ok(expr: Expr): Boolean = expr match {
+ def isValue(expr: Expr): Boolean = expr match {
case Const(_) => true
case Lam(_,_) => true
- case Pair(e1, e2) => ok(e1) && ok(e2)
+ case Pair(e1, e2) => isValue(e1) && isValue(e2)
case Var(_) => false
case Plus(_,_) => false
case App(_,_) => false
@@ -24,10 +24,6 @@ object LambdaEval {
case Snd(_) => false
}
- def okPair(p: StoreExprPairAbs): Boolean = p match {
- case StoreExprPair(_, res) => ok(res)
- }
-
sealed abstract class List
case class Cons(head: BindingPairAbs, tail: List) extends List
case class Nil() extends List
@@ -54,26 +50,53 @@ object LambdaEval {
case Snd(e) => freeVars(e)
}
+ def storeHasValues(store: List): Boolean = store match {
+ case Nil() => true
+ case Cons(BindingPair(k, v), ss) => isValue(v) && storeHasValues(ss)
+ }
+
// Find first element in list that has first component 'x' and return its
// second component, analogous to List.assoc in OCaml
def find(x: Int, l: List): Expr = {
- require(storeElems(l).contains(x))
+ require(
+ storeElems(l).contains(x) &&
+ storeHasValues(l)
+ )
l match {
case Cons(BindingPair(k,v), is) => if (k == x) v else find(x, is)
}
+ } ensuring(res => isValue(res))
+
+ def wellFormed(store: List, expr: Expr): Boolean = expr match {
+ case App(l, _) => eval(store, l) match {
+ case StoreExprPair(_, Lam(_,_)) => true
+ case _ => false
+ }
+ case Fst(e) => eval(store, e) match {
+ case StoreExprPair(_,Pair(e1, e2)) => true
+ case _ => false
+ }
+ case Snd(e) => eval(store, e) match {
+ case StoreExprPair(_,Pair(e1, e2)) => true
+ case _ => false
+ }
+ case Plus(e1, e2) => wellFormed(store, e1) && wellFormed(store, e2) && (eval(store, e1) match {
+ case StoreExprPair(_,Const(i1)) =>
+ eval(store, e2) match {
+ case StoreExprPair(_,Const(i2)) => true
+ case _ => false
+ }
+ case _ => false
+ })
+ case _ => true
}
// Evaluator
def eval(store: List, expr: Expr): StoreExprPairAbs = {
require(
- freeVars(expr).subsetOf(storeElems(store))
- && (expr match {
- case App(l, _) => eval(store, l) match {
- case StoreExprPair(_, Lam(_,_)) => true
- case _ => false
- }
- case _ => true
- })
+ freeVars(expr).subsetOf(storeElems(store)) &&
+ wellFormed(store, expr) &&
+ storeHasValues(store)
)
expr match {
@@ -97,11 +120,6 @@ object LambdaEval {
val e = eval(store, e1) match {
case StoreExprPair(_, Lam(_, resE)) => resE
}
- /*
- val StoreExprPair(store1, Lam(x, e)) = eval(store, e1) match {
- case StoreExprPair(resS, Lam(resX, resE)) => StoreExprPair(resS, Lam(resX, resE))
- }
- */
val v2 = eval(store, e2) match {
case StoreExprPair(_, v) => v
}
@@ -124,12 +142,13 @@ object LambdaEval {
case StoreExprPair(_, Pair(_, v2)) => StoreExprPair(store, v2)
}
}
- } ensuring(res => okPair(res))
- /*ensuring(res => res match {
- case StoreExprPair(_, resExpr) => ok(resExpr)
- }) */
+ } ensuring(res => res match {
+ case StoreExprPair(s, e) => storeHasValues(s) && isValue(e)
+ })
def property0() : Boolean = {
- okPair(eval(Cons(BindingPair(358, Const(349)), Nil()), Const(1)))
+ eval(Cons(BindingPair(358, Const(349)), Nil()), Const(1)) match {
+ case StoreExprPair(s, e) => isValue(e)
+ }
} holds
}
diff --git a/pldi2011-testcases/TreeMap.scala b/pldi2011-testcases/TreeMap.scala
index d247859b4351bb90ce22e38dac991425f6010b86..5b734cf92d97c55f7a5c5a0b255ee2f1fc326b18 100644
--- a/pldi2011-testcases/TreeMap.scala
+++ b/pldi2011-testcases/TreeMap.scala
@@ -42,26 +42,51 @@ object TreeMap {
case Node(_,_,_,_,h) => h
})
+ /*
def invariant0(tm : TreeMap) : Boolean = {
require(nodeHeightsAreCorrect(tm))
height(tm) == realHeight(tm)
} holds
+ def invariant1(tm: TreeMap): Boolean = {
+ require((tm match {
+ case Empty() => true
+ case Node(_,_,l,r,_) => nodeHeightsAreCorrect(l) && nodeHeightsAreCorrect(r)
+ }) && nodeHeightsAreCorrect(tm))
+ tm match {
+ case Empty() => true
+ case Node(_,_,l,r,h) => h == mmax(height(l), height(r)) + 1
+ }
+ } // holds
+
+ def invariant2(tm: TreeMap): Boolean = {
+ require(nodeHeightsAreCorrect(tm))
+ tm match {
+ case Empty() => true
+ case Node(_,_,l,r,_) =>
+ val h = height(tm)
+ h > height(l) && h > height(r) // && invariant2(l) && invariant2(r)
+ }
+ } // holds
+ */
+
def setOf(tm: TreeMap): Set[Int] = tm match {
case Empty() => Set.empty
case Node(d, _, l, r, _) => Set(d) ++ setOf(l) ++ setOf(r)
}
def create(k: Int, d: Int, l: TreeMap, r: TreeMap): TreeMap = {
- require(nodeHeightsAreCorrect(l) && nodeHeightsAreCorrect(r))
+ require(nodeHeightsAreCorrect(l) && nodeHeightsAreCorrect(r) && isBalanced(l) && isBalanced(r) &&
+ height(l) - height(r) <= 2 && height(r) - height(l) <= 2)
val hl = height(l)
val hr = height(r)
- Node(k, d, l, r, if (hl >= hr) hl + 1 else hr + 1)
- } ensuring(setOf(_) == Set(k) ++ setOf(l) ++ setOf(r)) //ensuring(isBalanced(_))
+ Node(k, d, l, r, mmax(hl, hr) + 1)
+ } ensuring(res => setOf(res) == Set(k) ++ setOf(l) ++ setOf(r) && isBalanced(res))
def balance(x: Int, d: Int, l: TreeMap, r: TreeMap): TreeMap = {
require(
- nodeHeightsAreCorrect(l) && nodeHeightsAreCorrect(r) &&
+ nodeHeightsAreCorrect(l) && nodeHeightsAreCorrect(r) && isBalanced(l) && isBalanced(r) &&
+ height(l) - height(r) <= 3 && height(r) - height(l) <= 3 &&
(r match {
case Empty() => false
case Node(_, _, Empty(), _, _) => false
@@ -100,67 +125,84 @@ object TreeMap {
}
} else
Node(x, d, l, r, if(hl >= hr) hl + 1 else hr + 1)
- } ensuring(setOf(_) == Set(x) ++ setOf(l) ++ setOf(r)) //ensuring(isBalanced(_))
-
- def add(x: Int, data: Int, tm: TreeMap): TreeMap = tm match {
- case Empty() => Node(x, data, Empty(), Empty(), 1)
- case Node(v, d, l, r, h) =>
- if (x == v)
- Node(x, data, l, r, h)
- else if (x < v)
- balance(v, d, add(x, data, l), r)
- else
- balance(v, d, l, add(x, data, r))
- }
-
- def removeMinBinding(t: TreeMap): Triple = t match {
- case Empty() => error("invalid arg")
- case Node(x, d, l, r, h) =>
- l match {
- case Empty() => Triple(x, d, r)
- case Node(_,_,ll, lr, h2) =>
- val triple = removeMinBinding(l)
- Triple(triple.key, triple.datum, balance(x, d, triple.tree, r))
- }
- }
+ } ensuring(isBalanced(_))
+
+ def add(x: Int, data: Int, tm: TreeMap): TreeMap = {
+ require(isBalanced(tm) && nodeHeightsAreCorrect(tm))
+ tm match {
+ case Empty() => Node(x, data, Empty(), Empty(), 1)
+ case Node(v, d, l, r, h) =>
+ if (x == v)
+ Node(x, data, l, r, h)
+ else if (x < v)
+ balance(v, d, add(x, data, l), r)
+ else
+ balance(v, d, l, add(x, data, r))
+ }
+ } ensuring(isBalanced(_))
+
+ def removeMinBinding(t: TreeMap): Triple = {
+ require(isBalanced(t) && (t match {
+ case Empty() => false
+ case _ => true
+ }))
+ t match {
+ case Node(x, d, l, r, h) =>
+ l match {
+ case Empty() => Triple(x, d, r)
+ case Node(_,_,ll, lr, h2) =>
+ val triple = removeMinBinding(l)
+ Triple(triple.key, triple.datum, balance(x, d, triple.tree, r))
+ }
+ }
+ } ensuring(res => isBalanced(res.tree))
// m is not used here!
- def merge(m: Int, t1: TreeMap, t2: TreeMap): TreeMap = t1 match {
- case Empty() => t2
- case Node(_, _, ll, lr, h1) =>
- t2 match {
- case Empty() => t1
- case Node(r, _, rl, rr, h2) =>
- val triple = removeMinBinding(t2)
- balance(triple.key, triple.datum, t1, triple.tree)
- }
- }
-
- def remove(x: Int, t: TreeMap): TreeMap = t match {
- case Empty() => Empty()
- case Node(v, d, l, r, h) =>
- if (x == v)
- merge(x, l, r)
- else if (x < v)
- balance(v, d, remove(x, l), r)
- else
- balance(v, d, l, remove(x, r))
+ def merge(m: Int, t1: TreeMap, t2: TreeMap): TreeMap = {
+ require(isBalanced(t1) && isBalanced(t2))
+ t1 match {
+ case Empty() => t2
+ case Node(_, _, ll, lr, h1) =>
+ t2 match {
+ case Empty() => t1
+ case Node(r, _, rl, rr, h2) =>
+ val triple = removeMinBinding(t2)
+ balance(triple.key, triple.datum, t1, triple.tree)
+ }
+ }
+ } ensuring(isBalanced(_))
+
+ def remove(x: Int, t: TreeMap): TreeMap = {
+ require(isBalanced(t))
+ t match {
+ case Empty() => Empty()
+ case Node(v, d, l, r, h) =>
+ if (x == v)
+ merge(x, l, r)
+ else if (x < v)
+ balance(v, d, remove(x, l), r)
+ else
+ balance(v, d, l, remove(x, r))
+ }
+ } ensuring(isBalanced(_))
+
+ def find(t: TreeMap, x: Int): Int = {
+ require(t match {
+ case Empty() => false
+ case _ => true
+ })
+ t match {
+ case Node(d, _, l, r, _) =>
+ if (x == d)
+ d
+ else if (x < d)
+ find(l, x)
+ else
+ find(r, x)
+ }
}
- def find(t: TreeMap, x: Int): Int = t match {
- case Empty() => error("invalid arg")
- case Node(d, _, l, r, _) =>
- if (x == d)
- d
- else if (x < d)
- find(l, x)
- else
- find(r, x)
- }
-
- // iter takes a function...
-
- // let us specialize it for the condition k < v
+ // let us specialize iter for the condition k < v
def iter1(t: TreeMap, v: Int): Boolean = t match {
case Empty() => true
case Node(k, d, l, r, _) =>
@@ -180,6 +222,8 @@ object TreeMap {
iter1(l, v) && iter2(r, v) && checkBST(l) && checkBST(r)
}
+ // We have a variant of AVL trees where the heights of the subtrees differ at
+ // most by 2
def isBalanced(t: TreeMap): Boolean = t match {
case Empty() => true
case Node(_, _, l, r, _) => (height(l) - height(r) <= 2 && height(r) - height(l) <= 2) && isBalanced(l) && isBalanced(r)
diff --git a/testcases/InsertionSort.scala b/testcases/InsertionSort.scala
index 50fcf358bcda91d3dbb3abf1eecd737ac4a3656b..550083e21ee0d53b89153583e0c2a78ceeaedaa3 100644
--- a/testcases/InsertionSort.scala
+++ b/testcases/InsertionSort.scala
@@ -18,15 +18,18 @@ object InsertionSort {
}
}
- def sortedIns(e: Int, l: List): List = (l match {
- case Nil() => Cons(e,Nil())
- case Cons(x,xs) => if (x < e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
- }) ensuring(res => contents(res) == contents(l) ++ Set(e))
+ def sortedIns(e: Int, l: List): List = {
+ require(isSorted(l))
+ l match {
+ case Nil() => Cons(e,Nil())
+ case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e) && isSorted(res))
def sort(l: List): List = (l match {
case Nil() => Nil()
case Cons(x,xs) => sortedIns(x, sort(xs))
- }) ensuring(res => contents(res) == contents(l))// && isSorted(res))
+ }) ensuring(res => contents(res) == contents(l) && isSorted(res))
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))
diff --git a/testcases/QuickSort.scala b/testcases/QuickSort.scala
index 030ff9e626f5881733fa3222109e8af3117e358e..83dd2c364bfcb3c9cbc2a62497a50903dfc22417 100644
--- a/testcases/QuickSort.scala
+++ b/testcases/QuickSort.scala
@@ -30,7 +30,7 @@ object QuickSort {
def greater(n:Int,list:List) : List = list match {
case Nil() => Nil()
- case Cons(x,xs) => if (n<x) Cons(x,greater(n,xs)) else greater(n,xs)
+ case Cons(x,xs) => if (n < x) Cons(x,greater(n,xs)) else greater(n,xs)
}
def smaller(n:Int,list:List) : List = list match {
@@ -47,7 +47,7 @@ object QuickSort {
case Nil() => Nil()
case Cons(x,Nil()) => list
case Cons(x,xs) => append(append(quickSort(smaller(x,xs)),Cons(x,equals(x,xs))),quickSort(greater(x,xs)))
- }) ensuring(res => contents(res) == contents(list) && is_sorted(res))
+ }) ensuring(res => contents(res) == contents(list)) // && is_sorted(res))
def main(args: Array[String]): Unit = {
val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil()))))))