From 0f5b3a4df864fc8bc6dbed40a09149ed1718c235 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Mon, 16 Mar 2015 21:44:39 +0100
Subject: [PATCH] Testcases for higher-order functions
---
.../higher-order/invalid/Continuations1.scala | 27 +++
.../higher-order/invalid/HOInvocations.scala | 16 ++
.../higher-order/invalid/Lists1.scala | 32 +++
.../higher-order/invalid/Map.scala | 20 ++
.../higher-order/invalid/ParBalance.scala | 133 +++++++++++
.../higher-order/invalid/PositiveMap.scala | 25 +++
.../higher-order/invalid/Sets1.scala | 16 ++
.../higher-order/valid/Anonymous.scala | 9 +
.../higher-order/valid/Closures.scala | 15 ++
.../higher-order/valid/Closures2.scala | 35 +++
.../higher-order/valid/FlatMap.scala | 48 ++++
.../higher-order/valid/FoldAssociative.scala | 101 +++++++++
.../higher-order/valid/HOInvocations.scala | 17 ++
.../higher-order/valid/Lambdas.scala | 15 ++
.../higher-order/valid/Lists1.scala | 30 +++
.../higher-order/valid/Lists2.scala | 49 +++++
.../higher-order/valid/Lists3.scala | 34 +++
.../higher-order/valid/Lists4.scala | 26 +++
.../higher-order/valid/Lists5.scala | 32 +++
.../higher-order/valid/Lists6.scala | 22 ++
.../higher-order/valid/Monads1.scala | 24 ++
.../higher-order/valid/Monads2.scala | 47 ++++
.../higher-order/valid/Monads3.scala | 77 +++++++
.../higher-order/valid/ParBalance.scala | 206 ++++++++++++++++++
.../higher-order/valid/PositiveMap.scala | 36 +++
.../higher-order/valid/Sets1.scala | 23 ++
.../higher-order/valid/Sets2.scala | 23 ++
.../higher-order/valid/Trees1.scala | 23 ++
28 files changed, 1161 insertions(+)
create mode 100644 testcases/verification/higher-order/invalid/Continuations1.scala
create mode 100644 testcases/verification/higher-order/invalid/HOInvocations.scala
create mode 100644 testcases/verification/higher-order/invalid/Lists1.scala
create mode 100644 testcases/verification/higher-order/invalid/Map.scala
create mode 100644 testcases/verification/higher-order/invalid/ParBalance.scala
create mode 100644 testcases/verification/higher-order/invalid/PositiveMap.scala
create mode 100644 testcases/verification/higher-order/invalid/Sets1.scala
create mode 100644 testcases/verification/higher-order/valid/Anonymous.scala
create mode 100644 testcases/verification/higher-order/valid/Closures.scala
create mode 100644 testcases/verification/higher-order/valid/Closures2.scala
create mode 100644 testcases/verification/higher-order/valid/FlatMap.scala
create mode 100644 testcases/verification/higher-order/valid/FoldAssociative.scala
create mode 100644 testcases/verification/higher-order/valid/HOInvocations.scala
create mode 100644 testcases/verification/higher-order/valid/Lambdas.scala
create mode 100644 testcases/verification/higher-order/valid/Lists1.scala
create mode 100644 testcases/verification/higher-order/valid/Lists2.scala
create mode 100644 testcases/verification/higher-order/valid/Lists3.scala
create mode 100644 testcases/verification/higher-order/valid/Lists4.scala
create mode 100644 testcases/verification/higher-order/valid/Lists5.scala
create mode 100644 testcases/verification/higher-order/valid/Lists6.scala
create mode 100644 testcases/verification/higher-order/valid/Monads1.scala
create mode 100644 testcases/verification/higher-order/valid/Monads2.scala
create mode 100644 testcases/verification/higher-order/valid/Monads3.scala
create mode 100644 testcases/verification/higher-order/valid/ParBalance.scala
create mode 100644 testcases/verification/higher-order/valid/PositiveMap.scala
create mode 100644 testcases/verification/higher-order/valid/Sets1.scala
create mode 100644 testcases/verification/higher-order/valid/Sets2.scala
create mode 100644 testcases/verification/higher-order/valid/Trees1.scala
diff --git a/testcases/verification/higher-order/invalid/Continuations1.scala b/testcases/verification/higher-order/invalid/Continuations1.scala
new file mode 100644
index 000000000..9511a8157
--- /dev/null
+++ b/testcases/verification/higher-order/invalid/Continuations1.scala
@@ -0,0 +1,27 @@
+import leon.lang._
+
+object Continuations1 {
+ def add_cps[T](x: BigInt, y: BigInt)(f: BigInt => T): T = {
+ f(x + y)
+ }
+
+ def square_cps[T](x: BigInt)(f: BigInt => T): T = {
+ f(x * x)
+ }
+
+ def pythagoras_cps[T](a: BigInt, b: BigInt)(f: BigInt => T): T = {
+ val a2 = square_cps(a)(x => x)
+ val b2 = square_cps(b)(x => x)
+ add_cps(a2, b2)(f)
+ }
+
+ def lemma1(a: BigInt, b: BigInt): Boolean = {
+ require(a > 0 && b > 0)
+ pythagoras_cps(a, b)(_ == a*a + b*b)
+ }.holds
+
+ def lemma2(a: BigInt, b: BigInt): Boolean = {
+ require(a > 0 && b > 0)
+ pythagoras_cps(a, b)(_ == a*a)
+ }.holds
+}
diff --git a/testcases/verification/higher-order/invalid/HOInvocations.scala b/testcases/verification/higher-order/invalid/HOInvocations.scala
new file mode 100644
index 000000000..3d2e16835
--- /dev/null
+++ b/testcases/verification/higher-order/invalid/HOInvocations.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object HOInvocations {
+ def switch(x: Int, f: (Int) => Int, g: (Int) => Int) = if(x > 0) f else g
+
+ def failling_1(f: (Int) => Int) = {
+ switch(-10, (x: Int) => x + 1, f)(2)
+ } ensuring { res => res > 0 }
+
+ def failling_2(x: Int, f: (Int) => Int, g: (Int) => Int) = {
+ require(x > 0)
+ switch(1, switch(x, f, g), g)(1)
+ } ensuring { res => res != f(1) }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/higher-order/invalid/Lists1.scala b/testcases/verification/higher-order/invalid/Lists1.scala
new file mode 100644
index 000000000..b84787c4e
--- /dev/null
+++ b/testcases/verification/higher-order/invalid/Lists1.scala
@@ -0,0 +1,32 @@
+import leon.lang._
+
+object Lists1 {
+ abstract class List[T]
+ case class Cons[T](head: T, tail: List[T]) extends List[T]
+ case class Nil[T]() extends List[T]
+
+ def forall[T](list: List[T], f: T => Boolean): Boolean = list match {
+ case Cons(head, tail) => f(head) && forall(tail, f)
+ case Nil() => true
+ }
+
+ def positive(list: List[Int]): Boolean = list match {
+ case Cons(head, tail) => if (head < 0) false else positive(tail)
+ case Nil() => true
+ }
+
+ def gt(i: Int): Int => Boolean = x => x > i
+
+ def positive_lemma(list: List[Int]): Boolean = {
+ positive(list) == forall(list, gt(0))
+ }
+
+ def failling_1(list: List[Int]): Boolean = {
+ list match {
+ case Nil() => positive_lemma(list)
+ case Cons(head, tail) => positive_lemma(list) && failling_1(tail)
+ }
+ }.holds
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/higher-order/invalid/Map.scala b/testcases/verification/higher-order/invalid/Map.scala
new file mode 100644
index 000000000..3179604ea
--- /dev/null
+++ b/testcases/verification/higher-order/invalid/Map.scala
@@ -0,0 +1,20 @@
+import leon.lang._
+import leon.collection._
+
+object Map {
+
+ def failure1[T](l: List[T], f: T => T): Boolean = {
+ l.map(f) == l.map(f).map(f)
+ }.holds
+
+ def failure2[T](l: List[T], f: T => T): Boolean = {
+ l.map(f) == (l match {
+ case Cons(head, tail) => Cons(head, tail.map(f))
+ case Nil() => Nil[T]()
+ })
+ }.holds
+
+ def failure3[T](l: List[T], f: T => List[T]): Boolean = {
+ l == l.flatMap(f)
+ }.holds
+}
diff --git a/testcases/verification/higher-order/invalid/ParBalance.scala b/testcases/verification/higher-order/invalid/ParBalance.scala
new file mode 100644
index 000000000..4a2a93c23
--- /dev/null
+++ b/testcases/verification/higher-order/invalid/ParBalance.scala
@@ -0,0 +1,133 @@
+import leon._
+import leon.lang._
+
+object ParBalance {
+
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class Option
+ case class Some(x: BigInt) extends Option
+ case class None() extends Option
+
+ val openPar : BigInt = BigInt(1)
+ val closePar : BigInt = BigInt(2)
+
+ def balanced(list: List, counter: BigInt): Boolean = {
+ if (counter < 0) false else list match {
+ case Cons(head, tail) =>
+ val c = if (head == openPar) counter + 1
+ else if (head == closePar) counter - 1
+ else counter
+ balanced(tail, c)
+ case Nil() => counter == 0
+ }
+ }
+
+ def balanced_nonEarly(list: List, counter: BigInt): Boolean = {
+ list match {
+ case Cons(head, tail) =>
+ if (counter < 0) balanced_nonEarly(tail, counter) else {
+ val c = if (head == openPar) counter + 1
+ else if (head == closePar) counter - 1
+ else counter
+ balanced_nonEarly(tail, c)
+ }
+ case Nil() => counter == 0
+ }
+ } ensuring { res => res == balanced(list, counter) }
+
+ def balanced_withFailure(list: List, counter: BigInt, failed: Boolean): Boolean = {
+ require(counter >= 0 || failed)
+ list match {
+ case Cons(head, tail) =>
+ val c = if (head == openPar) counter + 1
+ else if (head == closePar) counter - 1
+ else counter
+ balanced_withFailure(tail, c, failed || c < 0)
+ case Nil() => !failed && counter == 0
+ }
+ } ensuring { res =>
+ if (failed) {
+ res == balanced_nonEarly(list, -1)
+ } else {
+ res == balanced_nonEarly(list, counter)
+ }
+ }
+
+ def balanced_withReduce(list: List, p: (BigInt, BigInt)): Boolean = {
+ require(p._1 >= 0 && p._2 >= 0)
+ list match {
+ case Cons(head, tail) =>
+ val p2 = reduce(p, parPair(head))
+ balanced_withReduce(tail, p2)
+ case Nil() =>
+ p._1 == 0 && p._2 == 0
+ }
+ } ensuring { res => res == balanced_withFailure(list, p._1 - p._2, p._2 > 0) }
+
+ def balanced_foldLeft_equivalence(list: List, p: (BigInt, BigInt)): Boolean = {
+ require(p._1 >= 0 && p._2 >= 0)
+ val f = (s: (BigInt, BigInt), x: BigInt) => reduce(s, parPair(x))
+ (foldLeft(list, p, f) == (BigInt(0), BigInt(0))) == balanced_withReduce(list, p) && (list match {
+ case Cons(head, tail) =>
+ val p2 = f(p, head)
+ balanced_foldLeft_equivalence(tail, p2)
+ case Nil() => true
+ })
+ }.holds
+
+ def foldRight[A](list: List, state: A, f: (BigInt, A) => A): A = list match {
+ case Cons(head, tail) =>
+ val tailState = foldRight(tail, state, f)
+ f(head, tailState)
+ case Nil() => state
+ }
+
+ def foldLeft[A](list: List, state: A, f: (A, BigInt) => A): A = list match {
+ case Cons(head, tail) =>
+ val nextState = f(state, head)
+ foldLeft(tail, nextState, f)
+ case Nil() => state
+ }
+
+ def reduce(p1: (BigInt, BigInt), p2: (BigInt, BigInt)): (BigInt, BigInt) = {
+ if (p1._1 >= p2._2) {
+ (p1._1 - p2._2 + p2._1, p1._2)
+ } else {
+ (p2._1, p2._2 - p1._1 + p1._2)
+ }
+ }
+
+ def reduce_associative(p1: (BigInt, BigInt), p2: (BigInt, BigInt), p3: (BigInt, BigInt)): Boolean = {
+ reduce(p1, reduce(p2, p3)) == reduce(reduce(p1, p2), p3)
+ }.holds
+
+ def swap(p: (BigInt, BigInt)): (BigInt, BigInt) = (p._2, p._1)
+
+ def reduce_inverse(p1: (BigInt, BigInt), p2: (BigInt, BigInt)): Boolean = {
+ reduce(p1, p2) == swap(reduce(swap(p2), swap(p1)))
+ }.holds
+
+ def reduce_associative_inverse(p1: (BigInt, BigInt), p2: (BigInt, BigInt), p3: (BigInt, BigInt)): Boolean = {
+ reduce(p1, reduce(p2, p3)) == swap(reduce(reduce(swap(p3), swap(p2)), swap(p1)))
+ }.holds
+
+ def reduce_associative_inverse2(p1: (BigInt, BigInt), p2: (BigInt, BigInt), p3: (BigInt, BigInt)): Boolean = {
+ reduce(reduce(p1, p2), p3) == swap(reduce(swap(p3), reduce(swap(p2), swap(p1))))
+ }.holds
+
+ def parPair(x: BigInt): (BigInt, BigInt) = {
+ if (x == openPar) (1, 0) else if (x == closePar) (0, 1) else (0, 0)
+ }
+
+ def fold_equivalence(list: List): Boolean = {
+ val s = (BigInt(0), BigInt(0))
+ val fl = (s: (BigInt, BigInt), x: BigInt) => reduce(s, parPair(x))
+ val fr = (x: BigInt, s: (BigInt, BigInt)) => reduce(swap(parPair(x)), s)
+
+ foldLeft(list, s, fl) == swap(foldRight(list, swap(s), fr))
+ }.holds
+
+}
diff --git a/testcases/verification/higher-order/invalid/PositiveMap.scala b/testcases/verification/higher-order/invalid/PositiveMap.scala
new file mode 100644
index 000000000..fb1452f47
--- /dev/null
+++ b/testcases/verification/higher-order/invalid/PositiveMap.scala
@@ -0,0 +1,25 @@
+import leon.lang._
+
+object PositiveMap {
+
+ abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def positive(list: List): Boolean = list match {
+ case Cons(head, tail) => if (head < 0) false else positive(tail)
+ case Nil() => true
+ }
+
+ def positiveMap_failling_1(f: (Int) => Int, list: List): List = {
+ list match {
+ case Cons(head, tail) =>
+ val fh = f(head)
+ val nh = if (fh < -1) 0 else fh
+ Cons(nh, positiveMap_failling_1(f, tail))
+ case Nil() => Nil()
+ }
+ } ensuring { res => positive(res) }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/higher-order/invalid/Sets1.scala b/testcases/verification/higher-order/invalid/Sets1.scala
new file mode 100644
index 000000000..45545c356
--- /dev/null
+++ b/testcases/verification/higher-order/invalid/Sets1.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object Sets1 {
+ def set(i: Int): Int => Boolean = x => x == i
+
+ def complement(s: Int => Boolean): Int => Boolean = x => !s(x)
+
+ def union(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) || s2(x)
+
+ def intersection(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) && s2(x)
+
+ def failing(s1: Int => Boolean, s2: Int => Boolean): Boolean = {
+ complement(intersection(union(s1, s2), s1)) == s2
+ }.holds
+
+}
diff --git a/testcases/verification/higher-order/valid/Anonymous.scala b/testcases/verification/higher-order/valid/Anonymous.scala
new file mode 100644
index 000000000..d69b1f842
--- /dev/null
+++ b/testcases/verification/higher-order/valid/Anonymous.scala
@@ -0,0 +1,9 @@
+import leon.lang._
+
+object Anonymous {
+ def test(x: BigInt) = {
+ require(x > 0)
+ val i = (a: BigInt) => a + 1
+ i(x) + i(2)
+ } ensuring { res => res > 0 }
+}
diff --git a/testcases/verification/higher-order/valid/Closures.scala b/testcases/verification/higher-order/valid/Closures.scala
new file mode 100644
index 000000000..5e191cf81
--- /dev/null
+++ b/testcases/verification/higher-order/valid/Closures.scala
@@ -0,0 +1,15 @@
+import leon.lang._
+
+object Closures {
+ def addX(x: Int): Int => Int = {
+ (a: Int) => a + x
+ }
+
+ def test(x: Int): Boolean = {
+ val add1 = addX(1)
+ val add2 = addX(2)
+ add1(add2(1)) == 4
+ }.holds
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/higher-order/valid/Closures2.scala b/testcases/verification/higher-order/valid/Closures2.scala
new file mode 100644
index 000000000..b791965d1
--- /dev/null
+++ b/testcases/verification/higher-order/valid/Closures2.scala
@@ -0,0 +1,35 @@
+import leon.lang._
+
+object Closures2 {
+ def set(i: Int): Int => Boolean = x => x == i
+
+ def union(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) || s2(x)
+
+ def intersection(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) && s2(x)
+
+ def diff(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) && !s2(x)
+
+ def set123(): Int => Boolean = union(set(1), union(set(2), set(3)))
+
+ def test1(): Boolean = {
+ val s1 = set123()
+ val s2 = union(s1, set(4))
+ s2(1) && s2(2) && s2(3) && s2(4)
+ }.holds
+
+ def test2(): Boolean = {
+ val s1 = set123()
+ val s2 = intersection(s1, union(set(1), set(3)))
+ val s3 = diff(s1, s2)
+ s3(2) && !s3(1) && !s3(3)
+ }.holds
+
+ def test3(): Boolean = {
+ val s1 = set123()
+ val s2 = set123()
+ val s3 = union(s1, s2)
+ s3(1) && s3(2) && s3(3)
+ }.holds
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/higher-order/valid/FlatMap.scala b/testcases/verification/higher-order/valid/FlatMap.scala
new file mode 100644
index 000000000..56f8c47e8
--- /dev/null
+++ b/testcases/verification/higher-order/valid/FlatMap.scala
@@ -0,0 +1,48 @@
+import leon.lang._
+import leon.collection._
+
+object FlatMap {
+
+ def append[T](l1: List[T], l2: List[T]): List[T] = l1 match {
+ case Cons(head, tail) => Cons(head, append(tail, l2))
+ case Nil() => l2
+ }
+
+ def associative_append_lemma[T](l1: List[T], l2: List[T], l3: List[T]): Boolean = {
+ append(append(l1, l2), l3) == append(l1, append(l2, l3))
+ }
+
+ def associative_append_lemma_induct[T](l1: List[T], l2: List[T], l3: List[T]): Boolean = {
+ l1 match {
+ case Nil() => associative_append_lemma(l1, l2, l3)
+ case Cons(head, tail) => associative_append_lemma(l1, l2, l3) && associative_append_lemma_induct(tail, l2, l3)
+ }
+ }.holds
+
+ def flatMap[T,U](list: List[T], f: T => List[U]): List[U] = list match {
+ case Cons(head, tail) => append(f(head), flatMap(tail, f))
+ case Nil() => Nil()
+ }
+
+ def associative_lemma[T,U,V](list: List[T], f: T => List[U], g: U => List[V]): Boolean = {
+ flatMap(flatMap(list, f), g) == flatMap(list, (x: T) => flatMap(f(x), g))
+ }
+
+ def associative_lemma_induct[T,U,V](list: List[T], flist: List[U], glist: List[V], f: T => List[U], g: U => List[V]): Boolean = {
+ associative_lemma(list, f, g) &&
+ append(glist, flatMap(append(flist, flatMap(list, f)), g)) == append(append(glist, flatMap(flist, g)), flatMap(list, (x: T) => flatMap(f(x), g))) &&
+ (glist match {
+ case Cons(ghead, gtail) =>
+ associative_lemma_induct(list, flist, gtail, f, g)
+ case Nil() => flist match {
+ case Cons(fhead, ftail) =>
+ associative_lemma_induct(list, ftail, g(fhead), f, g)
+ case Nil() => list match {
+ case Cons(head, tail) => associative_lemma_induct(tail, f(head), Nil(), f, g)
+ case Nil() => true
+ }
+ }
+ })
+ }.holds
+
+}
diff --git a/testcases/verification/higher-order/valid/FoldAssociative.scala b/testcases/verification/higher-order/valid/FoldAssociative.scala
new file mode 100644
index 000000000..261d15c0f
--- /dev/null
+++ b/testcases/verification/higher-order/valid/FoldAssociative.scala
@@ -0,0 +1,101 @@
+import leon._
+import leon.lang._
+
+object FoldAssociative {
+
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class Option
+ case class Some(x: Int) extends Option
+ case class None() extends Option
+
+ def foldRight[A](list: List, state: A, f: (Int, A) => A): A = list match {
+ case Cons(head, tail) =>
+ val tailState = foldRight(tail, state, f)
+ f(head, tailState)
+ case Nil() => state
+ }
+
+ def take(list: List, count: Int): List = {
+ require(count >= 0)
+ list match {
+ case Cons(head, tail) if count > 0 => Cons(head, take(tail, count - 1))
+ case _ => Nil()
+ }
+ }
+
+ def drop(list: List, count: Int): List = {
+ require(count >= 0)
+ list match {
+ case Cons(head, tail) if count > 0 => drop(tail, count - 1)
+ case _ => list
+ }
+ }
+
+ def append(l1: List, l2: List): List = {
+ l1 match {
+ case Cons(head, tail) => Cons(head, append(tail, l2))
+ case Nil() => l2
+ }
+ }
+
+ def lemma_split(list: List, x: Int): Boolean = {
+ require(x >= 0)
+ val f = (x: Int, s: Int) => x + s
+ val l1 = take(list, x)
+ val l2 = drop(list, x)
+ foldRight(list, 0, f) == foldRight(l1, foldRight(l2, 0, f), f)
+ }
+
+ def lemma_split_induct(list: List, x: Int): Boolean = {
+ require(x >= 0)
+ val f = (x: Int, s: Int) => x + s
+ val l1 = take(list, x)
+ val l2 = drop(list, x)
+ lemma_split(list, x) && (list match {
+ case Cons(head, tail) if x > 0 =>
+ lemma_split_induct(tail, x - 1)
+ case _ => true
+ })
+ }.holds
+
+ def lemma_reassociative(list: List, x: Int): Boolean = {
+ require(x >= 0)
+ val f = (x: Int, s: Int) => x + s
+ val l1 = take(list, x)
+ val l2 = drop(list, x)
+
+ foldRight(list, 0, f) == foldRight(l1, 0, f) + foldRight(l2, 0, f)
+ }
+
+ def lemma_reassociative_induct(list: List, x: Int): Boolean = {
+ require(x >= 0)
+ val f = (x: Int, s: Int) => x + s
+ val l1 = take(list, x)
+ val l2 = drop(list, x)
+ lemma_reassociative(list, x) && (list match {
+ case Cons(head, tail) if x > 0 =>
+ lemma_reassociative_induct(tail, x - 1)
+ case _ => true
+ })
+ }.holds
+
+ def lemma_reassociative_presplit(l1: List, l2: List): Boolean = {
+ val f = (x: Int, s: Int) => x + s
+ val list = append(l1, l2)
+ foldRight(list, 0, f) == foldRight(l1, 0, f) + foldRight(l2, 0, f)
+ }
+
+ def lemma_reassociative_presplit_induct(l1: List, l2: List): Boolean = {
+ val f = (x: Int, s: Int) => x + s
+ val list = append(l1, l2)
+ lemma_reassociative_presplit(l1, l2) && (l1 match {
+ case Cons(head, tail) =>
+ lemma_reassociative_presplit_induct(tail, l2)
+ case Nil() => true
+ })
+ }.holds
+
+}
diff --git a/testcases/verification/higher-order/valid/HOInvocations.scala b/testcases/verification/higher-order/valid/HOInvocations.scala
new file mode 100644
index 000000000..0f2fbda2f
--- /dev/null
+++ b/testcases/verification/higher-order/valid/HOInvocations.scala
@@ -0,0 +1,17 @@
+import leon.lang._
+
+object HOInvocations {
+ def switch(x: Int, f: (Int) => Int, g: (Int) => Int) = if(x > 0) f else g
+
+ def passing_1(f: (Int) => Int) = {
+ switch(10, (x: Int) => x + 1, f)(2)
+ } ensuring { res => res > 0 }
+
+ def passing_2(x: Int, f: (Int) => Int, g: (Int) => Int) = {
+ require(x > 0)
+ switch(1, switch(x, f, g), g)(1)
+ } ensuring { res => res == f(1) }
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/higher-order/valid/Lambdas.scala b/testcases/verification/higher-order/valid/Lambdas.scala
new file mode 100644
index 000000000..36ae0c7ad
--- /dev/null
+++ b/testcases/verification/higher-order/valid/Lambdas.scala
@@ -0,0 +1,15 @@
+import leon.lang._
+
+object Lambdas {
+ def gen(x: Int): (Int) => Int = {
+ val f = (x: Int) => x + 1
+ val g = (x: Int) => x + 2
+ if (x > 0) g else f
+ }
+
+ def test(x: Int): Boolean = {
+ require(x > 0)
+ val f = gen(x)
+ f(x) == x + 2
+ }.holds
+}
diff --git a/testcases/verification/higher-order/valid/Lists1.scala b/testcases/verification/higher-order/valid/Lists1.scala
new file mode 100644
index 000000000..719c3d236
--- /dev/null
+++ b/testcases/verification/higher-order/valid/Lists1.scala
@@ -0,0 +1,30 @@
+import leon.lang._
+import leon.collection._
+import leon.annotation._
+
+object Lists1 {
+
+ def exists[T](list: List[T], f: T => Boolean): Boolean = list match {
+ case Cons(head, tail) => f(head) || exists(tail, f)
+ case Nil() => false
+ }
+
+ def forall[T](list: List[T], f: T => Boolean): Boolean = list match {
+ case Cons(head, tail) => f(head) && forall(tail, f)
+ case Nil() => true
+ }
+
+ def exists_lemma[T](list: List[T], f: T => Boolean): Boolean = {
+ exists(list, f) == !forall(list, (x: T) => !f(x))
+ }
+
+ def exists_lemma_induct[T](list: List[T], f: T => Boolean): Boolean = {
+ list match {
+ case Nil() => exists_lemma(list, f)
+ case Cons(head, tail) => exists_lemma(list, f) && exists_lemma_induct(tail, f)
+ }
+ }.holds
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/higher-order/valid/Lists2.scala b/testcases/verification/higher-order/valid/Lists2.scala
new file mode 100644
index 000000000..654046ba0
--- /dev/null
+++ b/testcases/verification/higher-order/valid/Lists2.scala
@@ -0,0 +1,49 @@
+import leon.lang._
+
+object Lists2 {
+ abstract class List[T]
+ case class Cons[T](head: T, tail: List[T]) extends List[T]
+ case class Nil[T]() extends List[T]
+
+ def forall[T](list: List[T], f: T => Boolean): Boolean = list match {
+ case Cons(head, tail) => f(head) && forall(tail, f)
+ case Nil() => true
+ }
+
+ def positive(list: List[Int]): Boolean = list match {
+ case Cons(head, tail) => if (head < 0) false else positive(tail)
+ case Nil() => true
+ }
+
+ def positive_lemma(list: List[Int]): Boolean = {
+ positive(list) == forall(list, (x: Int) => x >= 0)
+ }
+
+ def positive_lemma_induct(list: List[Int]): Boolean = {
+ list match {
+ case Nil() => positive_lemma(list)
+ case Cons(head, tail) => positive_lemma(list) && positive_lemma_induct(tail)
+ }
+ }.holds
+
+ def remove[T](list: List[T], e: T) : List[T] = {
+ list match {
+ case Nil() => Nil()
+ case Cons(x, xs) if x == e => remove(xs, e)
+ case Cons(x, xs) => Cons(x, remove(xs, e))
+ }
+ } //ensuring { (res: List[T]) => forall(res, (x : T) => x != e) }
+
+ def remove_lemma[T](list: List[T], e: T): Boolean = {
+ forall(remove(list, e), (x : T) => x != e)
+ }
+
+ def remove_lemma_induct[T](list: List[T], e: T): Boolean = {
+ list match {
+ case Nil() => remove_lemma(list, e)
+ case Cons(head, tail) => remove_lemma(list, e) && remove_lemma_induct(tail, e)
+ }
+ }.holds
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/higher-order/valid/Lists3.scala b/testcases/verification/higher-order/valid/Lists3.scala
new file mode 100644
index 000000000..67060133a
--- /dev/null
+++ b/testcases/verification/higher-order/valid/Lists3.scala
@@ -0,0 +1,34 @@
+import leon.lang._
+
+object Lists3 {
+ abstract class List[T]
+ case class Cons[T](head: T, tail: List[T]) extends List[T]
+ case class Nil[T]() extends List[T]
+
+ def forall[T](list: List[T], f: T => Boolean): Boolean = list match {
+ case Cons(head, tail) => f(head) && forall(tail, f)
+ case Nil() => true
+ }
+
+ def positive(list: List[Int]): Boolean = list match {
+ case Cons(head, tail) => if (head < 0) false else positive(tail)
+ case Nil() => true
+ }
+
+ def gt(i: Int): Int => Boolean = x => x > i
+
+ def gte(i: Int): Int => Boolean = x => gt(i)(x) || x == i
+
+ def positive_lemma(list: List[Int]): Boolean = {
+ positive(list) == forall(list, gte(0))
+ }
+
+ def positive_lemma_induct(list: List[Int]): Boolean = {
+ list match {
+ case Nil() => positive_lemma(list)
+ case Cons(head, tail) => positive_lemma(list) && positive_lemma_induct(tail)
+ }
+ }.holds
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/higher-order/valid/Lists4.scala b/testcases/verification/higher-order/valid/Lists4.scala
new file mode 100644
index 000000000..02c24111d
--- /dev/null
+++ b/testcases/verification/higher-order/valid/Lists4.scala
@@ -0,0 +1,26 @@
+import leon.lang._
+
+object Lists4 {
+ abstract class List[T]
+ case class Cons[T](head: T, tail: List[T]) extends List[T]
+ case class Nil[T]() extends List[T]
+
+ def map[F,T](list: List[F], f: F => T): List[T] = list match {
+ case Cons(head, tail) => Cons(f(head), map(tail, f))
+ case Nil() => Nil()
+ }
+
+ def map_lemma[A,B,C](list: List[A], f: A => B, g: B => C): Boolean = {
+ map(list, (x: A) => g(f(x))) == map(map(list, f), g)
+ }
+
+ def map_lemma_induct[D,E,F](list: List[D], f: D => E, g: E => F): Boolean = {
+ list match {
+ case Nil() => map_lemma(list, f, g)
+ case Cons(head, tail) => map_lemma(list, f, g) && map_lemma_induct(tail, f, g)
+ }
+ }.holds
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/higher-order/valid/Lists5.scala b/testcases/verification/higher-order/valid/Lists5.scala
new file mode 100644
index 000000000..51ff810c6
--- /dev/null
+++ b/testcases/verification/higher-order/valid/Lists5.scala
@@ -0,0 +1,32 @@
+import leon.lang._
+import leon.collection._
+
+object Lists5 {
+ abstract class Option[T]
+ case class Some[T](value: T) extends Option[T]
+ case class None[T]() extends Option[T]
+
+ def find[T](f: T => Boolean, list: List[T]): Option[T] = list match {
+ case Cons(head, tail) => if (f(head)) Some(head) else find(f, tail)
+ case Nil() => None()
+ }
+
+ def exists[T](f: T => Boolean, list: List[T]): Boolean = list match {
+ case Cons(head, tail) => f(head) || exists(f, tail)
+ case Nil() => false
+ }
+
+ def equivalence_lemma[T](f: T => Boolean, list: List[T]): Boolean = {
+ find(f, list) match {
+ case Some(e) => exists(f, list)
+ case None() => !exists(f, list)
+ }
+ }
+
+ def equivalence_lemma_induct[T](f: T => Boolean, list: List[T]): Boolean = {
+ list match {
+ case Cons(head, tail) => equivalence_lemma(f, list) && equivalence_lemma_induct(f, tail)
+ case Nil() => equivalence_lemma(f, list)
+ }
+ }.holds
+}
diff --git a/testcases/verification/higher-order/valid/Lists6.scala b/testcases/verification/higher-order/valid/Lists6.scala
new file mode 100644
index 000000000..f70d523c7
--- /dev/null
+++ b/testcases/verification/higher-order/valid/Lists6.scala
@@ -0,0 +1,22 @@
+import leon.lang._
+import leon.collection._
+
+object Lists6 {
+ def exists[T](list: List[T], f: T => Boolean): Boolean = {
+ list match {
+ case Cons(head, tail) => f(head) || exists(tail, f)
+ case Nil() => false
+ }
+ }
+
+ def associative_lemma[T](list: List[T], f: T => Boolean, g: T => Boolean): Boolean = {
+ exists(list, (x: T) => f(x) || g(x)) == (exists(list, f) || exists(list, g))
+ }
+
+ def associative_lemma_induct[T](list: List[T], f: T => Boolean, g: T => Boolean): Boolean = {
+ associative_lemma(list, f, g) && (list match {
+ case Cons(head, tail) => associative_lemma_induct(tail, f, g)
+ case Nil() => true
+ })
+ }.holds
+}
diff --git a/testcases/verification/higher-order/valid/Monads1.scala b/testcases/verification/higher-order/valid/Monads1.scala
new file mode 100644
index 000000000..da9cd6cec
--- /dev/null
+++ b/testcases/verification/higher-order/valid/Monads1.scala
@@ -0,0 +1,24 @@
+import leon.lang._
+
+object Monads1 {
+ abstract class Try[T]
+ case class Success[T](value: T) extends Try[T]
+ case class Failure[T](error: Int) extends Try[T]
+
+ def flatMap[T,U](t: Try[T], f: T => Try[U]): Try[U] = t match {
+ case Success(value) => f(value)
+ case fail @ Failure(error) => Failure(error)
+ }
+
+ def associative_law[T,U,V](t: Try[T], f: T => Try[U], g: U => Try[V]): Boolean = {
+ flatMap(flatMap(t, f), g) == flatMap(t, (x: T) => flatMap(f(x), g))
+ }.holds
+
+ def left_unit_law[T,U](x: T, f: T => Try[U]): Boolean = {
+ flatMap(Success(x), f) == f(x)
+ }.holds
+
+ def right_unit_law[T,U](t: Try[T]): Boolean = {
+ flatMap(t, (x: T) => Success(x)) == t
+ }.holds
+}
diff --git a/testcases/verification/higher-order/valid/Monads2.scala b/testcases/verification/higher-order/valid/Monads2.scala
new file mode 100644
index 000000000..f89b2b7f7
--- /dev/null
+++ b/testcases/verification/higher-order/valid/Monads2.scala
@@ -0,0 +1,47 @@
+import leon.lang._
+
+object Monads2 {
+ abstract class Option[T]
+ case class Some[T](t: T) extends Option[T]
+ case class None[T]() extends Option[T]
+
+ def flatMap[T,U](opt: Option[T], f: T => Option[U]): Option[U] = opt match {
+ case Some(x) => f(x)
+ case None() => None()
+ }
+
+ def add[T](o1: Option[T], o2: Option[T]): Option[T] = o1 match {
+ case Some(x) => o1
+ case None() => o2
+ }
+
+ def associative_law[T,U,V](opt: Option[T], f: T => Option[U], g: U => Option[V]): Boolean = {
+ flatMap(flatMap(opt, f), g) == flatMap(opt, (x: T) => flatMap(f(x), g))
+ }.holds
+
+ def left_unit_law[T,U](x: T, f: T => Option[U]): Boolean = {
+ flatMap(Some(x), f) == f(x)
+ }.holds
+
+ def right_unit_law[T,U](opt: Option[T]): Boolean = {
+ flatMap(opt, (x: T) => Some(x)) == opt
+ }.holds
+
+ def flatMap_zero_law[T,U](none: None[T], f: T => Option[U]): Boolean = {
+ flatMap(none, f) == None[U]()
+ }.holds
+
+ def flatMap_to_zero_law[T,U](opt: Option[T]): Boolean = {
+ flatMap(opt, (x: T) => None[U]()) == None[U]()
+ }.holds
+
+ def add_zero_law[T](opt: Option[T]): Boolean = {
+ add(opt, None[T]()) == opt
+ }.holds
+
+ def zero_add_law[T](opt: Option[T]): Boolean = {
+ add(None[T](), opt) == opt
+ }.holds
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/higher-order/valid/Monads3.scala b/testcases/verification/higher-order/valid/Monads3.scala
new file mode 100644
index 000000000..a2911c987
--- /dev/null
+++ b/testcases/verification/higher-order/valid/Monads3.scala
@@ -0,0 +1,77 @@
+import leon.lang._
+import leon.collection._
+
+object FlatMap {
+
+ def append[T](l1: List[T], l2: List[T]): List[T] = {
+ l1 match {
+ case Cons(head, tail) => Cons(head, append(tail, l2))
+ case Nil() => l2
+ }
+ } ensuring { res => (res == l1) || (l2 != Nil[T]()) }
+
+ def flatMap[T,U](list: List[T], f: T => List[U]): List[U] = list match {
+ case Cons(head, tail) => append(f(head), flatMap(tail, f))
+ case Nil() => Nil()
+ }
+
+ def associative_lemma[T,U,V](list: List[T], f: T => List[U], g: U => List[V]): Boolean = {
+ flatMap(flatMap(list, f), g) == flatMap(list, (x: T) => flatMap(f(x), g))
+ }
+
+ def associative_lemma_induct[T,U,V](list: List[T], flist: List[U], glist: List[V], f: T => List[U], g: U => List[V]): Boolean = {
+ associative_lemma(list, f, g) &&
+ append(glist, flatMap(append(flist, flatMap(list, f)), g)) == append(append(glist, flatMap(flist, g)), flatMap(list, (x: T) => flatMap(f(x), g))) &&
+ (glist match {
+ case Cons(ghead, gtail) =>
+ associative_lemma_induct(list, flist, gtail, f, g)
+ case Nil() => flist match {
+ case Cons(fhead, ftail) =>
+ associative_lemma_induct(list, ftail, g(fhead), f, g)
+ case Nil() => list match {
+ case Cons(head, tail) => associative_lemma_induct(tail, f(head), Nil(), f, g)
+ case Nil() => true
+ }
+ }
+ })
+ }.holds
+
+ def left_unit_law[T,U](x: T, f: T => List[U]): Boolean = {
+ flatMap(Cons(x, Nil()), f) == f(x)
+ }.holds
+
+ def right_unit_law[T](list: List[T]): Boolean = {
+ flatMap(list, (x: T) => Cons(x, Nil())) == list
+ }
+
+ def right_unit_induct[T,U](list: List[T]): Boolean = {
+ right_unit_law(list) && (list match {
+ case Cons(head, tail) => right_unit_induct(tail)
+ case Nil() => true
+ })
+ }.holds
+
+ def flatMap_zero_law[T,U](f: T => List[U]): Boolean = {
+ flatMap(Nil[T](), f) == Nil[U]()
+ }.holds
+
+ def flatMap_to_zero_law[T](list: List[T]): Boolean = {
+ flatMap(list, (x: T) => Nil[T]()) == Nil[T]()
+ }
+
+ def flatMap_to_zero_induct[T,U](list: List[T]): Boolean = {
+ flatMap_to_zero_law(list) && (list match {
+ case Cons(head, tail) => flatMap_to_zero_induct(tail)
+ case Nil() => true
+ })
+ }.holds
+
+ def add_zero_law[T](list: List[T]): Boolean = {
+ append(list, Nil()) == list
+ }.holds
+
+ def zero_add_law[T](list: List[T]): Boolean = {
+ append(Nil(), list) == list
+ }.holds
+
+}
diff --git a/testcases/verification/higher-order/valid/ParBalance.scala b/testcases/verification/higher-order/valid/ParBalance.scala
new file mode 100644
index 000000000..6943d3268
--- /dev/null
+++ b/testcases/verification/higher-order/valid/ParBalance.scala
@@ -0,0 +1,206 @@
+import leon._
+import leon.lang._
+
+object ParBalance {
+
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class Option
+ case class Some(x: BigInt) extends Option
+ case class None() extends Option
+
+ val openPar : BigInt = BigInt(1)
+ val closePar : BigInt = BigInt(2)
+
+ def balanced(list: List, counter: BigInt): Boolean = {
+ if (counter < 0) false else list match {
+ case Cons(head, tail) =>
+ val c = if (head == openPar) counter + 1
+ else if (head == closePar) counter - 1
+ else counter
+ balanced(tail, c)
+ case Nil() => counter == 0
+ }
+ }
+
+ def balanced_nonEarly(list: List, counter: BigInt): Boolean = {
+ list match {
+ case Cons(head, tail) =>
+ if (counter < 0) balanced_nonEarly(tail, counter) else {
+ val c = if (head == openPar) counter + 1
+ else if (head == closePar) counter - 1
+ else counter
+ balanced_nonEarly(tail, c)
+ }
+ case Nil() => counter == 0
+ }
+ } ensuring { res => res == balanced(list, counter) }
+
+ def balanced_withFailure(list: List, counter: BigInt, failed: Boolean): Boolean = {
+ require(counter >= 0 || failed)
+ list match {
+ case Cons(head, tail) =>
+ val c = if (head == openPar) counter + 1
+ else if (head == closePar) counter - 1
+ else counter
+ balanced_withFailure(tail, c, failed || c < 0)
+ case Nil() => !failed && counter == 0
+ }
+ } ensuring { res =>
+ if (failed) {
+ res == balanced_nonEarly(list, -1)
+ } else {
+ res == balanced_nonEarly(list, counter)
+ }
+ }
+
+ def balanced_withReduce(list: List, p: (BigInt, BigInt)): Boolean = {
+ require(p._1 >= 0 && p._2 >= 0)
+ list match {
+ case Cons(head, tail) =>
+ val p2 = reduce(p, parPair(head))
+ balanced_withReduce(tail, p2)
+ case Nil() =>
+ p._1 == 0 && p._2 == 0
+ }
+ } ensuring { res => res == balanced_withFailure(list, p._1 - p._2, p._2 > 0) }
+
+ def balanced_foldLeft_equivalence(list: List, p: (BigInt, BigInt)): Boolean = {
+ require(p._1 >= 0 && p._2 >= 0)
+ val f = (s: (BigInt, BigInt), x: BigInt) => reduce(s, parPair(x))
+ (foldLeft(list, p, f) == (BigInt(0), BigInt(0))) == balanced_withReduce(list, p) && (list match {
+ case Cons(head, tail) =>
+ val p2 = f(p, head)
+ balanced_foldLeft_equivalence(tail, p2)
+ case Nil() => true
+ })
+ }.holds
+
+ def foldRight[A](list: List, state: A, f: (BigInt, A) => A): A = list match {
+ case Cons(head, tail) =>
+ val tailState = foldRight(tail, state, f)
+ f(head, tailState)
+ case Nil() => state
+ }
+
+ def foldLeft[A](list: List, state: A, f: (A, BigInt) => A): A = list match {
+ case Cons(head, tail) =>
+ val nextState = f(state, head)
+ foldLeft(tail, nextState, f)
+ case Nil() => state
+ }
+
+ def reduce(p1: (BigInt, BigInt), p2: (BigInt, BigInt)): (BigInt, BigInt) = {
+ if (p1._1 >= p2._2) {
+ (p1._1 - p2._2 + p2._1, p1._2)
+ } else {
+ (p2._1, p2._2 - p1._1 + p1._2)
+ }
+ }
+
+ def reduce_associative(p1: (BigInt, BigInt), p2: (BigInt, BigInt), p3: (BigInt, BigInt)): Boolean = {
+ reduce(p1, reduce(p2, p3)) == reduce(reduce(p1, p2), p3)
+ }.holds
+
+ def swap(p: (BigInt, BigInt)): (BigInt, BigInt) = (p._2, p._1)
+
+ def reduce_inverse(p1: (BigInt, BigInt), p2: (BigInt, BigInt)): Boolean = {
+ reduce(p1, p2) == swap(reduce(swap(p2), swap(p1)))
+ }.holds
+
+ def reduce_associative_inverse(p1: (BigInt, BigInt), p2: (BigInt, BigInt), p3: (BigInt, BigInt)): Boolean = {
+ reduce(p1, reduce(p2, p3)) == swap(reduce(reduce(swap(p3), swap(p2)), swap(p1)))
+ }.holds
+
+ def reduce_associative_inverse2(p1: (BigInt, BigInt), p2: (BigInt, BigInt), p3: (BigInt, BigInt)): Boolean = {
+ reduce(reduce(p1, p2), p3) == swap(reduce(swap(p3), reduce(swap(p2), swap(p1))))
+ }.holds
+
+ def parPair(x: BigInt): (BigInt, BigInt) = {
+ if (x == openPar) (1, 0) else if (x == closePar) (0, 1) else (0, 0)
+ }
+
+ def headOption(list: List): Option = list match {
+ case Cons(head, tail) => Some(head)
+ case Nil() => None()
+ }
+
+ def lastOption(list: List): Option = list match {
+ case Cons(head, Nil()) => Some(head)
+ case Cons(head, tail) => lastOption(tail)
+ case Nil() => None()
+ }
+
+ def init(list: List): List = list match {
+ case Cons(head, Nil()) => Nil()
+ case Cons(head, tail) => Cons(head, init(tail))
+ case Nil() => Nil()
+ }
+
+ def tail(list: List): List = list match {
+ case Cons(head, tail) => tail
+ case Nil() => Nil()
+ }
+
+ def addLast(list: List, x: BigInt): List = {
+ list match {
+ case Cons(head, tail) => Cons(head, addLast(tail, x))
+ case Nil() => Cons(x, Nil())
+ }
+ } ensuring { res => lastOption(res) == Some(x) && init(res) == list }
+
+ def reverse(list: List): List = {
+ list match {
+ case Cons(head, tail) => addLast(reverse(tail), head)
+ case Nil() => Nil()
+ }
+ } ensuring { res =>
+ lastOption(res) == headOption(list) &&
+ lastOption(list) == headOption(res)
+ }
+
+ def reverse_tail_equivalence(list: List): Boolean = {
+ reverse(tail(list)) == init(reverse(list))
+ }.holds
+
+ def reverse_init_equivalence(list: List): Boolean = {
+ reverse(init(list)) == tail(reverse(list)) && (list match {
+ case Cons(head, tail) => reverse_init_equivalence(tail)
+ case Nil() => true
+ })
+ }.holds
+
+ def reverse_equality_equivalence(l1: List, l2: List): Boolean = {
+ (l1 == l2) == (reverse(l1) == reverse(l2)) && ((l1, l2) match {
+ case (Cons(h1, t1), Cons(h2, t2)) => reverse_equality_equivalence(t1, t2)
+ case _ => true
+ })
+ }.holds
+
+ def reverse_reverse_equivalence(list: List): Boolean = {
+ reverse(reverse(list)) == list && ((list, reverse(list)) match {
+ case (Cons(h1, t1), Cons(h2, t2)) =>
+ reverse_reverse_equivalence(t1) && reverse_reverse_equivalence(t2)
+ case _ => true
+ })
+ }.holds
+
+ /*
+ def fold_equivalence(list: List): Boolean = {
+ val s = (0, 0)
+ val fl = (s: (BigInt, BigInt), x: BigInt) => reduce(s, parPair(x))
+ val fr = (x: BigInt, s: (BigInt, BigInt)) => reduce(parPair(x), s)
+
+ foldLeft(list, s, fl) == foldRight(list, s, fr)
+ }.holds
+
+ def lemma(list: List): Boolean = {
+ val f = (x: BigInt, s: (BigInt, BigInt)) => reduce(parPair(x), s)
+ fold_equivalence(list) && balanced_foldLeft_equivalence(list, (0, 0)) &&
+ (foldRight(list, (0, 0), f) == (0, 0)) == balanced(list, 0)
+ }.holds
+ */
+
+}
diff --git a/testcases/verification/higher-order/valid/PositiveMap.scala b/testcases/verification/higher-order/valid/PositiveMap.scala
new file mode 100644
index 000000000..0441ec26c
--- /dev/null
+++ b/testcases/verification/higher-order/valid/PositiveMap.scala
@@ -0,0 +1,36 @@
+import leon.lang._
+
+object PositiveMap {
+
+ abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case class Nil() extends List
+
+ def positive(list: List): Boolean = list match {
+ case Cons(head, tail) => if (head < 0) false else positive(tail)
+ case Nil() => true
+ }
+
+ def positiveMap_passing_1(f: (BigInt) => BigInt, list: List): List = {
+ list match {
+ case Cons(head, tail) =>
+ val fh = f(head)
+ val nh = if (fh <= 0) -fh else fh
+ Cons(nh, positiveMap_passing_1(f, tail))
+ case Nil() => Nil()
+ }
+ } ensuring { res => positive(res) }
+
+ def positiveMap_passing_2(f: (BigInt) => BigInt, list: List): List = {
+ list match {
+ case Cons(head, tail) =>
+ val fh = f(head)
+ val nh = if (fh < 0) -fh else fh
+ Cons(nh, positiveMap_passing_2(f, tail))
+ case Nil() => Nil()
+ }
+ } ensuring { res => positive(res) }
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/testcases/verification/higher-order/valid/Sets1.scala b/testcases/verification/higher-order/valid/Sets1.scala
new file mode 100644
index 000000000..4cfca4890
--- /dev/null
+++ b/testcases/verification/higher-order/valid/Sets1.scala
@@ -0,0 +1,23 @@
+import leon.lang._
+
+object Sets1 {
+ def set(i: Int): Int => Boolean = x => x == i
+
+ def complement(s: Int => Boolean): Int => Boolean = x => !s(x)
+
+ def union(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) || s2(x)
+
+ def intersection(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) && s2(x)
+
+ def de_morgan_1(s1: Int => Boolean, s2: Int => Boolean, x: Int): Boolean = {
+ val u1 = union(s1, s2)
+ val u2 = complement(intersection(complement(s1), complement(s2)))
+ u1(x) == u2(x)
+ }.holds
+
+ def de_morgan_2(s1: Int => Boolean, s2: Int => Boolean, x: Int): Boolean = {
+ val u1 = intersection(s1, s2)
+ val u2 = complement(union(complement(s1), complement(s2)))
+ u1(x) == u2(x)
+ }.holds
+}
diff --git a/testcases/verification/higher-order/valid/Sets2.scala b/testcases/verification/higher-order/valid/Sets2.scala
new file mode 100644
index 000000000..f25449028
--- /dev/null
+++ b/testcases/verification/higher-order/valid/Sets2.scala
@@ -0,0 +1,23 @@
+import leon.lang._
+
+object Sets1 {
+ def set(i: Int): Int => Boolean = x => x == i
+
+ def complement(s: Int => Boolean): Int => Boolean = x => !s(x)
+
+ def union(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) || s2(x)
+
+ def intersection(s1: Int => Boolean, s2: Int => Boolean): Int => Boolean = x => s1(x) && s2(x)
+
+ def union_associativity(sa1: Int => Boolean, sa2: Int => Boolean, sa3: Int => Boolean, x: Int): Boolean = {
+ val u1 = union(union(sa1, sa2), sa3)
+ val u2 = union(sa1, union(sa2, sa3))
+ u1(x) == u2(x)
+ }.holds
+
+ def intersection_associativity(sa1: Int => Boolean, sa2: Int => Boolean, sa3: Int => Boolean, x: Int): Boolean = {
+ val u1 = intersection(intersection(sa1, sa2), sa3)
+ val u2 = intersection(sa1, intersection(sa2, sa3))
+ u1(x) == u2(x)
+ }.holds
+}
diff --git a/testcases/verification/higher-order/valid/Trees1.scala b/testcases/verification/higher-order/valid/Trees1.scala
new file mode 100644
index 000000000..4c01ae06e
--- /dev/null
+++ b/testcases/verification/higher-order/valid/Trees1.scala
@@ -0,0 +1,23 @@
+import leon.lang._
+
+object Trees1 {
+ abstract class Tree[T]
+ case class Node[T](left: Tree[T], right: Tree[T]) extends Tree[T]
+ case class Leaf[T](value: T) extends Tree[T]
+
+ def map[T,U](tree: Tree[T], f: T => U): Tree[U] = tree match {
+ case Node(left, right) => Node(map(left, f), map(right, f))
+ case Leaf(value) => Leaf(f(value))
+ }
+
+ def associative_lemma[T,U,V](tree: Tree[T], f: T => U, g: U => V): Boolean = {
+ map(map(tree, f), g) == map(tree, (x: T) => g(f(x)))
+ }
+
+ def associative_lemma_induct[T,U,V](tree: Tree[T], f: T => U, g: U => V): Boolean = {
+ tree match {
+ case Node(left, right) => associative_lemma_induct(left, f, g) && associative_lemma_induct(right, f, g) && associative_lemma(tree, f, g)
+ case Leaf(value) => associative_lemma(tree, f, g)
+ }
+ }.holds
+}
--
GitLab