From 3cd0ea5967eb9fe8b7c4ddb8a82d29950c6fc01d Mon Sep 17 00:00:00 2001
From: Viktor Kuncak <vkuncak@gmail.com>
Date: Fri, 21 Jan 2011 13:54:34 +0000
Subject: [PATCH] why CAV cannot find counterexample
---
pldi2011-testcases/RedBlackTree.scala | 1 +
testcases/ListWithSize.scala | 23 ++++++++++++++++++-----
2 files changed, 19 insertions(+), 5 deletions(-)
diff --git a/pldi2011-testcases/RedBlackTree.scala b/pldi2011-testcases/RedBlackTree.scala
index 1994a857c..7153bba2f 100644
--- a/pldi2011-testcases/RedBlackTree.scala
+++ b/pldi2011-testcases/RedBlackTree.scala
@@ -38,6 +38,7 @@ object RedBlackTree {
case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
}
+ // <<insert element x into the tree t>>
def ins(x: Int, t: Tree): Tree = {
require(redNodesHaveBlackChildren(t))
t match {
diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala
index 49e08b9da..33a4f7a32 100644
--- a/testcases/ListWithSize.scala
+++ b/testcases/ListWithSize.scala
@@ -87,14 +87,23 @@ object ListWithSize {
def nilAppend(l : List) : Boolean = (append(l, Nil()) == l) holds
// unclear if we needed this--it was meant to force folding
- def appendFold(x : Int, xs : List, ys : List) : Boolean = {
- true
- } ensuring (res => res && Cons(x,append(xs, ys)) == append(Cons(x,xs), ys))
+ //def appendFold(x : Int, xs : List, ys : List) : Boolean = {
+ // true
+ //} ensuring (res => res && Cons(x,append(xs, ys)) == append(Cons(x,xs), ys))
@induct
def appendAssoc(xs : List, ys : List, zs : List) : Boolean =
(append(append(xs, ys), zs) == append(xs, append(ys, zs))) holds
+ def revAuxBroken(l1 : List, e : Int, l2 : List) : Boolean = {
+ (append(reverse(l1), Cons(e,l2)) == reverse0(l1, l2))
+ } holds
+
+ @induct
+ def reverse0exposed(l1 : List, l2 : List) : Boolean = {
+ (reverse0(l1, l2) == append(reverse(l1), l2))
+ } holds
+
@induct
def sizeAppend(l1 : List, l2 : List) : Boolean =
(size(append(l1, l2)) == size(l1) + size(l2)) holds
@@ -115,8 +124,12 @@ object ListWithSize {
case Cons(x, xs) => concat0(xs, l2, Cons(x, l3))
}) ensuring(content(_) == content(l1) ++ content(l2) ++ content(l3))
+ def reverseConcat0(l1: List, l2: List) : Boolean = {
+ reverse(concat(l1, l2)) == concat(reverse(l2), reverse(l1))
+ } // holds
+
// proved with unrolling=2 ???
- def property1(l1: List, l2: List) : Boolean = {
+ def reverseConcat(l1: List, l2: List) : Boolean = {
reverse(concat(l1, l2)) == concat(reverse(l2), reverse(l1))
- } // ensuring(_ == true)
+ } // holds
}
--
GitLab