From c5f704ebc3352844de17b45707c7ace4aad989b9 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ali=20Sinan=20K=C3=B6ksal?= <alisinan@gmail.com>
Date: Fri, 19 Nov 2010 14:32:47 +0000
Subject: [PATCH] Size equivalence, concat and reverse proofs in ListWithSize
---
evaluation_results | 42 ++++++++++++++++++-----------
pldi2011-testcases/LambdaEval.scala | 38 +++++++++++++++-----------
testcases/ListWithSize.scala | 30 ++++++++++++++++-----
3 files changed, 72 insertions(+), 38 deletions(-)
diff --git a/evaluation_results b/evaluation_results
index ced6b7199..c1d60e790 100644
--- a/evaluation_results
+++ b/evaluation_results
@@ -2,26 +2,36 @@ testcases/ListWithSize.scala
verifies: associativity of append, size
-size match. (11,34) valid Z3 0.266
-size postcond. valid Z3 0.031
-content match. (16,41) valid Z3 0.002
-sizeAndContent postcond. valid Z3 0.007
-drunk match. (25,37) valid Z3 0.002
-drunk postcond. valid Z3 0.406
-funnyCons match. (31,48) valid Z3 0.005
-funnyCons postcond. valid Z3 0.154
-reverse0 match. (38,50) valid Z3 0.004
-append match. (43,51) valid Z3 0.002
-nilAppend postcond. valid induction Z3 0.004
+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
+sizesAreEquiv postcond. valid Z3 0.010
+content match. (30,41) valid Z3 0.004
+sizeAndContent postcond. valid Z3 0.009
+drunk match. (39,37) valid Z3 0.002
+drunk postcond. valid Z3 0.671
+funnyCons match. (45,48) valid Z3 0.007
+funnyCons postcond. valid Z3 0.263
+reverse postcond. valid Z3 0.010
+reverse0 match. (52,51) valid Z3 0.002
+reverse0 postcond. valid Z3 0.023
+append match. (57,51) valid Z3 0.002
+nilAppend postcond. valid induction Z3 0.003
nilAppend postcond. valid induction Z3 0.003
appendFold postcond. valid Z3 0.006
appendAssoc postcond. valid induction Z3 0.005
-appendAssoc postcond. valid induction Z3 0.006
+appendAssoc postcond. valid induction Z3 0.007
sizeAppend postcond. valid induction Z3 0.006
-sizeAppend postcond. valid induction Z3 0.011
-concat0 match. (67,60) valid Z3 0.002
-concat0 match. (68,24) valid Z3 0.002
-property1 postcond. unknown
+sizeAppend postcond. valid induction Z3 0.012
+concat postcond. valid induction Z3 0.010
+concat postcond. valid induction Z3 0.012
+concat0 match. (84,60) valid induction Z3 0.002
+concat0 match. (85,24) valid induction Z3 0.002
+concat0 postcond. valid induction Z3 0.054
+concat0 postcond. valid induction Z3 0.085
/* Appending a list 'l' to an empty list yields 'l' */
@induct
diff --git a/pldi2011-testcases/LambdaEval.scala b/pldi2011-testcases/LambdaEval.scala
index 9cdcb161f..889847edb 100644
--- a/pldi2011-testcases/LambdaEval.scala
+++ b/pldi2011-testcases/LambdaEval.scala
@@ -1,4 +1,5 @@
import scala.collection.immutable.Set
+import funcheck.Annotations._
import funcheck.Utils._
object LambdaEval {
@@ -55,11 +56,16 @@ object LambdaEval {
case Cons(BindingPair(k, v), ss) => isValue(v) && storeHasValues(ss)
}
+ def contains(store: List, key: Int): Boolean = store match {
+ case Nil() => false
+ case Cons(BindingPair(k, v), xs) => k == key || contains(xs, key)
+ }
+
// 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) &&
+ contains(l, x) &&
storeHasValues(l)
)
l match {
@@ -68,18 +74,7 @@ object LambdaEval {
} 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 Const(_) => true
case Plus(e1, e2) => wellFormed(store, e1) && wellFormed(store, e2) && (eval(store, e1) match {
case StoreExprPair(_,Const(i1)) =>
eval(store, e2) match {
@@ -88,13 +83,26 @@ object LambdaEval {
}
case _ => false
})
- case _ => true
+ case Lam(x, body) => wellFormed(Cons(BindingPair(x, Const(0)), store), body)
+ case Pair(e1, e2) => wellFormed(store, e1) && wellFormed(store, e2)
+ case Var(x) => contains(store, x)
+ case App(l, r) => wellFormed(store, l) && wellFormed(store, r) && (eval(store, l) match {
+ case StoreExprPair(_, Lam(_,_)) => true
+ case _ => false
+ })
+ case Fst(e) => wellFormed(store, e) && (eval(store, e) match {
+ case StoreExprPair(_,Pair(e1, e2)) => true
+ case _ => false
+ })
+ case Snd(e) => wellFormed(store, e) && (eval(store, e) match {
+ case StoreExprPair(_,Pair(e1, e2)) => true
+ case _ => false
+ })
}
// Evaluator
def eval(store: List, expr: Expr): StoreExprPairAbs = {
require(
- freeVars(expr).subsetOf(storeElems(store)) &&
wellFormed(store, expr) &&
storeHasValues(store)
)
diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala
index 684dfa806..5ee384786 100644
--- a/testcases/ListWithSize.scala
+++ b/testcases/ListWithSize.scala
@@ -13,6 +13,19 @@ 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 = {
+ require(acc >= 0)
+ l match {
+ case Nil() => acc
+ case Cons(_, xs) => size2acc(xs, acc+1)
+ }
+ } ensuring(res => res == size(l) + acc)
+
+ def sizesAreEquiv(l: List) : Boolean = {
+ size(l) == size2(l)
+ } holds
+
def content(l: List) : Set[Int] = l match {
case Nil() => Set.empty[Int]
case Cons(x, xs) => Set(x) ++ content(xs)
@@ -34,11 +47,11 @@ object ListWithSize {
}) ensuring(size(_) > 0)
// proved with unrolling=2
- def reverse(l: List) : List = reverse0(l, Nil()) // ensuring(content(_) == content(l))
- def reverse0(l1: List, l2: List) : List = l1 match {
+ def reverse(l: List) : List = reverse0(l, Nil()) ensuring(content(_) == content(l))
+ def reverse0(l1: List, l2: List) : List = (l1 match {
case Nil() => l2
case Cons(x, xs) => reverse0(xs, Cons(x, l2))
- }
+ }) ensuring(content(_) == content(l1) ++ content(l2))
def append(l1 : List, l2 : List) : List = (l1 match {
case Nil() => l2
@@ -62,8 +75,11 @@ object ListWithSize {
(size(append(l1, l2)) == size(l1) + size(l2)) holds
// proved with unrolling=4
- def concat(l1: List, l2: List) : List = concat0(l1, l2, Nil())
- // ensuring(content(_) == content(l1) ++ content(l2))
+ @induct
+ def concat(l1: List, l2: List) : List =
+ concat0(l1, l2, Nil()) ensuring(content(_) == content(l1) ++ content(l2))
+
+ @induct
def concat0(l1: List, l2: List, l3: List) : List = (l1 match {
case Nil() => l2 match {
case Nil() => reverse(l3)
@@ -72,10 +88,10 @@ object ListWithSize {
}
}
case Cons(x, xs) => concat0(xs, l2, Cons(x, l3))
- }) //ensuring(content(_) == content(l1) ++ content(l2) ++ content(l3))
+ }) ensuring(content(_) == content(l1) ++ content(l2) ++ content(l3))
// proved with unrolling=2 ???
def property1(l1: List, l2: List) : Boolean = {
reverse(concat(l1, l2)) == concat(reverse(l2), reverse(l1))
- } ensuring(_ == true)
+ } // ensuring(_ == true)
}
--
GitLab