no more demo stuff

demo/Arith.scala

-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)
-
-}

demo/BubbleSortBug.scala

-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)
-      i = i - 1
-    }) invariant(i >= 0 && i < sa.length)
-    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
-  }
-
-}

demo/List.scala

-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
-  }
-
-}

demo/ListOperations.scala

-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))
-}

demo/MaxSum.scala

-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)
-  }
-
-}

demo/RedBlackTree.scala

-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))
-}

run-demo

-./leon --timeout=10 --noLuckyTests $@

run-demo-testgen

-./leon --nodefaults --extensions=leon.TestGeneration $@