Skip to content
Snippets Groups Projects
Commit 3cd0ea59 authored by Viktor Kuncak's avatar Viktor Kuncak
Browse files

why CAV cannot find counterexample

parent 99fb25b5
No related branches found
No related tags found
No related merge requests found
...@@ -38,6 +38,7 @@ object RedBlackTree { ...@@ -38,6 +38,7 @@ object RedBlackTree {
case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r) case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
} }
// <<insert element x into the tree t>>
def ins(x: Int, t: Tree): Tree = { def ins(x: Int, t: Tree): Tree = {
require(redNodesHaveBlackChildren(t)) require(redNodesHaveBlackChildren(t))
t match { t match {
......
...@@ -87,14 +87,23 @@ object ListWithSize { ...@@ -87,14 +87,23 @@ object ListWithSize {
def nilAppend(l : List) : Boolean = (append(l, Nil()) == l) holds def nilAppend(l : List) : Boolean = (append(l, Nil()) == l) holds
// unclear if we needed this--it was meant to force folding // unclear if we needed this--it was meant to force folding
def appendFold(x : Int, xs : List, ys : List) : Boolean = { //def appendFold(x : Int, xs : List, ys : List) : Boolean = {
true // true
} ensuring (res => res && Cons(x,append(xs, ys)) == append(Cons(x,xs), ys)) //} ensuring (res => res && Cons(x,append(xs, ys)) == append(Cons(x,xs), ys))
@induct @induct
def appendAssoc(xs : List, ys : List, zs : List) : Boolean = def appendAssoc(xs : List, ys : List, zs : List) : Boolean =
(append(append(xs, ys), zs) == append(xs, append(ys, zs))) holds (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 @induct
def sizeAppend(l1 : List, l2 : List) : Boolean = def sizeAppend(l1 : List, l2 : List) : Boolean =
(size(append(l1, l2)) == size(l1) + size(l2)) holds (size(append(l1, l2)) == size(l1) + size(l2)) holds
...@@ -115,8 +124,12 @@ object ListWithSize { ...@@ -115,8 +124,12 @@ object ListWithSize {
case Cons(x, xs) => concat0(xs, l2, Cons(x, l3)) 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))
def reverseConcat0(l1: List, l2: List) : Boolean = {
reverse(concat(l1, l2)) == concat(reverse(l2), reverse(l1))
} // holds
// proved with unrolling=2 ??? // 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)) reverse(concat(l1, l2)) == concat(reverse(l2), reverse(l1))
} // ensuring(_ == true) } // holds
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment