diff --git a/README.md b/README.md
index 4cc0b8eb272a5eff8861973eb961be951d8aa545..f4f3f6120ae06bead692d0e99e32d8a56641019b 100644
--- a/README.md
+++ b/README.md
@@ -29,31 +29,38 @@ To build, type this:
Then you can try e.g.
- $ ./leon ./testcases/sas2011-testcases/RedBlackTree.scala
+ $ ./leon ./testcases/verification/sas2011-testcases/RedBlackTree.scala
and get something like this:
<pre>
- ┌─────────â”
- â•”â•â•¡ Summary â•žâ•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•—
- ║ └─────────┘ ║
- â•‘ add postcond. valid Z3-f+t 0.314 â•‘
- â•‘ add precond. (82,14) valid Z3-f+t 0.020 â•‘
- â•‘ add precond. (82,18) valid Z3-f+t 0.005 â•‘
- â•‘ balance postcond. valid Z3-f+t 0.409 â•‘
- â•‘ balance match. (91,19) valid Z3-f+t 0.034 â•‘
- â•‘ blackHeight match. (51,39) valid Z3-f+t 0.004 â•‘
- â•‘ buggyAdd postcond. invalid Z3-f+t 4.084 â•‘
- â•‘ buggyAdd precond. (87,8) invalid Z3-f+t 0.111 â•‘
- â•‘ buggyBalance postcond. invalid Z3-f+t 0.055 â•‘
- â•‘ buggyBalance match. (105,19) invalid Z3-f+t 0.007 â•‘
- â•‘ ins postcond. valid Z3-f+t 6.577 â•‘
- â•‘ ins precond. (63,40) valid Z3-f+t 0.021 â•‘
- â•‘ ins precond. (65,43) valid Z3-f+t 0.005 â•‘
- â•‘ makeBlack postcond. valid Z3-f+t 0.007 â•‘
- â•‘ redNodesHaveBlackChildren match. (35,56) valid Z3-f+t 0.003 â•‘
- â•‘ size postcond. valid Z3-f+t 0.012 â•‘
- â•šâ•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•
+ ┌──────────────────────â”
+ â•”â•â•¡ Verification Summary â•žâ•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•—
+ ║ └──────────────────────┘ ║
+ â•‘ add postcondition 83:22 valid Z3-f 0.057 â•‘
+ â•‘ add precondition 82:5 valid Z3-f 0.017 â•‘
+ â•‘ add precondition 82:15 valid Z3-f 0.003 â•‘
+ â•‘ balance match exhaustiveness 91:5 valid Z3-f 0.005 â•‘
+ â•‘ balance postcondition 102:22 valid Z3-f 0.055 â•‘
+ â•‘ blackBalanced match exhaustiveness 46:43 valid Z3-f 0.003 â•‘
+ â•‘ blackHeight match exhaustiveness 51:40 valid Z3-f 0.004 â•‘
+ â•‘ buggyAdd postcondition 88:22 invalid Z3-f 1.162 â•‘
+ â•‘ buggyAdd precondition 87:5 invalid Z3-f 0.027 â•‘
+ â•‘ buggyBalance match exhaustiveness 105:5 invalid Z3-f 0.007 â•‘
+ â•‘ buggyBalance postcondition 116:22 invalid Z3-f 0.017 â•‘
+ â•‘ content match exhaustiveness 18:37 valid Z3-f 0.034 â•‘
+ â•‘ ins match exhaustiveness 60:5 valid Z3-f 0.003 â•‘
+ â•‘ ins postcondition 67:22 valid Z3-f 1.753 â•‘
+ â•‘ ins precondition 63:37 valid Z3-f 0.011 â•‘
+ â•‘ ins precondition 65:40 valid Z3-f 0.012 â•‘
+ â•‘ makeBlack postcondition 78:21 valid Z3-f 0.012 â•‘
+ â•‘ redDescHaveBlackChildren match exhaustiveness 41:53 valid Z3-f 0.003 â•‘
+ â•‘ redNodesHaveBlackChildren match exhaustiveness 35:54 valid Z3-f 0.004 â•‘
+ â•‘ size match exhaustiveness 23:33 valid Z3-f 0.004 â•‘
+ â•‘ size postcondition 26:15 valid Z3-f 0.043 â•‘
+ ╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
+ â•‘ total: 21 valid: 17 invalid: 4 unknown 0 3.236 â•‘
+ â•šâ•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•â•
</pre>
Building Leon
diff --git a/testcases/verification/sas2011-testcases/AmortizedQueue.scala b/testcases/verification/sas2011-testcases/AmortizedQueue.scala
index 52e4ed7e2c313d83b46f766e7694e152ca4c19b9..a3636e00aa2141d95c814a7448d6be950710c906 100644
--- a/testcases/verification/sas2011-testcases/AmortizedQueue.scala
+++ b/testcases/verification/sas2011-testcases/AmortizedQueue.scala
@@ -10,8 +10,8 @@ object AmortizedQueue {
sealed abstract class AbsQueue
case class Queue(front : List, rear : List) extends AbsQueue
- def size(list : List) : Int = (list match {
- case Nil() => 0
+ def size(list : List) : BigInt = (list match {
+ case Nil() => BigInt(0)
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)
diff --git a/testcases/verification/sas2011-testcases/InsertionSort.scala b/testcases/verification/sas2011-testcases/InsertionSort.scala
index a29e2116d2783f02f4759d0ffd1e8103420883fe..b01d0ae2f292b8a27a9ec911d167a50478a93ce3 100644
--- a/testcases/verification/sas2011-testcases/InsertionSort.scala
+++ b/testcases/verification/sas2011-testcases/InsertionSort.scala
@@ -4,19 +4,19 @@ 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) : Int = (l match {
- case Nil() => 0
+ 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 {
+ def contents(l: List): Set[BigInt] = l match {
case Nil() => Set.empty
case Cons(x,xs) => contents(xs) ++ Set(x)
}
@@ -37,7 +37,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())
@@ -50,7 +50,7 @@ object InsertionSort {
/* 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 = {
+ def buggySortedIns(e: BigInt, l: List): List = {
// require(isSorted(l))
l match {
case Nil() => Cons(e,Nil())
diff --git a/testcases/verification/sas2011-testcases/ListOperations.scala b/testcases/verification/sas2011-testcases/ListOperations.scala
index 86d0f522f69633e0321da4d52bb32352b7cc1239..2cba911ada05b76afc8bd7cf906c0ed196e9a7fd 100644
--- a/testcases/verification/sas2011-testcases/ListOperations.scala
+++ b/testcases/verification/sas2011-testcases/ListOperations.scala
@@ -14,13 +14,13 @@ object ListOperations {
sealed abstract class IntPair
case class IP(fst: Int, snd: Int) extends IntPair
- def size(l: List) : Int = (l match {
- case Nil() => 0
+ 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) : Int = (l match {
- case IPNil() => 0
+ def iplSize(l: IntPairList) : BigInt = (l match {
+ case IPNil() => BigInt(0)
case IPCons(_, xs) => 1 + iplSize(xs)
}) ensuring(_ >= 0)
@@ -37,8 +37,8 @@ object ListOperations {
}
} ensuring(iplSize(_) == size(l1))
- def sizeTailRec(l: List) : Int = sizeTailRecAcc(l, 0)
- def sizeTailRecAcc(l: List, acc: Int) : Int = {
+ def sizeTailRec(l: List) : BigInt = sizeTailRecAcc(l, 0)
+ def sizeTailRecAcc(l: List, acc: BigInt) : BigInt = {
require(acc >= 0)
l match {
case Nil() => acc
diff --git a/testcases/verification/sas2011-testcases/RedBlackTree.scala b/testcases/verification/sas2011-testcases/RedBlackTree.scala
index 11daef0b03ee0e4eae57db7735128456e3844649..e77838fff0d92429c7cea9065ec69c775e3151de 100644
--- a/testcases/verification/sas2011-testcases/RedBlackTree.scala
+++ b/testcases/verification/sas2011-testcases/RedBlackTree.scala
@@ -20,8 +20,8 @@ object RedBlackTree {
case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
}
- def size(t: Tree) : Int = (t match {
- case Empty() => 0
+ def size(t: Tree) : BigInt = (t match {
+ case Empty() => BigInt(0)
case Node(_, l, v, r) => size(l) + 1 + size(r)
}) ensuring(_ >= 0)
@@ -48,8 +48,8 @@ object RedBlackTree {
case Empty() => true
}
- def blackHeight(t : Tree) : Int = t match {
- case Empty() => 1
+ def blackHeight(t : Tree) : BigInt = t match {
+ case Empty() => BigInt(1)
case Node(Black(), l, _, _) => blackHeight(l) + 1
case Node(Red(), l, _, _) => blackHeight(l)
}
diff --git a/testcases/verification/sas2011-testcases/SearchLinkedList.scala b/testcases/verification/sas2011-testcases/SearchLinkedList.scala
index 02f265f12b1c6cf6e12c0d6fcf5df6dbb3e71558..40f29050f030f2ab260580d5d03df9db42de2477 100644
--- a/testcases/verification/sas2011-testcases/SearchLinkedList.scala
+++ b/testcases/verification/sas2011-testcases/SearchLinkedList.scala
@@ -7,8 +7,8 @@ object SearchLinkedList {
case class Cons(head : Int, tail : List) extends List
case class Nil() extends List
- def size(list : List) : Int = (list match {
- case Nil() => 0
+ def size(list : List) : BigInt = (list match {
+ case Nil() => BigInt(0)
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)
@@ -17,9 +17,9 @@ object SearchLinkedList {
case Cons(x, xs) => x == elem || contains(xs, elem)
})
- def firstZero(list : List) : Int = (list match {
- case Nil() => 0
- case Cons(x, xs) => if (x == 0) 0 else firstZero(xs) + 1
+ def firstZero(list : List) : BigInt = (list match {
+ case Nil() => BigInt(0)
+ case Cons(x, xs) => if (x == 0) BigInt(0) else firstZero(xs) + 1
}) ensuring (res =>
res >= 0 && (if (contains(list, 0)) {
firstZeroAtPos(list, res)
@@ -27,14 +27,14 @@ object SearchLinkedList {
res == size(list)
}))
- def firstZeroAtPos(list : List, pos : Int) : Boolean = {
+ def firstZeroAtPos(list : List, pos : BigInt) : Boolean = {
list match {
case Nil() => false
case Cons(x, xs) => if (pos == 0) x == 0 else x != 0 && firstZeroAtPos(xs, pos - 1)
}
}
- def goal(list : List, i : Int) : Boolean = {
+ def goal(list : List, i : BigInt) : Boolean = {
if(firstZero(list) == i) {
if(contains(list, 0)) {
firstZeroAtPos(list, i)
diff --git a/testcases/verification/sas2011-testcases/SumAndMax.scala b/testcases/verification/sas2011-testcases/SumAndMax.scala
index a3fd5c3a50d6c56592dbd6d48b7bc90ac940d58f..c9383e64c0108f2a9c23091a7c85fe54b5f0b007 100644
--- a/testcases/verification/sas2011-testcases/SumAndMax.scala
+++ b/testcases/verification/sas2011-testcases/SumAndMax.scala
@@ -3,10 +3,10 @@ import leon.annotation._
object SumAndMax {
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 max(list : List) : Int = {
+ def max(list : List) : BigInt = {
require(list != Nil())
list match {
case Cons(x, Nil()) => x
@@ -17,13 +17,13 @@ object SumAndMax {
}
}
- def sum(list : List) : Int = list match {
- case Nil() => 0
+ def sum(list : List) : BigInt = list match {
+ case Nil() => BigInt(0)
case Cons(x, xs) => x + sum(xs)
}
- def size(list : List) : Int = (list match {
- case Nil() => 0
+ def size(list : List) : BigInt = (list match {
+ case Nil() => BigInt(0)
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)