From ee367ec714b40d817c07962195638328ad080ebd Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Mon, 25 May 2015 17:20:45 +0200
Subject: [PATCH] Improve/add/correct testcases for new solvers
---
.../invalid/AddingNegativeNumbers.scala | 12 ++
.../invalid/AddingPositiveNumbers.scala | 11 ++
.../newsolvers/invalid/Array1.scala | 11 ++
.../newsolvers/invalid/Array2.scala | 12 ++
.../newsolvers/invalid/Array3.scala | 14 ++
.../newsolvers/invalid/Array4.scala | 12 ++
.../newsolvers/invalid/Asserts1.scala | 26 +++
.../newsolvers/invalid/BVDivision.scala | 11 ++
.../newsolvers/invalid/BVDivision2.scala | 11 ++
.../newsolvers/invalid/BigArray.scala | 13 ++
.../newsolvers/invalid/Division.scala | 11 ++
.../newsolvers/invalid/EnsuringBoolean.scala | 12 ++
.../newsolvers/invalid/FiniteSort.scala | 56 ++++++
.../newsolvers/invalid/Generics.scala | 15 ++
.../newsolvers/invalid/Generics2.scala | 25 +++
.../newsolvers/invalid/InsertionSort.scala | 43 +++++
.../newsolvers/invalid/ListOperations.scala | 108 +++++++++++
.../newsolvers/invalid/MyTuple1.scala | 13 ++
.../newsolvers/invalid/MyTuple2.scala | 16 ++
.../newsolvers/invalid/MyTuple3.scala | 9 +
.../newsolvers/invalid/PositiveMap.scala | 27 +++
.../invalid/PropositionalLogic.scala | 87 +++++++++
.../verification/newsolvers/invalid/README | 2 +
.../newsolvers/invalid/RedBlackTree.scala | 103 ++++++++++
.../newsolvers/invalid/Unit1.scala | 9 +
.../newsolvers/valid/AmortizedQueue.scala | 20 +-
.../newsolvers/valid/FiniteSort.scala | 8 +-
.../verification/newsolvers/valid/Heap.scala | 18 +-
.../newsolvers/valid/InsertionSort.scala | 8 +-
.../newsolvers/valid/ListOperations.scala | 176 ++++++++----------
.../newsolvers/valid/MergeSort.scala | 10 +-
.../newsolvers/valid/SearchLinkedList.scala | 4 +-
.../newsolvers/valid/Subtyping1.scala | 16 +-
33 files changed, 790 insertions(+), 139 deletions(-)
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/AddingNegativeNumbers.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/AddingPositiveNumbers.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/Array1.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/Array2.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/Array3.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/Array4.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/Asserts1.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/BVDivision.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/BVDivision2.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/BigArray.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/Division.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/EnsuringBoolean.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/FiniteSort.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/Generics.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/Generics2.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/InsertionSort.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/ListOperations.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/MyTuple1.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/MyTuple2.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/MyTuple3.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/PositiveMap.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/PropositionalLogic.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/README
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/RedBlackTree.scala
create mode 100644 src/test/resources/regression/verification/newsolvers/invalid/Unit1.scala
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/AddingNegativeNumbers.scala b/src/test/resources/regression/verification/newsolvers/invalid/AddingNegativeNumbers.scala
new file mode 100644
index 000000000..897aceefa
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/AddingNegativeNumbers.scala
@@ -0,0 +1,12 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+package test.resources.regression.verification.purescala.invalid
+
+object AddingNegativeNumbers {
+
+ def additionOverflow(x: Int, y: Int): Int = {
+ require(x <= 0 && y <= 0)
+ x + y
+ } ensuring(_ <= 0)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/AddingPositiveNumbers.scala b/src/test/resources/regression/verification/newsolvers/invalid/AddingPositiveNumbers.scala
new file mode 100644
index 000000000..fa89830c4
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/AddingPositiveNumbers.scala
@@ -0,0 +1,11 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object AddingPositiveNumbers {
+
+ //this should overflow with bit vectors
+ def additionOverflow(x: Int, y: Int): Int = {
+ require(x >= 0 && y >= 0)
+ x + y
+ } ensuring(_ >= 0)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/Array1.scala b/src/test/resources/regression/verification/newsolvers/invalid/Array1.scala
new file mode 100644
index 000000000..a7e3fea8e
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/Array1.scala
@@ -0,0 +1,11 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+
+object Array1 {
+
+ def foo(a: Array[Int]): Int = {
+ a(2)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/Array2.scala b/src/test/resources/regression/verification/newsolvers/invalid/Array2.scala
new file mode 100644
index 000000000..3996f1fb7
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/Array2.scala
@@ -0,0 +1,12 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+
+object Array2 {
+
+ def foo(a: Array[Int]): Int = {
+ require(a.length > 2)
+ a(2)
+ } ensuring(_ == 0)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/Array3.scala b/src/test/resources/regression/verification/newsolvers/invalid/Array3.scala
new file mode 100644
index 000000000..f5c75c538
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/Array3.scala
@@ -0,0 +1,14 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+
+object Array3 {
+ def find(c: Array[Int], i: Int): Int = {
+ require(i >= 0)
+ if(c(i) == i)
+ 42
+ else
+ 12
+ } ensuring(_ > 0)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/Array4.scala b/src/test/resources/regression/verification/newsolvers/invalid/Array4.scala
new file mode 100644
index 000000000..4e630cd42
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/Array4.scala
@@ -0,0 +1,12 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ val tmp = a.updated(0, 0)
+ 42
+ }
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/Asserts1.scala b/src/test/resources/regression/verification/newsolvers/invalid/Asserts1.scala
new file mode 100644
index 000000000..4375995d5
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/Asserts1.scala
@@ -0,0 +1,26 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+import leon.annotation._
+import leon._
+
+object Asserts1 {
+
+ def foo(a: BigInt): BigInt = {
+ require(a > 0)
+ val b = a
+ assert(b > 0, "Hey now")
+ b + bar(1)
+ } ensuring { res =>
+ res > a && res < 2
+ }
+
+ def bar(a: BigInt): BigInt = {
+ require(a > 0)
+ val b = a
+ assert(b > 0, "Hey now")
+ b + 2
+ } ensuring { res =>
+ res > a && res > 2
+ }
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/BVDivision.scala b/src/test/resources/regression/verification/newsolvers/invalid/BVDivision.scala
new file mode 100644
index 000000000..a2572db84
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/BVDivision.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object BVDivision {
+
+ def divByZero(x: Int): Boolean = {
+ (x / 0 == 10)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/BVDivision2.scala b/src/test/resources/regression/verification/newsolvers/invalid/BVDivision2.scala
new file mode 100644
index 000000000..c11405429
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/BVDivision2.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object BVDivision2 {
+
+ def division(x: Int, y: Int): Int = {
+ x / y
+ }
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/BigArray.scala b/src/test/resources/regression/verification/newsolvers/invalid/BigArray.scala
new file mode 100644
index 000000000..1395a1e89
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/BigArray.scala
@@ -0,0 +1,13 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.annotation._
+import leon.lang._
+
+object BigArray {
+
+ def big(a: Array[Int]): Int = {
+ require(a.length >= 10 && a(7) == 42)
+ a.length
+ } ensuring(_ <= 1000000000)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/Division.scala b/src/test/resources/regression/verification/newsolvers/invalid/Division.scala
new file mode 100644
index 000000000..6b505a773
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/Division.scala
@@ -0,0 +1,11 @@
+import leon.lang._
+import leon.collection._
+import leon._
+
+object Division {
+
+ def divByZero(x: BigInt): Boolean = {
+ (x / BigInt(0) == BigInt(10))
+ }
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/EnsuringBoolean.scala b/src/test/resources/regression/verification/newsolvers/invalid/EnsuringBoolean.scala
new file mode 100644
index 000000000..239cb7db2
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/EnsuringBoolean.scala
@@ -0,0 +1,12 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon._
+import leon.lang._
+import leon.annotation._
+import scala.language.postfixOps
+object EnsuringBoolean {
+ def congR(x: BigInt)(implicit mod: BigInt): Unit = {
+ require(mod >= 1);
+ ()
+ } ensuring(false)
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/FiniteSort.scala b/src/test/resources/regression/verification/newsolvers/invalid/FiniteSort.scala
new file mode 100644
index 000000000..0cb31c890
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/FiniteSort.scala
@@ -0,0 +1,56 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+
+object FiniteSort {
+
+ // These finite sorting functions essentially implement insertion sort.
+ def sort2(x : Int, y : Int) : (Int,Int) = {
+ if(x < y) (x, y) else (y, x)
+ }
+
+ def sort3(x1 : Int, x2 : Int, x3 : Int) : (Int, Int, Int) = {
+ val (x1s, x2s) = sort2(x1, x2)
+
+ if(x2s <= x3) {
+ (x1s, x2s, x3)
+ } else if(x1s <= x3) {
+ (x1s, x3, x2s)
+ } else {
+ (x3, x1s, x2s)
+ }
+ }
+
+ def sort4(x1 : Int, x2 : Int, x3 : Int, x4 : Int) : (Int, Int, Int, Int) = {
+ val (x1s, x2s, x3s) = sort3(x1, x2, x3)
+
+ if(x3s <= x4) {
+ (x1s, x2s, x3s, x4)
+ } else if(x2s <= x4) {
+ (x1s, x2s, x4, x3s)
+ } else if(x1s <= x4) {
+ (x1s, x4, x2s, x3s)
+ } else {
+ (x4, x1s, x2s, x3s)
+ }
+ }
+
+ def sort5WrongSpec(x1 : Int, x2 : Int, x3 : Int, x4 : Int, x5 : Int) : (Int, Int, Int, Int, Int) = {
+ val (x1s, x2s, x3s, x4s) = sort4(x1, x2, x3, x4)
+
+ if(x4s <= x5) {
+ (x1s, x2s, x3s, x4s, x5)
+ } else if(x3s <= x5) {
+ (x1s, x2s, x3s, x5, x4s)
+ } else if(x2s <= x5) {
+ (x1s, x2s, x5, x3s, x4s)
+ } else if(x1s <= x5) {
+ (x1s, x5, x2s, x3s, x4s)
+ } else {
+ (x5, x1s, x2s, x3s, x4s)
+ }
+
+ } ensuring (_ match {
+ case (a, b, c, d, e) => a <= b && b <= c && c <= d && d <= e && Set(a,b,c,d,e) == Set(x1,x2,x3,x4,x4) // last one should be x5
+ })
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/Generics.scala b/src/test/resources/regression/verification/newsolvers/invalid/Generics.scala
new file mode 100644
index 000000000..21971e521
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/Generics.scala
@@ -0,0 +1,15 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+
+object Generics {
+ abstract class List[T]
+ case class Cons[A](head: A, tail: List[A]) extends List[A]
+ case class Nil[B]() extends List[B]
+
+ def size[T](l: List[T]): BigInt = (l match {
+ case Nil() => BigInt(0)
+ case Cons(h, t) => 1+size(t)
+ })ensuring { _ > 0 }
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/Generics2.scala b/src/test/resources/regression/verification/newsolvers/invalid/Generics2.scala
new file mode 100644
index 000000000..32d97e003
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/Generics2.scala
@@ -0,0 +1,25 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+
+object Generics2 {
+ abstract class List[T]
+ case class Cons[A](head: A, tail: List[A]) extends List[A]
+ case class Nil[B]() extends List[B]
+
+ def size[T](l: List[T]): BigInt = (l match {
+ case Nil() => BigInt(0)
+ case Cons(h, t) => 1+size(t)
+ })ensuring { _ >= 0 }
+
+ def foo[T](l: List[T]): List[T] = {
+ require(size(l) < 2)
+
+ l
+ }
+
+ def bar(l: List[Int]) = {
+ foo(l)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/InsertionSort.scala b/src/test/resources/regression/verification/newsolvers/invalid/InsertionSort.scala
new file mode 100644
index 000000000..d82f045b5
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/InsertionSort.scala
@@ -0,0 +1,43 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.annotation._
+import leon.lang._
+
+object InsertionSort {
+ sealed abstract class List
+ case class Cons(head:Int,tail:List) extends List
+ case class Nil() extends List
+
+ sealed abstract class OptInt
+ case class Some(value: Int) extends OptInt
+ case class None() extends OptInt
+
+ def size(l : List) : BigInt = (l match {
+ case Nil() => BigInt(0)
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def contents(l: List): Set[Int] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def isSorted(l: List): Boolean = l match {
+ case Nil() => true
+ case Cons(x, Nil()) => true
+ case Cons(x, Cons(y, ys)) => x <= y && isSorted(Cons(y, ys))
+ }
+
+ /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+ * the expected content and size */
+ def buggySortedIns(e: Int, l: List): List = {
+ // require(isSorted(l))
+ l match {
+ case Nil() => Cons(e,Nil())
+ case Cons(x,xs) => if (x <= e) Cons(x,buggySortedIns(e, xs)) else Cons(e, l)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ && isSorted(res)
+ && size(res) == size(l) + 1
+ )
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/ListOperations.scala b/src/test/resources/regression/verification/newsolvers/invalid/ListOperations.scala
new file mode 100644
index 000000000..196353358
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/ListOperations.scala
@@ -0,0 +1,108 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.annotation._
+import leon.lang._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class BigIntPairList
+ case class IPCons(head: BigIntPair, tail: BigIntPairList) extends BigIntPairList
+ case class IPNil() extends BigIntPairList
+
+ sealed abstract class BigIntPair
+ case class IP(fst: BigInt, snd: BigInt) extends BigIntPair
+
+ def size(l: List) : BigInt = (l match {
+ case Nil() => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def iplSize(l: BigIntPairList) : BigInt = (l match {
+ case IPNil() => BigInt(0)
+ case IPCons(_, xs) => 1 + iplSize(xs)
+ }) ensuring(_ >= 0)
+
+ def zip(l1: List, l2: List) : BigIntPairList = {
+ // try to comment this and see how pattern-matching becomes
+ // non-exhaustive and post-condition fails
+ require(size(l1) == size(l2))
+
+ l1 match {
+ case Nil() => IPNil()
+ case Cons(x, xs) => l2 match {
+ case Cons(y, ys) => IPCons(IP(x, y), zip(xs, ys))
+ }
+ }
+ } ensuring(iplSize(_) == size(l1))
+
+ def sizeTailRec(l: List) : BigInt = sizeTailRecAcc(l, 0)
+ def sizeTailRecAcc(l: List, acc: BigInt) : BigInt = {
+ require(acc >= 0)
+ l match {
+ case Nil() => acc
+ case Cons(_, xs) => sizeTailRecAcc(xs, acc+1)
+ }
+ } ensuring(res => res == size(l) + acc)
+
+ def sizesAreEquiv(l: List) : Boolean = {
+ size(l) == sizeTailRec(l)
+ }.holds
+
+ def content(l: List) : Set[BigInt] = l match {
+ case Nil() => Set.empty[BigInt]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def sizeAndContent(l: List) : Boolean = {
+ size(l) == BigInt(0) || content(l) != Set.empty[BigInt]
+ }.holds
+
+ def drunk(l : List) : List = (l match {
+ case Nil() => Nil()
+ case Cons(x,l1) => Cons(x,Cons(x,drunk(l1)))
+ }) ensuring (size(_) == 2 * size(l))
+
+ 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
+ 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
+
+ @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 : BigInt, l2 : List) : Boolean = {
+ (append(reverse(l1), Cons(e,l2)) == reverse0(l1, l2))
+ }.holds
+
+ @induct
+ def sizeAppend(l1 : List, l2 : List) : Boolean =
+ (size(append(l1, l2)) == size(l1) + size(l2)).holds
+
+ @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)
+ case Cons(y, ys) => {
+ concat0(Nil(), ys, Cons(y, l3))
+ }
+ }
+ case Cons(x, xs) => concat0(xs, l2, Cons(x, l3))
+ }) ensuring(content(_) == content(l1) ++ content(l2) ++ content(l3))
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/MyTuple1.scala b/src/test/resources/regression/verification/newsolvers/invalid/MyTuple1.scala
new file mode 100644
index 000000000..f2aa840a8
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/MyTuple1.scala
@@ -0,0 +1,13 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object MyTuple1 {
+
+ def foo(): Int = {
+ val t = (1, true, 3)
+ val a1 = t._1
+ val a2 = t._2
+ val a3 = t._3
+ a3
+ } ensuring( _ == 1)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/MyTuple2.scala b/src/test/resources/regression/verification/newsolvers/invalid/MyTuple2.scala
new file mode 100644
index 000000000..0bd3d302f
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/MyTuple2.scala
@@ -0,0 +1,16 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object MyTuple2 {
+
+ abstract class A
+ case class B(i: Int) extends A
+ case class C(a: A) extends A
+
+ def foo(): Int = {
+ val t = (B(2), C(B(3)))
+ t match {
+ case (B(x), C(y)) => x
+ }
+ } ensuring( _ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/MyTuple3.scala b/src/test/resources/regression/verification/newsolvers/invalid/MyTuple3.scala
new file mode 100644
index 000000000..cd514455b
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/MyTuple3.scala
@@ -0,0 +1,9 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object MyTuple3 {
+
+ def foo(t: (Int, Int)): (Int, Int) = {
+ t
+ } ensuring(res => res._1 > 0 && res._2 > 1)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/PositiveMap.scala b/src/test/resources/regression/verification/newsolvers/invalid/PositiveMap.scala
new file mode 100644
index 000000000..c9f290853
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/PositiveMap.scala
@@ -0,0 +1,27 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+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/src/test/resources/regression/verification/newsolvers/invalid/PropositionalLogic.scala b/src/test/resources/regression/verification/newsolvers/invalid/PropositionalLogic.scala
new file mode 100644
index 000000000..547978dbc
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/PropositionalLogic.scala
@@ -0,0 +1,87 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+import leon.annotation._
+
+object PropositionalLogic {
+
+ sealed abstract class Formula
+ case class And(lhs: Formula, rhs: Formula) extends Formula
+ case class Or(lhs: Formula, rhs: Formula) extends Formula
+ case class Implies(lhs: Formula, rhs: Formula) extends Formula
+ case class Not(f: Formula) extends Formula
+ case class Literal(id: Int) extends Formula
+
+ def simplify(f: Formula): Formula = (f match {
+ case And(lhs, rhs) => And(simplify(lhs), simplify(rhs))
+ case Or(lhs, rhs) => Or(simplify(lhs), simplify(rhs))
+ case Implies(lhs, rhs) => Or(Not(simplify(lhs)), simplify(rhs))
+ case Not(f) => Not(simplify(f))
+ case Literal(_) => f
+ }) ensuring(isSimplified(_))
+
+ def isSimplified(f: Formula): Boolean = f match {
+ case And(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
+ case Or(lhs, rhs) => isSimplified(lhs) && isSimplified(rhs)
+ case Implies(_,_) => false
+ case Not(f) => isSimplified(f)
+ case Literal(_) => true
+ }
+
+ def nnf(formula: Formula): Formula = (formula match {
+ case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
+ case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
+ case Implies(lhs, rhs) => Implies(nnf(lhs), nnf(rhs))
+ case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
+ case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
+ case Not(Not(f)) => nnf(f)
+ case Not(Literal(_)) => formula
+ case Literal(_) => formula
+ }) ensuring(isNNF(_))
+
+ def isNNF(f: Formula): Boolean = f match {
+ case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Implies(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+ case Not(Literal(_)) => true
+ case Not(_) => false
+ case Literal(_) => true
+ }
+
+ def vars(f: Formula): Set[Int] = {
+ require(isNNF(f))
+ f match {
+ case And(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Or(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Implies(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Not(Literal(i)) => Set[Int](i)
+ case Literal(i) => Set[Int](i)
+ }
+ }
+
+ def fv(f : Formula) = { vars(nnf(f)) }
+
+ // @induct
+ // def wrongCommutative(f: Formula) : Boolean = {
+ // nnf(simplify(f)) == simplify(nnf(f))
+ // }.holds
+
+ @induct
+ def simplifyBreaksNNF(f: Formula) : Boolean = {
+ require(isNNF(f))
+ isNNF(simplify(f))
+ }.holds
+
+ @induct
+ def nnfIsStable(f: Formula) : Boolean = {
+ require(isNNF(f))
+ nnf(f) == f
+ }.holds
+
+ @induct
+ def simplifyIsStable(f: Formula) : Boolean = {
+ require(isSimplified(f))
+ simplify(f) == f
+ }.holds
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/README b/src/test/resources/regression/verification/newsolvers/invalid/README
new file mode 100644
index 000000000..3b276ff54
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/README
@@ -0,0 +1,2 @@
+This particular directory contains PureScala programs that have *at least* one
+failing verification condition.
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/RedBlackTree.scala b/src/test/resources/regression/verification/newsolvers/invalid/RedBlackTree.scala
new file mode 100644
index 000000000..c0d4fd9a6
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/RedBlackTree.scala
@@ -0,0 +1,103 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.annotation._
+import leon.lang._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case class Red() extends Color
+ case class Black() extends Color
+
+ sealed abstract class Tree
+ case class Empty() extends Tree
+ case class Node(color: Color, left: Tree, value: BigInt, right: Tree) extends Tree
+
+ sealed abstract class OptionBigInt
+ case class Some(v : BigInt) extends OptionBigInt
+ case class None() extends OptionBigInt
+
+ def content(t: Tree) : Set[BigInt] = t match {
+ case Empty() => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : BigInt = (t match {
+ case Empty() => BigInt(0)
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }) ensuring(_ >= 0)
+
+ def isBlack(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(),_,_,_) => true
+ case _ => false
+ }
+
+ def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(Black(), l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ case Node(Red(), l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+ case Empty() => true
+ case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+ }
+
+ def blackBalanced(t : Tree) : Boolean = t match {
+ case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+ case Empty() => true
+ }
+
+ def blackHeight(t : Tree) : BigInt = t match {
+ case Empty() => 1
+ case Node(Black(), l, _, _) => blackHeight(l) + 1
+ case Node(Red(), l, _, _) => blackHeight(l)
+ }
+
+ def ins(x: BigInt, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ t match {
+ case Empty() => Node(Red(),Empty(),x,Empty())
+ case Node(c,a,y,b) =>
+ if (x < y) balance(c, ins(x, a), y, b)
+ else if (x == y) Node(c,a,y,b)
+ else balance(c,a,y,ins(x, b))
+ }
+ } ensuring (res => content(res) == content(t) ++ Set(x)
+ && size(t) <= size(res) && size(res) <= size(t) + 1
+ && redDescHaveBlackChildren(res)
+ && blackBalanced(res))
+
+ def balance(c: Color, a: Tree, x: BigInt, b: Tree): Tree = {
+ Node(c,a,x,b) match {
+ case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
+
+ def buggyAdd(x: BigInt, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t))
+ ins(x, t)
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+
+ def buggyBalance(c: Color, a: Tree, x: BigInt, b: Tree): Tree = {
+ Node(c,a,x,b) match {
+ case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+ Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+ // case Node(c,a,xV,b) => Node(c,a,xV,b)
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)))
+}
diff --git a/src/test/resources/regression/verification/newsolvers/invalid/Unit1.scala b/src/test/resources/regression/verification/newsolvers/invalid/Unit1.scala
new file mode 100644
index 000000000..d286487c0
--- /dev/null
+++ b/src/test/resources/regression/verification/newsolvers/invalid/Unit1.scala
@@ -0,0 +1,9 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object Unit1 {
+
+ def foo(u: Unit): Unit = ({
+ u
+ }) ensuring(res => false)
+
+}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/AmortizedQueue.scala b/src/test/resources/regression/verification/newsolvers/valid/AmortizedQueue.scala
index 0b55b9a51..b5f30a7e1 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/AmortizedQueue.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/AmortizedQueue.scala
@@ -5,7 +5,7 @@ import leon.annotation._
object AmortizedQueue {
sealed abstract class List
- case class Cons(head : Int, tail : List) extends List
+ case class Cons(head : BigInt, tail : List) extends List
case class Nil() extends List
sealed abstract class AbsQueue
@@ -16,8 +16,8 @@ object AmortizedQueue {
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)
- def content(l: List) : Set[Int] = l match {
- case Nil() => Set.empty[Int]
+ def content(l: List) : Set[BigInt] = l match {
+ case Nil() => Set.empty[BigInt]
case Cons(x, xs) => Set(x) ++ content(xs)
}
@@ -51,7 +51,7 @@ object AmortizedQueue {
Queue(concat(front, reverse(rear)), Nil())
} ensuring(isAmortized(_))
- def enqueue(queue : AbsQueue, elem : Int) : AbsQueue = (queue match {
+ def enqueue(queue : AbsQueue, elem : BigInt) : AbsQueue = (queue match {
case Queue(front, rear) => amortizedQueue(front, Cons(elem, rear))
}) ensuring(isAmortized(_))
@@ -62,7 +62,7 @@ object AmortizedQueue {
}
} ensuring (isAmortized(_))
- def front(queue : AbsQueue) : Int = {
+ def front(queue : AbsQueue) : BigInt = {
require(isAmortized(queue) && !isEmpty(queue))
queue match {
case Queue(Cons(f, _), _) => f
@@ -70,7 +70,7 @@ object AmortizedQueue {
}
// @induct
- // def propEnqueue(rear : List, front : List, list : List, elem : Int) : Boolean = {
+ // def propEnqueue(rear : List, front : List, list : List, elem : BigInt) : Boolean = {
// require(isAmortized(Queue(front, rear)))
// val queue = Queue(front, rear)
// if (asList(queue) == list) {
@@ -80,7 +80,7 @@ object AmortizedQueue {
// }.holds
@induct
- def propFront(queue : AbsQueue, list : List, elem : Int) : Boolean = {
+ def propFront(queue : AbsQueue, list : List, elem : BigInt) : Boolean = {
require(!isEmpty(queue) && isAmortized(queue))
if (asList(queue) == list) {
list match {
@@ -91,7 +91,7 @@ object AmortizedQueue {
}.holds
@induct
- def propTail(rear : List, front : List, list : List, elem : Int) : Boolean = {
+ def propTail(rear : List, front : List, list : List, elem : BigInt) : Boolean = {
require(!isEmpty(Queue(front, rear)) && isAmortized(Queue(front, rear)))
if (asList(Queue(front, rear)) == list) {
list match {
@@ -101,14 +101,14 @@ object AmortizedQueue {
true
} //.holds
- def enqueueAndFront(queue : AbsQueue, elem : Int) : Boolean = {
+ def enqueueAndFront(queue : AbsQueue, elem : BigInt) : Boolean = {
if (isEmpty(queue))
front(enqueue(queue, elem)) == elem
else
true
}.holds
- def enqueueDequeueThrice(queue : AbsQueue, e1 : Int, e2 : Int, e3 : Int) : Boolean = {
+ def enqueueDequeueThrice(queue : AbsQueue, e1 : BigInt, e2 : BigInt, e3 : BigInt) : Boolean = {
if (isEmpty(queue)) {
val q1 = enqueue(queue, e1)
val q2 = enqueue(q1, e2)
diff --git a/src/test/resources/regression/verification/newsolvers/valid/FiniteSort.scala b/src/test/resources/regression/verification/newsolvers/valid/FiniteSort.scala
index 94d90c3f4..bdebd2527 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/FiniteSort.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/FiniteSort.scala
@@ -5,13 +5,13 @@ import leon.lang._
object FiniteSorting {
// These finite sorting functions essentially implement insertion sort.
- def sort2(x : Int, y : Int) : (Int,Int) = {
+ def sort2(x : BigInt, y : BigInt) : (BigInt,BigInt) = {
if(x < y) (x, y) else (y, x)
} ensuring (_ match {
case (a, b) => a <= b && Set(a,b) == Set(x,y)
})
- def sort3(x1 : Int, x2 : Int, x3 : Int) : (Int, Int, Int) = {
+ def sort3(x1 : BigInt, x2 : BigInt, x3 : BigInt) : (BigInt, BigInt, BigInt) = {
val (x1s, x2s) = sort2(x1, x2)
if(x2s <= x3) {
@@ -25,7 +25,7 @@ object FiniteSorting {
case (a, b, c) => a <= b && b <= c && Set(a,b,c) == Set(x1,x2,x3)
})
- def sort4(x1 : Int, x2 : Int, x3 : Int, x4 : Int) : (Int, Int, Int, Int) = {
+ def sort4(x1 : BigInt, x2 : BigInt, x3 : BigInt, x4 : BigInt) : (BigInt, BigInt, BigInt, BigInt) = {
val (x1s, x2s, x3s) = sort3(x1, x2, x3)
if(x3s <= x4) {
@@ -41,7 +41,7 @@ object FiniteSorting {
case (a, b, c, d) => a <= b && b <= c && c <= d && Set(a,b,c,d) == Set(x1,x2,x3,x4)
})
- def sort5(x1 : Int, x2 : Int, x3 : Int, x4 : Int, x5 : Int) : (Int, Int, Int, Int, Int) = {
+ def sort5(x1 : BigInt, x2 : BigInt, x3 : BigInt, x4 : BigInt, x5 : BigInt) : (BigInt, BigInt, BigInt, BigInt, BigInt) = {
val (x1s, x2s, x3s, x4s) = sort4(x1, x2, x3, x4)
if(x4s <= x5) {
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Heap.scala b/src/test/resources/regression/verification/newsolvers/valid/Heap.scala
index 260cc8583..11f577ea1 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/Heap.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/Heap.scala
@@ -7,25 +7,25 @@ object Heaps {
/*~~~~~~~~~~~~~~~~~~~~~~~*/
/* Data type definitions */
/*~~~~~~~~~~~~~~~~~~~~~~~*/
- private case class Node(rank : BigInt, elem : Int, nodes : Heap)
+ private case class Node(rank : BigInt, elem : BigInt, nodes : Heap)
sealed abstract class Heap
private case class Nodes(head : Node, tail : Heap) extends Heap
private case object Empty extends Heap
sealed abstract class OptInt
- case class Some(value : Int) extends OptInt
+ case class Some(value : BigInt) extends OptInt
case object None extends OptInt
/*~~~~~~~~~~~~~~~~~~~~~~~*/
/* Abstraction functions */
/*~~~~~~~~~~~~~~~~~~~~~~~*/
- def heapContent(h : Heap) : Set[Int] = h match {
- case Empty => Set.empty[Int]
+ def heapContent(h : Heap) : Set[BigInt] = h match {
+ case Empty => Set.empty[BigInt]
case Nodes(n, ns) => nodeContent(n) ++ heapContent(ns)
}
- def nodeContent(n : Node) : Set[Int] = n match {
+ def nodeContent(n : Node) : Set[BigInt] = n match {
case Node(_, e, h) => Set(e) ++ heapContent(h)
}
@@ -74,17 +74,17 @@ object Heaps {
})
/*~~~~~~~~~~~~~~~~*/
- /* Heap interface */
+ /* Heap Interface */
/*~~~~~~~~~~~~~~~~*/
def empty() : Heap = {
Empty
- } ensuring(res => heapContent(res) == Set.empty[Int])
+ } ensuring(res => heapContent(res) == Set.empty[BigInt])
def isEmpty(h : Heap) : Boolean = {
(h == Empty)
- } ensuring(res => res == (heapContent(h) == Set.empty[Int]))
+ } ensuring(res => res == (heapContent(h) == Set.empty[BigInt]))
- def insert(e : Int, h : Heap) : Heap = {
+ def insert(e : BigInt, h : Heap) : Heap = {
insertNode(Node(0, e, Empty), h)
} ensuring(res => heapContent(res) == heapContent(h) ++ Set(e))
diff --git a/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala b/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala
index 81109ba33..0a922e2a4 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/InsertionSort.scala
@@ -5,11 +5,11 @@ import leon.lang._
object InsertionSort {
sealed abstract class List
- case class Cons(head:Int,tail:List) extends List
+ case class Cons(head:BigInt,tail:List) extends List
case class Nil() extends List
sealed abstract class OptInt
- case class Some(value: Int) extends OptInt
+ case class Some(value: BigInt) extends OptInt
case class None() extends OptInt
def size(l : List) : BigInt = (l match {
@@ -17,7 +17,7 @@ object InsertionSort {
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)
- def contents(l: List): Set[Int] = l match {
+ def contents(l: List): Set[BigInt] = l match {
case Nil() => Set.empty
case Cons(x,xs) => contents(xs) ++ Set(x)
}
@@ -38,7 +38,7 @@ object InsertionSort {
/* Inserting element 'e' into a sorted list 'l' produces a sorted list with
* the expected content and size */
- def sortedIns(e: Int, l: List): List = {
+ def sortedIns(e: BigInt, l: List): List = {
require(isSorted(l))
l match {
case Nil() => Cons(e,Nil())
diff --git a/src/test/resources/regression/verification/newsolvers/valid/ListOperations.scala b/src/test/resources/regression/verification/newsolvers/valid/ListOperations.scala
index 3965ab57d..4a2b54d6e 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/ListOperations.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/ListOperations.scala
@@ -2,103 +2,89 @@
import leon.annotation._
import leon.lang._
+import leon.collection._
object ListOperations {
- sealed abstract class List
- case class Cons(head: Int, tail: List) extends List
- case class Nil() extends List
-
- sealed abstract class IntPairList
- case class IPCons(head: IntPair, tail: IntPairList) extends IntPairList
- case class IPNil() extends IntPairList
-
- sealed abstract class IntPair
- case class IP(fst: Int, snd: Int) extends IntPair
-
- def size(l: List) : BigInt = (l match {
- case Nil() => BigInt(0)
- case Cons(_, t) => 1 + size(t)
- }) ensuring(res => res >= 0)
-
- def iplSize(l: IntPairList) : BigInt = (l match {
- case IPNil() => BigInt(0)
- case IPCons(_, xs) => 1 + iplSize(xs)
- }) ensuring(_ >= 0)
-
- def zip(l1: List, l2: List) : IntPairList = {
- // try to comment this and see how pattern-matching becomes
- // non-exhaustive and post-condition fails
- require(size(l1) == size(l2))
-
- l1 match {
- case Nil() => IPNil()
- case Cons(x, xs) => l2 match {
- case Cons(y, ys) => IPCons(IP(x, y), zip(xs, ys))
- }
- }
- } ensuring(iplSize(_) == size(l1))
-
- def sizeTailRec(l: List) : BigInt = sizeTailRecAcc(l, 0)
- def sizeTailRecAcc(l: List, acc: BigInt) : BigInt = {
- require(acc >= 0)
- l match {
- case Nil() => acc
- case Cons(_, xs) => sizeTailRecAcc(xs, acc+1)
- }
- } ensuring(res => res == size(l) + acc)
-
- def sizesAreEquiv(l: List) : Boolean = {
- size(l) == sizeTailRec(l)
- }.holds
-
- def content(l: List) : Set[Int] = l match {
- case Nil() => Set.empty[Int]
- case Cons(x, xs) => Set(x) ++ content(xs)
- }
- def sizeAndContent(l: List) : Boolean = {
- size(l) == BigInt(0) || content(l) != Set.empty[Int]
- }.holds
-
- def drunk(l : List) : List = (l match {
- case Nil() => Nil()
- case Cons(x,l1) => Cons(x,Cons(x,drunk(l1)))
- }) ensuring (size(_) == 2 * size(l))
-
- 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
- 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
-
- @induct
- def appendAssoc(xs : List, ys : List, zs : List) : Boolean =
- (append(append(xs, ys), zs) == append(xs, append(ys, zs))).holds
-
- @induct
- def sizeAppend(l1 : List, l2 : List) : Boolean =
- (size(append(l1, l2)) == size(l1) + size(l2)).holds
-
- @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)
- case Cons(y, ys) => {
- concat0(Nil(), ys, Cons(y, l3))
- }
+ def size[A](l: List[A]) : BigInt = (l match {
+ case Nil() => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content[A](l: List[A]) : Set[A] = l match {
+ case Nil() => Set[A]()
+ case Cons(h, t) => content(t) ++ Set[A](h)
+ }
+
+ def zip[A,B](l1: List[A], l2: List[B]): List[(A, B)] = {
+ // try to comment this and see how pattern-matching becomes
+ // non-exhaustive and post-condition fails
+ require(size(l1) == size(l2))
+ (l1, l2) match {
+ case (Nil(), Nil()) =>
+ Nil[(A, B)]()
+ case (Cons(x, xs), Cons(y, ys)) =>
+ Cons( (x,y), zip(xs, ys) )
+ }
+ } ensuring(size(_) == size(l1))
+
+ def sizeTailRec[A](l: List[A]) : BigInt = sizeTailRecAcc(l, 0)
+
+ def sizeTailRecAcc[A](l: List[A], acc: BigInt) : BigInt = {
+ require(acc >= 0)
+ l match {
+ case Nil() => acc
+ case Cons(_, xs) => sizeTailRecAcc(xs, acc+1)
+ }
+ } ensuring(res => res == size(l) + acc)
+
+ def sizesAreEquiv[A](l: List[A]) : Boolean = {
+ size(l) == sizeTailRec(l)
+ }.holds
+
+ def sizeAndContent[A](l: List[A]) : Boolean = {
+ size(l) == BigInt(0) || content(l) != Set.empty[A]
+ }.holds
+
+ def drunk[A](l : List[A]) : List[A] = (l match {
+ case Nil() => Nil()
+ case Cons(x,l1) => Cons(x,Cons(x,drunk(l1)))
+ }) ensuring (size(_) == 2 * size(l))
+
+ def reverse[A](l: List[A]) : List[A] = reverse0(l, Nil[A]()) ensuring(content(_) == content(l))
+ def reverse0[A](l1: List[A], l2: List[A]) : List[A] = (l1 match {
+ case Nil() => l2
+ case Cons(x, xs) => reverse0(xs, Cons[A](x, l2))
+ }) ensuring(content(_) == content(l1) ++ content(l2))
+
+ def append[A](l1 : List[A], l2 : List[A]) : List[A] = (l1 match {
+ case Nil() => l2
+ case Cons(x,xs) => Cons[A](x, append(xs, l2))
+ }) ensuring(content(_) == content(l1) ++ content(l2))
+
+ @induct
+ def nilAppend[A](l : List[A]) : Boolean = (append(l, Nil[A]()) == l).holds
+
+ @induct
+ def appendAssoc[A](xs : List[A], ys : List[A], zs : List[A]) : Boolean =
+ (append(append(xs, ys), zs) == append(xs, append(ys, zs))).holds
+
+ @induct
+ def sizeAppend[A](l1 : List[A], l2 : List[A]) : Boolean =
+ (size(append(l1, l2)) == size(l1) + size(l2)).holds
+
+ @induct
+ def concat[A](l1: List[A], l2: List[A]) : List[A] =
+ concat0(l1, l2, Nil[A]()) ensuring(content(_) == content(l1) ++ content(l2))
+
+ @induct
+ def concat0[A](l1: List[A], l2: List[A], l3: List[A]) : List[A] = (l1 match {
+ case Nil() => l2 match {
+ case Nil() => reverse(l3)
+ case Cons(y, ys) => {
+ concat0(Nil[A](), ys, Cons(y, l3))
}
- case Cons(x, xs) => concat0(xs, l2, Cons(x, l3))
- }) ensuring(content(_) == content(l1) ++ content(l2) ++ content(l3))
+ }
+ case Cons(x, xs) => concat0(xs, l2, Cons(x, l3))
+ }) ensuring(content(_) == content(l1) ++ content(l2) ++ content(l3))
}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/MergeSort.scala b/src/test/resources/regression/verification/newsolvers/valid/MergeSort.scala
index de8b0c32b..133c19bca 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/MergeSort.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/MergeSort.scala
@@ -6,20 +6,20 @@ import leon.lang._
object MergeSort {
// Data types
sealed abstract class List
- case class Cons(head : Int, tail : List) extends List
+ case class Cons(head : BigInt, tail : List) extends List
case class Nil() extends List
sealed abstract class LList
case class LCons(head : List, tail : LList) extends LList
case class LNil() extends LList
- def content(list : List) : Set[Int] = list match {
- case Nil() => Set.empty[Int]
+ def content(list : List) : Set[BigInt] = list match {
+ case Nil() => Set.empty[BigInt]
case Cons(x, xs) => Set(x) ++ content(xs)
}
- def lContent(llist : LList) : Set[Int] = llist match {
- case LNil() => Set.empty[Int]
+ def lContent(llist : LList) : Set[BigInt] = llist match {
+ case LNil() => Set.empty[BigInt]
case LCons(x, xs) => content(x) ++ lContent(xs)
}
diff --git a/src/test/resources/regression/verification/newsolvers/valid/SearchLinkedList.scala b/src/test/resources/regression/verification/newsolvers/valid/SearchLinkedList.scala
index 87076bb97..f0fd1c13f 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/SearchLinkedList.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/SearchLinkedList.scala
@@ -5,7 +5,7 @@ import leon.annotation._
object SearchLinkedList {
sealed abstract class List
- case class Cons(head : Int, tail : List) extends List
+ case class Cons(head : BigInt, tail : List) extends List
case class Nil() extends List
def size(list : List) : BigInt = (list match {
@@ -13,7 +13,7 @@ object SearchLinkedList {
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)
- def contains(list : List, elem : Int) : Boolean = (list match {
+ def contains(list : List, elem : BigInt) : Boolean = (list match {
case Nil() => false
case Cons(x, xs) => x == elem || contains(xs, elem)
})
diff --git a/src/test/resources/regression/verification/newsolvers/valid/Subtyping1.scala b/src/test/resources/regression/verification/newsolvers/valid/Subtyping1.scala
index 8e3433b94..e84f5bafa 100644
--- a/src/test/resources/regression/verification/newsolvers/valid/Subtyping1.scala
+++ b/src/test/resources/regression/verification/newsolvers/valid/Subtyping1.scala
@@ -14,21 +14,17 @@ object Subtyping1 {
}
def treeMax(tree: Node): Int = {
- tree match {
- case Node(_, v, right) => right match {
- case Leaf() => v
- case Node(l, v, r) => treeMax(Node(l, v, r))
- }
+ tree.right match {
+ case Leaf() => tree.value
+ case n:Node => treeMax(n)
}
} ensuring(content(tree).contains(_))
def f2(tree: Node): Int = {
require(treeMax(tree) > 0)
- tree match {
- case Node(_, v, right) => right match {
- case Leaf() => v
- case Node(l, v, r) => treeMax(Node(l, v, r))
- }
+ tree.right match {
+ case Leaf() => tree.value
+ case n:Node => f2(n)
}
} ensuring(content(tree).contains(_))
--
GitLab