From e20455d15674bf2bbf4c8669293a8f822a33f5ed Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Wed, 24 Oct 2012 17:43:52 -0700
Subject: [PATCH] no more demo stuff
---
demo/Arith.scala | 41 -------------
demo/BubbleSortBug.scala | 39 -------------
demo/List.scala | 20 -------
demo/ListOperations.scala | 107 ----------------------------------
demo/MaxSum.scala | 38 -------------
demo/RedBlackTree.scala | 117 --------------------------------------
run-demo | 1 -
run-demo-testgen | 1 -
8 files changed, 364 deletions(-)
delete mode 100644 demo/Arith.scala
delete mode 100644 demo/BubbleSortBug.scala
delete mode 100644 demo/List.scala
delete mode 100644 demo/ListOperations.scala
delete mode 100644 demo/MaxSum.scala
delete mode 100644 demo/RedBlackTree.scala
delete mode 100755 run-demo
delete mode 100755 run-demo-testgen
diff --git a/demo/Arith.scala b/demo/Arith.scala
deleted file mode 100644
index d4b02f51b..000000000
--- a/demo/Arith.scala
+++ /dev/null
@@ -1,41 +0,0 @@
-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
deleted file mode 100644
index a25554f03..000000000
--- a/demo/BubbleSortBug.scala
+++ /dev/null
@@ -1,39 +0,0 @@
-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
- }
-
-}
diff --git a/demo/List.scala b/demo/List.scala
deleted file mode 100644
index 302e86774..000000000
--- a/demo/List.scala
+++ /dev/null
@@ -1,20 +0,0 @@
-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
deleted file mode 100644
index a4fc4f8dc..000000000
--- a/demo/ListOperations.scala
+++ /dev/null
@@ -1,107 +0,0 @@
-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
deleted file mode 100644
index ba724d255..000000000
--- a/demo/MaxSum.scala
+++ /dev/null
@@ -1,38 +0,0 @@
-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
deleted file mode 100644
index bc2de6ba9..000000000
--- a/demo/RedBlackTree.scala
+++ /dev/null
@@ -1,117 +0,0 @@
-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
deleted file mode 100755
index a3db30e66..000000000
--- a/run-demo
+++ /dev/null
@@ -1 +0,0 @@
-./leon --timeout=10 --noLuckyTests $@
diff --git a/run-demo-testgen b/run-demo-testgen
deleted file mode 100755
index 90b0479f2..000000000
--- a/run-demo-testgen
+++ /dev/null
@@ -1 +0,0 @@
-./leon --nodefaults --extensions=leon.TestGeneration $@
--
GitLab