diff --git a/evaluation_results b/evaluation_results
index c1d60e790219024f71dd9af707024a46808a1e85..50bf1fc9ac8e7c851a2fbe99d393197945ece5c0 100644
--- a/evaluation_results
+++ b/evaluation_results
@@ -4,10 +4,10 @@ verifies: associativity of append, size
size match. (11,34) valid Z3 0.383
size postcond. valid Z3 0.036
-size2 precond. (16,40) valid Z3 0.003
-size2acc precond. (21,36) valid Z3 0.005
-size2acc match. (19,8) valid Z3 0.003
-size2acc postcond. valid Z3 0.026
+sizeTailRec precond. (16,40) valid Z3 0.003
+sizeTailRecAcc precond. (21,36) valid Z3 0.005
+sizeTailRecAcc match. (19,8) valid Z3 0.003
+sizeTailRecAcc postcond. valid Z3 0.026
sizesAreEquiv postcond. valid Z3 0.010
content match. (30,41) valid Z3 0.004
sizeAndContent postcond. valid Z3 0.009
@@ -19,6 +19,8 @@ reverse postcond. valid Z3 0.01
reverse0 match. (52,51) valid Z3 0.002
reverse0 postcond. valid Z3 0.023
append match. (57,51) valid Z3 0.002
+append match. (80,51) valid Z3 0.004
+append postcond. valid Z3 0.050
nilAppend postcond. valid induction Z3 0.003
nilAppend postcond. valid induction Z3 0.003
appendFold postcond. valid Z3 0.006
@@ -37,16 +39,35 @@ concat0 postcond. valid induction Z3 0.08
@induct
def nilAppend(l : List) : Boolean = (append(l, Nil()) == l) holds
- /* append is associative */
- @induct
- def appendAssoc(xs : List, ys : List, zs : List) : Boolean =
- (append(append(xs, ys), zs) == append(xs, append(ys, zs))) holds
-
- /* The size of the result of appending two lists is the sum of the sizes of
- * the lists */
- @induct
- def sizeAppend(l1 : List, l2 : List) : Boolean =
- (size(append(l1, l2)) == size(l1) + size(l2)) holds
+* /* append is associative */
+* @induct
+* def appendAssoc(xs : List, ys : List, zs : List) : Boolean =
+* (append(append(xs, ys), zs) == append(xs, append(ys, zs))) holds
+
+* /* The size of the result of appending two lists is the sum of the sizes of
+* * the lists */
+* @induct
+* def sizeAppend(l1 : List, l2 : List) : Boolean =
+* (size(append(l1, l2)) == size(l1) + size(l2)) holds
+
+ def size(l: List) : Int = (l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(_ >= 0)
+
+ def sizeTailRec(l: List) : Int = sizeTailRecAcc(l, 0)
+ def sizeTailRecAcc(l: List, acc: Int) : Int = {
+ require(acc >= 0)
+ l match {
+ case Nil() => acc
+ case Cons(_, xs) => sizeTailRecAcc(xs, acc+1)
+ }
+ } ensuring(res => res == size(l) + acc)
+
+* /* The two size functions are equivalent */
+* def sizesAreEquiv(l: List) : Boolean = {
+* size(l) == sizeTailRec(l)
+* } holds
==============================
@@ -83,12 +104,12 @@ readOverWrite postcond. valid induction Z3 0.02
case KeyValuePair(k, v) => domain(res) == domain(l) ++ Set[Int](k)
})
- /* Finding with a key that has been updated gives the most recently updated value */
- @induct
- def readOverWrite(l: List, e: KeyValuePairAbs, k: Int) : Boolean = (e match {
- case KeyValuePair(key, value) =>
- find(updateElem(l, e), k) == (if (k == key) Some(value) else find(l, k))
- }) holds
+* /* Finding with a key that has been updated gives the most recently updated value */
+* @induct
+* def readOverWrite(l: List, e: KeyValuePairAbs, k: Int) : Boolean = (e match {
+* case KeyValuePair(key, value) =>
+* find(updateElem(l, e), k) == (if (k == key) Some(value) else find(l, k))
+* }) holds
==============================
@@ -161,6 +182,13 @@ add postcond. valid Z3 0.02
balance match. (94,19) valid Z3 0.028
balance postcond. valid Z3 0.999
+w/o balance conditions
+ins precond. (46,40) valid Z3 0.029
+ins precond. (48,43) valid Z3 0.012
+ins match. (43,7) valid Z3 0.005
+ins postcond. valid Z3 100.981
+
+
/* Adding value 'x' to tree 't' in which no red node has a red child produces
* a tree which conserves the same property and has the expected content */
def add(x: Int, t: Tree): Tree = {
@@ -212,26 +240,38 @@ nnfIsStable postcond. valid induction Z3 0.07
nnfIsStable postcond. valid induction Z3 0.076
nnfIsStable postcond. valid induction Z3 0.053
nnfIsStable postcond. valid induction Z3 0.073
-
- /* Wrong assumption that 'nnf' and 'simplify' commute */
- @induct
- def wrongCommutative(f: Formula) : Boolean = {
- nnf(simplify(f)) == simplify(nnf(f))
- } holds
-
- /* Wrong assumption that 'simplify' preserves NNF */
- @induct
- def simplifyBreaksNNF(f: Formula) : Boolean = {
- require(isNNF(f))
- isNNF(simplify(f))
- } holds
-
- /* A formula in NNF is not modified by the NNF transformation */
- @induct
- def nnfIsStable(f: Formula) : Boolean = {
- require(isNNF(f))
- nnf(f) == f
- } holds
+simplifyIsStable postcond. valid induction Z3 0.079
+simplifyIsStable postcond. valid induction Z3 0.078
+simplifyIsStable postcond. valid induction Z3 0.078
+simplifyIsStable postcond. valid induction Z3 0.055
+simplifyIsStable postcond. valid induction Z3 0.068
+
+* /* Wrong assumption that 'nnf' and 'simplify' commute */
+* @induct
+* def wrongCommutative(f: Formula) : Boolean = {
+* nnf(simplify(f)) == simplify(nnf(f))
+* } holds
+
+* /* Wrong assumption that 'simplify' preserves NNF */
+* @induct
+* def simplifyBreaksNNF(f: Formula) : Boolean = {
+* require(isNNF(f))
+* isNNF(simplify(f))
+* } holds
+
+* /* A formula in NNF is not modified by the NNF transformation */
+* @induct
+* def nnfIsStable(f: Formula) : Boolean = {
+* require(isNNF(f))
+* nnf(f) == f
+* } holds
+
+* /* A simplified formula is not modified by the simplifying transformation */
+* @induct
+* def simplifyIsStable(f: Formula) : Boolean = {
+* require(isSimplified(f))
+* simplify(f) == f
+* } holds
/* It is sufficient to consider negations of only literals in pattern
* matching */
diff --git a/pldi2011-testcases/PropositionalLogic.scala b/pldi2011-testcases/PropositionalLogic.scala
index b82f96854f3c7bad829bbe060d2c674fb1cd63ad..5c35713afafdba77a78a4ef08721b8266e579975 100644
--- a/pldi2011-testcases/PropositionalLogic.scala
+++ b/pldi2011-testcases/PropositionalLogic.scala
@@ -77,4 +77,10 @@ object PropositionalLogic {
require(isNNF(f))
nnf(f) == f
} holds
+
+ @induct
+ def simplifyIsStable(f: Formula) : Boolean = {
+ require(isSimplified(f))
+ simplify(f) == f
+ } holds
}
diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala
index 5ee3847861e34c8e84b3481c7e5367c427809a26..08f93d8b495525d5165c4129fd60f794ab0ce238 100644
--- a/testcases/ListWithSize.scala
+++ b/testcases/ListWithSize.scala
@@ -13,17 +13,17 @@ object ListWithSize {
case Cons(_, t) => 1 + size(t)
}) ensuring(_ >= 0)
- def size2(l: List) : Int = size2acc(l, 0)
- def size2acc(l: List, acc: Int) : Int = {
+ def sizeTailRec(l: List) : Int = sizeTailRecAcc(l, 0)
+ def sizeTailRecAcc(l: List, acc: Int) : Int = {
require(acc >= 0)
l match {
case Nil() => acc
- case Cons(_, xs) => size2acc(xs, acc+1)
+ case Cons(_, xs) => sizeTailRecAcc(xs, acc+1)
}
} ensuring(res => res == size(l) + acc)
def sizesAreEquiv(l: List) : Boolean = {
- size(l) == size2(l)
+ size(l) == sizeTailRec(l)
} holds
def content(l: List) : Set[Int] = l match {
@@ -33,7 +33,7 @@ object ListWithSize {
def sizeAndContent(l: List) : Boolean = {
size(l) == 0 || content(l) != Set.empty[Int]
- } ensuring(_ == true)
+ } holds
def drunk(l : List) : List = (l match {
case Nil() => Nil()
@@ -53,10 +53,34 @@ 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))
- })
+ }) ensuring(content(_) == content(l1) ++ content(l2))
@induct
def nilAppend(l : List) : Boolean = (append(l, Nil()) == l) holds