diff --git a/demo/Arith.scala b/demo/Arith.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d4b02f51b5e532a15b9fb3571534316e0cc962ce
--- /dev/null
+++ b/demo/Arith.scala
@@ -0,0 +1,41 @@
+import leon.Utils._
+
+object Arith {
+
+ def mult(x : Int, y : Int): Int = ({
+ var r = 0
+ if(y < 0) {
+ var n = y
+ (while(n != 0) {
+ r = r - x
+ n = n + 1
+ }) invariant(r == x * (y - n) && 0 <= -n)
+ } else {
+ var n = y
+ (while(n != 0) {
+ r = r + x
+ n = n - 1
+ }) invariant(r == x * (y - n) && 0 <= n)
+ }
+ r
+ }) ensuring(_ == x*y)
+
+ def add(x : Int, y : Int): Int = ({
+ var r = x
+ if(y < 0) {
+ var n = y
+ (while(n != 0) {
+ r = r - 1
+ n = n + 1
+ }) invariant(r == x + y - n && 0 <= -n)
+ } else {
+ var n = y
+ (while(n != 0) {
+ r = r + 1
+ n = n - 1
+ }) invariant(r == x + y - n && 0 <= n)
+ }
+ r
+ }) ensuring(_ == x+y)
+
+}
diff --git a/demo/BubbleSortBug.scala b/demo/BubbleSortBug.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d8d1c4eb9097b7bf09fe67f981efd55f183fe375
--- /dev/null
+++ b/demo/BubbleSortBug.scala
@@ -0,0 +1,74 @@
+import leon.Utils._
+
+/* The calculus of Computation textbook */
+
+object BubbleSortBug {
+
+ def sort(a: Array[Int]): Array[Int] = ({
+ require(a.length >= 1)
+ var i = a.length - 1
+ var j = 0
+ val sa = a.clone
+ (while(i > 0) {
+ j = 0
+ (while(j < i) {
+ if(sa(j) < sa(j+1)) {
+ val tmp = sa(j)
+ sa(j) = sa(j+1)
+ sa(j+1) = tmp
+ }
+ j = j + 1
+ }) invariant(
+ j >= 0 &&
+ j <= i &&
+ i < sa.length &&
+ sa.length >= 0 &&
+ partitioned(sa, 0, i, i+1, sa.length-1) &&
+ sorted(sa, i, sa.length-1) &&
+ partitioned(sa, 0, j, j+1, j+1)
+ )
+ i = i - 1
+ }) invariant(
+ i >= 0 &&
+ i < sa.length &&
+ sa.length >= 0 &&
+ partitioned(sa, 0, i, i+1, sa.length-1) &&
+ sorted(sa, i, sa.length-1)
+ )
+ sa
+ }) ensuring(res => sorted(res, 0, a.length-1))
+
+ def sorted(a: Array[Int], l: Int, u: Int): Boolean = {
+ require(a.length >= 0 && l >= 0 && u < a.length && l <= u)
+ var k = l
+ var isSorted = true
+ (while(k < u) {
+ if(a(k) > a(k+1))
+ isSorted = false
+ k = k + 1
+ }) invariant(k <= u && k >= l)
+ isSorted
+ }
+
+ def partitioned(a: Array[Int], l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+ require(a.length >= 0 && l1 >= 0 && u1 < l2 && u2 < a.length)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ var i = l1
+ var j = l2
+ var isPartitionned = true
+ (while(i <= u1) {
+ j = l2
+ (while(j <= u2) {
+ if(a(i) > a(j))
+ isPartitionned = false
+ j = j + 1
+ }) invariant(j >= l2 && i <= u1)
+ i = i + 1
+ }) invariant(i >= l1)
+ isPartitionned
+ }
+ }
+
+}
diff --git a/demo/List.scala b/demo/List.scala
new file mode 100644
index 0000000000000000000000000000000000000000..302e86774c7d1e68e08d48ce957c87ec483b3d56
--- /dev/null
+++ b/demo/List.scala
@@ -0,0 +1,20 @@
+import leon.Utils._
+
+object List {
+
+ abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ def size(l: List): Int = waypoint(1, (l match {
+ case Cons(_, tail) => sizeTail(tail, 1)
+ case Nil() => 0
+ })) ensuring(_ >= 0)
+
+
+ def sizeTail(l2: List, acc: Int): Int = l2 match {
+ case Cons(_, tail) => sizeTail(tail, acc+1)
+ case Nil() => acc
+ }
+
+}
diff --git a/demo/ListOperations.scala b/demo/ListOperations.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a4fc4f8dc44a90f59a772b52b1a05053316e94d2
--- /dev/null
+++ b/demo/ListOperations.scala
@@ -0,0 +1,107 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+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) : Int = (l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def iplSize(l: IntPairList) : Int = (l match {
+ case IPNil() => 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) : Int = sizeTailRecAcc(l, 0)
+ def sizeTailRecAcc(l: List, acc: Int) : Int = {
+ 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) == 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
+
+ def revAuxBroken(l1 : List, e : Int, 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/demo/MaxSum.scala b/demo/MaxSum.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ba724d255c23b782e1b4de716ccc8d50043e2059
--- /dev/null
+++ b/demo/MaxSum.scala
@@ -0,0 +1,38 @@
+import leon.Utils._
+
+/* VSTTE 2010 challenge 1 */
+
+object MaxSum {
+
+ def maxSum(a: Array[Int]): (Int, Int) = ({
+ require(a.length >= 0 && isPositive(a))
+ var sum = 0
+ var max = 0
+ var i = 0
+ (while(i < a.length) {
+ if(max < a(i))
+ max = a(i)
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant (sum <= i * max && i >= 0 && i <= a.length)
+ (sum, max)
+ }) ensuring(res => res._1 <= a.length * res._2)
+
+
+ def isPositive(a: Array[Int]): Boolean = {
+ require(a.length >= 0)
+ def rec(i: Int): Boolean = {
+ require(i >= 0)
+ if(i >= a.length)
+ true
+ else {
+ if(a(i) < 0)
+ false
+ else
+ rec(i+1)
+ }
+ }
+ rec(0)
+ }
+
+}
diff --git a/demo/RedBlackTree.scala b/demo/RedBlackTree.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bc2de6ba96ee699736d4558932b752eea9ebba9f
--- /dev/null
+++ b/demo/RedBlackTree.scala
@@ -0,0 +1,117 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+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: Int, right: Tree) extends Tree
+
+ sealed abstract class OptionInt
+ case class Some(v : Int) extends OptionInt
+ case class None() extends OptionInt
+
+ def content(t: Tree) : Set[Int] = t match {
+ case Empty() => Set.empty
+ case Node(_, l, v, r) => content(l) ++ Set(v) ++ content(r)
+ }
+
+ def size(t: Tree) : Int = (t match {
+ case Empty() => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }) ensuring(_ >= 0)
+
+ /* We consider leaves to be black by definition */
+ 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) : Int = t match {
+ case Empty() => 1
+ case Node(Black(), l, _, _) => blackHeight(l) + 1
+ case Node(Red(), l, _, _) => blackHeight(l)
+ }
+
+ // <<insert element x into the tree t>>
+ def ins(x: Int, 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 makeBlack(n: Tree): Tree = {
+ require(redDescHaveBlackChildren(n) && blackBalanced(n))
+ n match {
+ case Node(Red(),l,v,r) => Node(Black(),l,v,r)
+ case _ => n
+ }
+ } ensuring(res => redNodesHaveBlackChildren(res) && blackBalanced(res))
+
+ def add(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+ makeBlack(ins(x, t))
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res))
+
+ def buggyAdd(x: Int, t: Tree): Tree = {
+ require(redNodesHaveBlackChildren(t))
+ ins(x, t)
+ } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
+
+ def balance(c: Color, a: Tree, x: Int, 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 buggyBalance(c: Color, a: Tree, x: Int, 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))
+}
diff --git a/run-demo b/run-demo
new file mode 100755
index 0000000000000000000000000000000000000000..0b47f73e90dd9e0ec5f5cbe80a9e7ae508824832
--- /dev/null
+++ b/run-demo
@@ -0,0 +1 @@
+./leon --timeout=5 --noLuckyTests $@
diff --git a/run-demo-testgen b/run-demo-testgen
new file mode 100755
index 0000000000000000000000000000000000000000..90b0479f2dc548a4b2df35042cc802604aca3ee3
--- /dev/null
+++ b/run-demo-testgen
@@ -0,0 +1 @@
+./leon --nodefaults --extensions=leon.TestGeneration $@