diff --git a/testcases/web/demos/01_Compiler.scala b/testcases/web/demos/01_Compiler.scala
new file mode 100644
index 0000000000000000000000000000000000000000..87b06b2c61473eb5c4172785ffc956a461d5fc04
--- /dev/null
+++ b/testcases/web/demos/01_Compiler.scala
@@ -0,0 +1,201 @@
+import leon.lang._
+import leon.annotation._
+import leon.collection._
+import leon._
+
+object Tokens {
+ abstract class Token
+ case object TPlus extends Token
+ case object TTimes extends Token
+ case object TLT extends Token
+ case object TIf extends Token
+ case object TElse extends Token
+ case object TLAnd extends Token
+ case object TLOr extends Token
+ case object TLeftBrace extends Token
+ case object TRightBrace extends Token
+ case object TLeftPar extends Token
+ case object TRightPar extends Token
+ case class TInt(v: BigInt) extends Token
+ case class TId(name: BigInt) extends Token // All variables are : BigInt
+}
+
+object Trees {
+ abstract class Expr
+ case class Times(lhs: Expr, rhs: Expr) extends Expr
+ case class Plus(lhs: Expr, rhs: Expr) extends Expr
+ case class And(lhs: Expr, rhs: Expr) extends Expr
+ case class Or(lhs: Expr, rhs: Expr) extends Expr
+ case class Var(id: BigInt) extends Expr
+ case class IntLiteral(v: BigInt) extends Expr
+ case class LessThan(lhs: Expr, rhs: Expr) extends Expr
+ case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
+}
+
+object Types {
+ abstract class Type
+ case object IntType extends Type
+ case object BoolType extends Type
+}
+
+object Parser {
+ import Tokens._
+ import Trees._
+
+ def parsePhrase(ts: List[Token]): Option[Expr] = {
+ parseGoal(ts) match {
+ case Some((res, Nil())) => Some(res)
+ case _ => None()
+ }
+ }
+
+ def parseGoal(ts: List[Token]): Option[(Expr, List[Token])] = {
+ parseOr(ts)
+ }
+
+ def parseOr(ts: List[Token]): Option[(Expr, List[Token])] = {
+ parseAnd(ts) match {
+ case Some((lhs, Cons(TLOr, r))) =>
+ parseAnd(r) match {
+ case Some((rhs, ts2)) => Some((Or(lhs, rhs), ts2))
+ case None() => None()
+ }
+ case r => r
+ }
+ }
+
+ def parseAnd(ts: List[Token]): Option[(Expr, List[Token])] = {
+ parseLT(ts) match {
+ case Some((lhs, Cons(TLAnd, r))) =>
+ parseLT(r) match {
+ case Some((rhs, ts2)) => Some((And(lhs, rhs), ts2))
+ case None() => None()
+ }
+ case r => r
+ }
+ }
+
+ def parseLT(ts: List[Token]): Option[(Expr, List[Token])] = {
+ parsePlus(ts) match {
+ case Some((lhs, Cons(TLT, r))) =>
+ parsePlus(r) match {
+ case Some((rhs, ts2)) => Some((LessThan(lhs, rhs), ts2))
+ case None() => None()
+ }
+ case r => r
+ }
+ }
+
+ def parsePlus(ts: List[Token]): Option[(Expr, List[Token])] = {
+ parseTimes(ts) match {
+ case Some((lhs, Cons(TPlus, r))) =>
+ parsePlus(r) match {
+ case Some((rhs, ts2)) => Some((Plus(lhs, rhs), ts2))
+ case None() => None()
+ }
+ case r => r
+ }
+ }
+
+ def parseTimes(ts: List[Token]): Option[(Expr, List[Token])] = {
+ parseLits(ts) match {
+ case Some((lhs, Cons(t, r))) if (t == TTimes) =>
+ parseTimes(r) match {
+ case Some((rhs, ts2)) => Some((Plus(lhs, rhs), ts2))
+ case None() => None()
+ }
+ case r => r
+ }
+ }
+
+ def parseLits(ts: List[Token]): Option[(Expr, List[Token])] = ts match {
+ case Cons(TInt(v), r) => Some((IntLiteral(v), r))
+ case Cons(TId(v), r) => Some((Var(v), r))
+ case Cons(TLeftPar, r) =>
+ parseGoal(r) match {
+ case Some((e, Cons(TRightPar, ts2))) => Some((e, ts2))
+ case _ => None()
+ }
+ case Cons(TIf, Cons(TLeftPar, r)) =>
+ parseGoal(r) match {
+ case Some((c, Cons(TRightPar, Cons(TLeftBrace, ts2)))) =>
+ // Then
+ parseGoal(ts2) match {
+ case Some((th, Cons(TRightBrace, Cons(TElse, Cons(TLeftBrace, ts3))))) =>
+ // Else
+ parseGoal(ts3) match {
+ case Some((el, Cons(TRightBrace, ts4))) =>
+ Some((Ite(c, th, el), ts4))
+ case _ => None()
+ }
+ case _ => None()
+ }
+ case _ => None()
+ }
+ case _ => None()
+ }
+}
+
+object TypeChecker {
+ import Trees._
+ import Types._
+
+ def typeChecks(e: Expr, exp: Option[Type]): Boolean = e match {
+ case Times(l, r) => (exp.getOrElse(IntType) == IntType) && typeChecks(l, Some(IntType)) && typeChecks(r, Some(IntType))
+ case Plus(l, r) => (exp.getOrElse(IntType) == IntType) && typeChecks(l, Some(IntType)) && typeChecks(r, Some(IntType))
+ case And(l, r) => (exp.getOrElse(BoolType) == BoolType) && typeChecks(l, Some(BoolType)) && typeChecks(r, Some(BoolType))
+ case Or(l, r) => (exp.getOrElse(BoolType) == BoolType) && typeChecks(l, Some(BoolType)) && typeChecks(r, Some(BoolType))
+ case LessThan(l, r) => (exp.getOrElse(BoolType) == BoolType) && typeChecks(l, Some(IntType)) && typeChecks(r, Some(IntType))
+ case Ite(c, th, el) => typeChecks(c, Some(BoolType)) && typeChecks(th, exp) && typeChecks(el, exp)
+ case IntLiteral(_) => exp.getOrElse(IntType) == IntType
+ case Var(_) => exp.getOrElse(IntType) == IntType
+ }
+
+ def typeChecks(e: Expr): Boolean = typeChecks(e, None())
+}
+
+object Simplifier {
+ import Trees._
+ import Runtime._
+
+ // Constant folding + tautologies
+ def simplify(e: Expr)(implicit m: Map[BigInt, BigInt]): Expr = (e match {
+ // Special cases
+ case Plus(IntLiteral(a), IntLiteral(b)) => IntLiteral(a+b)
+ case LessThan(Var(id1), Var(id2)) if id1 == id2 => IntLiteral(0)
+
+ // Recursion
+ case Times(lhs, rhs) => Times(simplify(lhs), simplify(rhs))
+ case Plus(lhs, rhs) => Plus(simplify(lhs), simplify(rhs))
+ case And(lhs, rhs) => And(simplify(lhs), simplify(rhs))
+ case Or(lhs, rhs) => And(simplify(lhs), simplify(rhs))
+ case LessThan(lhs, rhs) => LessThan(simplify(lhs), simplify(rhs))
+ case Ite(cond, then, elze) => Ite(simplify(cond), simplify(then), simplify(elze))
+ case _ => e
+ }) ensuring {
+ res => run(res)(m) == run(e)(m)
+ }
+
+}
+
+object Runtime {
+ import Trees._
+
+ def run(e: Expr)(implicit m: Map[BigInt, BigInt]): BigInt = e match {
+ case Times(lhs, rhs) => run(lhs) * run(rhs)
+ case Plus(lhs, rhs) => run(lhs) + run(rhs)
+ case And(lhs, rhs) => run(lhs) * run(rhs)
+ case Or(lhs, rhs) => if ((run(lhs) + run(rhs)) > 0) 1 else 0
+ case IntLiteral(v) => v
+ case Var(id) => if (m contains id) m(id) else 0
+ case LessThan(lhs, rhs) => if (run(lhs) < run(rhs)) 1 else 0
+ case Ite(cond, then, elze) => if (run(cond) != 0) run(then) else run(elze)
+ }
+
+ def test() = {
+ run(Plus(IntLiteral(42), Var(0)))(Map(0 -> 1))
+ }
+}
+
+
+
diff --git a/testcases/web/demos/02_Lists.scala b/testcases/web/demos/02_Lists.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f4abad115e3cc0f5e1908884f0088c3e21021010
--- /dev/null
+++ b/testcases/web/demos/02_Lists.scala
@@ -0,0 +1,46 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object List {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set()
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+
+
+ def insertUnique(l: List, v: BigInt): List = (l match {
+ case Cons(h, t) =>
+ if (h == v) {
+ l
+ } else {
+ Cons(h, insertUnique(t, v))
+ }
+ case Nil =>
+ Cons(v, Nil)
+ }) ensuring { (res: List) =>
+ true
+ //content(res) == content(l) ++ Set(v) &&
+ //size(res) >= size(l)
+ }
+
+
+
+
+ def delete(l: List, v: BigInt): List = {
+ choose{ (res: List) =>
+ content(res) == content(l) -- Set(v)
+ }
+ }
+
+}
diff --git a/testcases/web/demos/03_Splits.scala b/testcases/web/demos/03_Splits.scala
new file mode 100644
index 0000000000000000000000000000000000000000..740dc34a8cf6ce680b3807779ee70fb97c3fa635
--- /dev/null
+++ b/testcases/web/demos/03_Splits.scala
@@ -0,0 +1,46 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object List {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def abs(i : BigInt) : BigInt = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ def split1(list: List): (List,List) = {
+ choose { (res: (List,List)) =>
+ (content(res._1) ++ content(res._2) == content(list))
+ }
+ }
+
+ def split2(list: List): (List,List) = {
+ choose { (res: (List,List)) =>
+ (content(res._1) ++ content(res._2) == content(list)) &&
+ abs(size(res._1) - size(res._2)) <= 1
+ }
+ }
+
+ def split3(list: List): (List,List) = {
+ choose { (res: (List,List)) =>
+ (content(res._1) ++ content(res._2) == content(list)) &&
+ abs(size(res._1) - size(res._2)) <= 1 &&
+ size(res._1)+size(res._2) == size(list)
+ }
+ }
+
+}
+
diff --git a/testcases/web/demos/04_Sort.scala b/testcases/web/demos/04_Sort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a53a8987055fe802e75aaadd602589ab47d074fd
--- /dev/null
+++ b/testcases/web/demos/04_Sort.scala
@@ -0,0 +1,77 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+object Sort {
+/*
+ def sort2(x : BigInt, y : BigInt) = choose{(res: (BigInt,BigInt)) =>
+ Set(x,y) == Set(res._1, res._2) && res._1 <= res._2
+ }
+*/
+
+/*
+ sealed abstract class List
+ case object Nil extends List
+ case class Cons(head: BigInt, tail: List) extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(x, rest) => x + size(rest)
+ })
+*/
+ // ensuring(res => res > 0)
+
+ // def s1 = size(Cons(10, Cons(1000, Nil)))
+
+/*
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set()
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+*/
+
+/*
+ def isSorted(l : List) : Boolean = l match {
+ case Nil => true
+ case Cons(_,Nil) => true
+ case Cons(x1, Cons(x2, rest)) =>
+ x1 < x2 && isSorted(Cons(x2,rest))
+ }
+*/
+ //def t1 = isSorted(Cons(10, Cons(20, Nil)))
+ //def t2 = isSorted(Cons(15, Cons(15, Nil)))
+
+/*
+ def sInsert(x : BigInt, l : List) : List = {
+ require(isSorted(l))
+ l match {
+ case Nil => Cons(x, Nil)
+ case Cons(e, rest) if (x == e) => l
+ case Cons(e, rest) if (x < e) => Cons(x, Cons(e,rest))
+ case Cons(e, rest) if (x > e) => Cons(e, sInsert(x,rest))
+ }
+ } ensuring {(res:List) =>
+ isSorted(res) && content(res) == content(l) ++ Set(x)}
+
+ // size(res) == size(l) + 1
+*/
+
+/*
+ def insertMagic(x: BigInt, l: List): List = {
+ require(isSorted(l))
+ choose {(res: List) =>
+ isSorted(res) && content(res) == content(l) ++ Set[BigInt](x)
+ }
+ }
+*/
+
+ //def m = insertMagic(17, Cons(10, Cons(15, Cons(20, Nil))))
+
+/*
+ def sortMagic(l : List) = choose{(res:List) =>
+ isSorted(res) && content(res) == content(l)
+ }
+*/
+
+ // def mm = sortMagic(Cons(20, Cons(5, Cons(50, Cons(2, Nil)))))
+
+}
diff --git a/testcases/web/demos/05_OpenDays.scala b/testcases/web/demos/05_OpenDays.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9314e4b7585aa19fd66c4f736f81db05b9f3ee76
--- /dev/null
+++ b/testcases/web/demos/05_OpenDays.scala
@@ -0,0 +1,74 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object EpflOpenDays {
+
+ sealed abstract class Liste
+ case object Vide extends Liste
+ case class Elem(e: BigInt, reste: Liste) extends Liste
+
+ def taille(l: Liste): BigInt = (l match {
+ case Vide => 0
+ case Elem(x, reste) => x + taille(reste)
+ })
+
+ //def s0 = taille(Elem(10, Elem(1000, Vide)))
+
+ //ensuring(res => res >= 0)
+
+ //def s1 = taille(Elem(10, Elem(1000, Vide)))
+
+ def contenu(l: Liste): Set[BigInt] = l match {
+ case Vide => Set()
+ case Elem(e, reste) => Set(e) ++ contenu(reste)
+ }
+
+/*
+ def estTriée(l: Liste): Boolean = l match {
+ case Vide => true
+ case Elem(_, Vide) => true
+ case Elem(e1, Elem(e2, reste)) =>
+ e1 < e2 && estTriée(Elem(e2, reste))
+ }
+*/
+
+ //def t1 = estTriée(Elem(10, Elem(14, Elem(20, Elem(25, Vide)))))
+ //def t2 = estTriée(Elem(10, Elem(14, Elem(1, Elem(2, Vide)))))
+
+/*
+ def insertion(x: BigInt, l: Liste): Liste = {
+ require(estTriée(l))
+ l match {
+ case Vide => Elem(x, Vide)
+ case Elem(e, reste) if (x == e) => l
+ case Elem(e, reste) if (x < e) => Elem(x, Elem(e,reste))
+ case Elem(e, reste) if (x > e) => Elem(e, insertion(x, reste))
+ }
+ } ensuring { (res: Liste) =>
+ estTriée(res) &&
+ contenu(res) == contenu(l) ++ Set(x)
+ }
+*/
+/*
+ def insertionMagique(x: BigInt, l: Liste): Liste = {
+ require(estTriée(l))
+ choose { (res: Liste) =>
+ estTriée(res) &&
+ contenu(res) == contenu(l) ++ Set(x)
+ }
+ }
+*/
+
+ //def m1 = insertionMagique(17, Elem(10, Elem(14, Elem(20, Elem(25, Vide)))))
+
+/*
+ def trier(l: Liste) = choose{ (res: Liste) =>
+ estTriée(res) && contenu(res) == contenu(l)
+ }
+*/
+
+ //def mm = trier(Elem(10, Elem(14, Elem(1, Elem(2, Vide)))))
+
+}
+
diff --git a/testcases/web/demos/05_OpenDays1.scala b/testcases/web/demos/05_OpenDays1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6a08b6138710efc005e6127cf0d72cea1dbf44ce
--- /dev/null
+++ b/testcases/web/demos/05_OpenDays1.scala
@@ -0,0 +1,24 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object EpflOpenDays {
+
+ def max3(a: BigInt, b: BigInt, c: BigInt): BigInt = {
+ if (a > b) {
+ if (c > a) {
+ c
+ } else {
+ a
+ }
+ } else {
+ if (c > b) {
+ c
+ } else {
+ a
+ }
+ }
+ } ensuring {
+ res => res >= a && res >= b && res >= c
+ }
+}
diff --git a/testcases/web/demos/05_OpenDays2.scala b/testcases/web/demos/05_OpenDays2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fe99ebb2c17e0473f0cec12c1b020dec4219f8d7
--- /dev/null
+++ b/testcases/web/demos/05_OpenDays2.scala
@@ -0,0 +1,83 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object EpflOpenDays {
+ @library
+ sealed abstract class Piece {
+ def valeur = this match {
+ case Cent5 => 5
+ case Cent10 => 10
+ case Cent20 => 20
+ case Cent50 => 50
+ case Fr1 => 100
+ case Fr2 => 200
+ case Fr5 => 500
+ case Bi10 => 1000
+ case Bi20 => 2000
+ case Bi50 => 5000
+ case Bi100 => 10000
+ case Bi200 => 20000
+ case Bi1000 => 100000
+ }
+
+ }
+ case object Cent5 extends Piece
+ case object Cent10 extends Piece
+ case object Cent20 extends Piece
+ case object Cent50 extends Piece
+ case object Fr1 extends Piece
+ case object Fr2 extends Piece
+ case object Fr5 extends Piece
+ case object Bi10 extends Piece
+ case object Bi20 extends Piece
+ case object Bi50 extends Piece
+ case object Bi100 extends Piece
+ case object Bi200 extends Piece
+ case object Bi1000 extends Piece
+
+
+ @library
+ sealed abstract class Liste {
+ def somme: BigInt = {
+ this match {
+ case Vide => 0
+ case Elem(p, reste) => p.valeur + reste.somme
+ }
+ } ensuring { _ >= 0 }
+ }
+ case object Vide extends Liste
+ case class Elem(e: Piece, reste: Liste) extends Liste
+
+ def pieceMax(v: BigInt): Piece = {
+ require(v > 0 && v%5 == 0)
+ if (v >= Bi1000.valeur) Bi1000
+ else if (v >= Bi200.valeur ) Bi200
+ else if (v >= Bi100.valeur ) Bi100
+ else if (v >= Bi50.valeur ) Bi50
+ else if (v >= Bi20.valeur ) Bi100
+ else if (v >= Bi10.valeur ) Bi10
+ else if (v >= Fr5.valeur ) Fr5
+ else if (v >= Fr2.valeur ) Fr2
+ else if (v >= Fr1.valeur ) Fr1
+ else if (v >= Cent50.valeur ) Cent50
+ else if (v >= Cent20.valeur ) Cent20
+ else if (v >= Cent10.valeur ) Cent10
+ else Cent5
+ } ensuring { _.valeur <= v }
+
+ def pieces(v: BigInt): Liste = {
+ require(v >= 0 && v%5 == 0)
+ if (v == 0) {
+ Vide
+ } else {
+ val p = pieceMax(v)
+ Elem(p, pieces(v - p.valeur))
+ }
+ } ensuring { res =>
+ res.somme == v
+ }
+
+
+ def t = pieces(18440)
+}
diff --git a/testcases/web/sav15/01_Exercise1.scala b/testcases/web/sav15/01_Exercise1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2b5e433c01dae897db69a303f59500f215232b15
--- /dev/null
+++ b/testcases/web/sav15/01_Exercise1.scala
@@ -0,0 +1,19 @@
+object Bank1 {
+ case class Acc(checking : BigInt, savings : BigInt)
+
+ def putAside(x: BigInt, a: Acc): Acc = {
+ require (notRed(a) && a.checking >= x)
+ Acc(a.checking - x, a.savings + x)
+ } ensuring {
+ r => notRed(r) && sameTotal(a, r)
+ }
+
+
+ def sameTotal(a1: Acc, a2: Acc): Boolean = {
+ a1.checking + a1.savings == a2.checking + a2.savings
+ }
+
+ def notRed(a: Acc) : Boolean = {
+ a.checking >= 0 && a.savings >= 0
+ }
+}
diff --git a/testcases/web/sav15/02_Exercise2.scala b/testcases/web/sav15/02_Exercise2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b67ce260367e52ded82e3986d3ab1013a5695d7e
--- /dev/null
+++ b/testcases/web/sav15/02_Exercise2.scala
@@ -0,0 +1,37 @@
+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: BigInt) extends Formula
+
+
+ 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) => nnf(Or(Not(lhs), 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 {
+ /* TODO: Implement isNNF */
+ }
+
+ // Note that matching should be exhaustive due to precondition.
+ def vars(f: Formula): Set[BigInt] = {
+ require(isNNF(f))
+ f match {
+ case And(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Or(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Not(Literal(i)) => Set[BigInt](i)
+ case Literal(i) => Set[BigInt](i)
+ }
+ }
+}
diff --git a/testcases/web/sav15/03_Exercise3.scala b/testcases/web/sav15/03_Exercise3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4dff97756cb94f21b7379c2038d9d323eb14e6aa
--- /dev/null
+++ b/testcases/web/sav15/03_Exercise3.scala
@@ -0,0 +1,100 @@
+import leon.lang._
+import leon.annotation._
+
+object ListWithSize {
+ sealed abstract class List[T] {
+ def size: BigInt = {
+ this match {
+ case Cons(h, t) => 1 + t.size
+ case Nil() => 0
+ }
+ } // TODO: Add appropriate post-condition
+
+ def sizeTailRec: BigInt = sizeTailRec0(0)
+
+ def sizeTailRec0(acc: BigInt): BigInt = {
+ require(acc >= 0)
+ this match {
+ case Cons(h, t) => t.sizeTailRec0(acc + 1)
+ case Nil() => acc
+ }
+ } // TODO: Add appropriate post-condition
+
+ // Verify
+ def zip[U](that: List[U]): List[(T, U)] = {
+ // TODO: Add appropriate pre-condition
+ this match {
+ case Nil() => Nil()
+ case Cons(h1, t1) => that match {
+ case Cons(h2, t2) => Cons((h1, h2), t1.zip(t2))
+ }
+ }
+ } ensuring(_.size == this.size)
+
+
+ def content: Set[T] = this match {
+ case Nil() => Set()
+ case Cons(h, t) => Set(h) ++ t.content
+ }
+
+ // Verify
+ def reverse: List[T] = {
+ reverse0(Nil())
+ } ensuring(_.content == this.content)
+
+ def reverse0(acc: List[T]): List[T] = (this match {
+ case Nil() => acc
+ case Cons(h, t) => t.reverse0(Cons(h, acc))
+ }) // TODO: Add appropriate post-condition
+
+
+ def append(that: List[T]): List[T] = (this match {
+ case Nil() => that
+ case Cons(h, t) => Cons(h, t.append(that))
+ }) ensuring(_.content == this.content ++ that.content)
+
+
+ }
+ case class Cons[T](head: T, tail: List[T]) extends List[T]
+ case class Nil[T]() extends List[T]
+
+
+ // Verify
+ def sizesAreEquiv[T](l: List[T]): Boolean = {
+ l.size == l.sizeTailRec
+ }.holds
+
+
+ def sizeAndContent[T](l: List[T]): Boolean = {
+ l.size == 0 || l.content != Set[T]()
+ }.holds
+
+ def drunk[T](l: List[T]): List[T] = (l match {
+ case Nil() => Nil()
+ case Cons(x,l1) => Cons(x,Cons(x,drunk(l1)))
+ }) ensuring {
+ res => true // TODO: find postcondition
+ }
+
+
+ def funnyCons[T](x: T, l: List[T]): List[T] = (l match {
+ case Nil() => Cons(x, Nil())
+ case c @ Cons(_,_) => Cons(x, c)
+ }) ensuring(_.size > 0)
+
+
+ @induct
+ def nilAppend[T](l: List[T]): Boolean = {
+ l.append(Nil()) == l
+ }.holds
+
+ @induct
+ def appendAssoc[T](xs: List[T], ys: List[T], zs: List[T]) : Boolean = {
+ false // find predicate
+ }.holds
+
+ @induct
+ def sizeAppend[T](l1: List[T], l2 : List[T]) : Boolean = {
+ (l1.append(l2).size == l1.size + l2.size)
+ }.holds
+}
diff --git a/testcases/web/sav15/04_Exercise4.scala b/testcases/web/sav15/04_Exercise4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..411a731137072dc0da6d8ace59620e3ab4c9c63e
--- /dev/null
+++ b/testcases/web/sav15/04_Exercise4.scala
@@ -0,0 +1,68 @@
+import leon.annotation._
+import leon.lang._
+
+object InsertionSort {
+
+ sealed abstract class Option[T]
+ case class Some[T](value: T) extends Option[T]
+ case class None[T]() extends Option[T]
+
+
+ sealed abstract class List {
+ def size: BigInt = (this match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + t.size
+ })
+
+ def content: Set[BigInt] = this match {
+ case Nil() => Set()
+ case Cons(h, t) => Set(h) ++ t.content
+ }
+
+ def min: Option[BigInt] = this match {
+ case Nil() => None()
+ case Cons(h, t) => t.min match {
+ case None() => Some(h)
+ case Some(m) => if(h < m) Some(h) else Some(m)
+ }
+ }
+
+ def isSorted: Boolean = this match {
+ case Nil() => true
+ case Cons(h, Nil()) => true
+ case Cons(h1, t1 @ Cons(h2, t2)) => h1 <= h2 && t1.isSorted
+ }
+
+
+ /* Inserting element 'e' into a sorted list 'l' produces a sorted list with
+ * the expected content and size */
+ def insert(e: BigInt): List = {
+ require(isSorted)
+ this match {
+ case Nil() => Cons(e, Nil())
+ case Cons(h, t) =>
+ if (h <= e) {
+ Cons(h, t.insert(e))
+ } else {
+ Cons(e, this)
+ }
+ }
+ }
+
+
+ /* Insertion sort yields a sorted list of same size and content as the input
+ * list */
+ def sort: List = (this match {
+ case Nil() => Nil()
+ case Cons(h, t) => t.sort.insert(h)
+ }) ensuring(res => res.content == this.content
+ && res.isSorted
+ && res.size == this.size
+ )
+
+ }
+ case class Cons(h: BigInt, t: List) extends List
+ case class Nil() extends List
+
+
+}
diff --git a/testcases/web/sav15/05_Exercise5.scala b/testcases/web/sav15/05_Exercise5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..787ab6de2f8ce304734c0c31fda5ac22695606ba
--- /dev/null
+++ b/testcases/web/sav15/05_Exercise5.scala
@@ -0,0 +1,67 @@
+import leon.lang._
+import leon.annotation._
+
+object SearchList {
+ sealed abstract class List[T] {
+ def size: BigInt = {
+ this match {
+ case Nil() => 0
+ case Cons(h, t) => 1 + t.size
+ }
+ } ensuring { _ >= 0 }
+
+ def content: Set[T] = {
+ this match {
+ case Nil() => Set()
+ case Cons(h, t) => Set(h) ++ t.content
+ }
+ }
+
+ def firstPosOf(v: T): BigInt = {
+ this match {
+ case Nil() => -1
+ case Cons(h, t) if h == v => 0
+ case Cons(h, t) =>
+ val p = t.firstPosOf(v)
+ if (p >= 0) {
+ p + 1
+ } else {
+ p
+ }
+ }
+ } ensuring {
+ res => false // TODO: Ensure that if (and only if) res is non-negative, the list contains v.
+
+ }
+
+ def take(n: BigInt): List[T] = {
+ require(n >= 0)
+ this match {
+ case Nil() => Nil()
+ case Cons(h, t) if n == 0 => Nil()
+ case Cons(h, t) => Cons(h, t.take(n - 1))
+ }
+ } ensuring {
+ res => res.size <= n
+ }
+
+ def contains(v: T): Boolean = {
+ this match {
+ case Nil() => false
+ case Cons(h, _) if h == v => true
+ case Cons(_, t) => t.contains(v)
+ }
+ } ensuring {
+ res => res == (content contains v)
+ }
+ }
+
+ case class Cons[T](h: T, t: List[T]) extends List[T]
+ case class Nil[T]() extends List[T]
+
+ @induct
+ def wtf[T](l: List[T], v: T): Boolean = {
+ !((l.contains(v)) && (l.take(l.firstPosOf(v)).contains(v))) // What is this function checking? Translate to english. Can you remove the l.contains(v) part? Why?
+ }.holds
+}
+
diff --git a/testcases/web/sav15/06_Exercise6.scala b/testcases/web/sav15/06_Exercise6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..636abaca00477c95a0b0d195690f54f49ee0d1e1
--- /dev/null
+++ b/testcases/web/sav15/06_Exercise6.scala
@@ -0,0 +1,104 @@
+import leon.lang._
+import leon.collection._
+import leon._
+/**
+ * 1) Implement the isSearchTree property that checks bounds of elements in a
+ * search tree. Assume that the tree is strictly sorted (no dupplicates)
+ *
+ * 2) Implement operations on Binary Search Trees as efficiently as you can.
+ * These operations will likely not verify, but make sure that leon does not
+ * find counter-examples within a reasonnable timeout (e.g. --timeout=5 )
+ *
+ * You do not need to change the pre-/post-conditions
+ *
+ * 3) Implement toList to return a sorted list from a search tree.
+ */
+
+object BinaryTree {
+
+ abstract class Tree {
+ def content: Set[BigInt] = {
+ this match {
+ case Empty => Set()
+ case Node(l, v, r) => l.content ++ Set(v) ++ r.content
+ }
+ }
+
+ def size: BigInt = {
+ this match {
+ case Empty => 0
+ case Node(l, _, r) => l.size + r.size + 1
+ }
+ } ensuring { _ >= 0 }
+
+
+ def +(x: BigInt): Tree = {
+ require(isBT)
+ this // TODO
+ } ensuring {
+ res => res.isBT &&
+ res.content == this.content ++ Set(x) &&
+ res.size >= this.size &&
+ res.size <= this.size + 1
+ }
+
+ def -(x: BigInt): Tree = {
+ require(isBT)
+ this // TODO
+ } ensuring {
+ res => res.isBT &&
+ res.content == this.content -- Set(x) &&
+ res.size <= this.size &&
+ res.size >= this.size - 1
+ }
+
+ def ++(that: Tree): Tree = {
+ require(this.isBT && that.isBT)
+ this // TODO
+ } ensuring {
+ res => res.isBT && res.content == this.content ++ that.content
+ }
+
+ def contains(x: BigInt): Boolean = {
+ require(isBT)
+ false // TODO
+ } ensuring {
+ res => res == (content contains x)
+ }
+
+ def toList: List[BigInt] = {
+ require(isBT)
+ Nil() // TODO
+ } ensuring {
+ res => res.content == this.content && isSorted(res)
+ }
+
+ // Properties
+
+ def isBT: Boolean = {
+ isSearchTree(None(), None())
+ }
+
+ def isSearchTree(min: Option[BigInt], max: Option[BigInt]): Boolean = {
+ this match {
+ case Empty => true
+ case Node(l, v, r) =>
+ true // TODO
+ }
+ }
+ }
+
+ case object Empty extends Tree
+ case class Node(l: Tree, v: BigInt, r: Tree) extends Tree
+
+
+ def isSorted(l: List[BigInt]): Boolean = {
+ l match {
+ case Cons(v1, t @ Cons(v2, _)) if v1 >= v2 => false
+ case Cons(h, t) => isSorted(t)
+ case Nil() => true
+ }
+ }
+}
+
+
diff --git a/testcases/web/sav15/07_Exercise7.scala b/testcases/web/sav15/07_Exercise7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..dab1fcb5ea47b415810d5fddf1c72cf447c4a11d
--- /dev/null
+++ b/testcases/web/sav15/07_Exercise7.scala
@@ -0,0 +1,32 @@
+import leon.lang._
+
+/**
+ * 1) Implement operations on rationals: addition, substraction, multiplication and division
+ * Ensure that the results are rationals, add necessary preconditions.
+ * 2) Implement rational equivalence (~).
+ * 3) Write lemmas that show that if a1 ~ a2, and b1 ~ b2, then (a1 <op> b1) ~ (a2 <op> b2), for each <op>
+ */
+object Rationals {
+ // Represents n/d
+ case class Q(n: BigInt, d: BigInt) {
+
+ def +(that: Q):Q = this // TODO
+
+ def -(that: Q):Q = this // TODO
+
+ def *(that: Q):Q = this // TODO
+
+ def /(that: Q):Q = this // TODO
+
+ // Equivalence of two rationals
+ def ~(that: Q): Boolean = false // TODO
+
+ def isRational = !(d == 0)
+ def nonZero = !(n == 0)
+ }
+
+ def lemma1(a1: Q, a2: Q, b1: Q, b2: Q): Boolean = {
+ true // TODO
+ }.holds
+}
+
diff --git a/testcases/web/sav15/08_Exercise8.scala b/testcases/web/sav15/08_Exercise8.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1483670b6f5590daa43bc2cd1af9d3781155a823
--- /dev/null
+++ b/testcases/web/sav15/08_Exercise8.scala
@@ -0,0 +1,118 @@
+/**
+ * In this exercise, you will have to implement a packed representation of a set of numbers.
+ * This representation uses a chained list of sorted ranges to represent the stored values.
+ *
+ * [0, 10] :: [15, 15] :: Empty
+ *
+ * stores
+ *
+ * Set(0,1,2,3,4,5,6,7,8,9,10,15)
+ *
+ * You need to implement + and - that adds and deletes single elements from the set.
+ * Leon will not generally be able to verify everything, but it should give you
+ * counter-examples in case you do something wrong.
+ */
+
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object PackedSet {
+ case class Range(min: BigInt, max: BigInt) {
+ def size: BigInt = {
+ if (max >= min) max-min+1
+ else 0
+ }
+
+ def content: Set[BigInt] = {
+ if (max == min) Set(min)
+ else if (max > min) Set(min) ++ Range(min+1, max).content
+ else Set()
+ }
+
+ def contains(v: BigInt): Boolean = {
+ min <= v && max >= v
+ }
+
+ def <(that: Range) = {
+ this.min < that.min
+ }
+
+ def merge(that: Range): Range = {
+ require(this.min == that.min)
+ Range(min, if (this.max > that.max) this.max else that.max)
+ } ensuring {
+ res => res.content == this.content ++ that.content
+ }
+ }
+
+
+ abstract class PackedSet {
+ def size: BigInt = {
+ this match {
+ case Empty => 0
+ case NonEmpty(r, t) => r.size + t.size
+ }
+ }
+
+ def depth: BigInt = {
+ this match {
+ case Empty => 0
+ case NonEmpty(_, t) => 1 + t.depth
+ }
+ }
+
+ def content: Set[BigInt] = {
+ this match {
+ case Empty => Set()
+ case NonEmpty(r, t) => r.content ++ t.content
+ }
+ }
+
+ def contains(v: BigInt): Boolean = {
+ this match {
+ case Empty => false
+ case NonEmpty(r, t) =>
+ if (r.min > v) false
+ else r.contains(v) || t.contains(v)
+ }
+ }
+
+ def isPackedSet = isSorted && isPacked
+
+ def isSorted: Boolean = {
+ this match {
+ case NonEmpty(r1, t @ NonEmpty(r2, _)) => r1 < r2 && t.isSorted
+ case _ => true
+ }
+ }
+
+ def isPacked: Boolean = {
+ this match {
+ case Empty => true
+ case NonEmpty(r, t) => r.size >= 1 && t.isPacked
+ }
+ }
+
+ def +(v: BigInt): PackedSet = {
+ require(this.isPackedSet)
+ this // TODO
+ } ensuring {
+ res => res.content == this.content ++ Set(v) &&
+ res.isPackedSet
+ }
+
+ def -(v: BigInt): PackedSet = {
+ require(this.isPackedSet)
+ this // TODO
+ } ensuring {
+ res => res.content == this.content -- Set(v) &&
+ res.isPackedSet
+ }
+
+ }
+ case class NonEmpty(r: Range, tail: PackedSet) extends PackedSet
+ case object Empty extends PackedSet
+
+
+}
diff --git a/testcases/web/synthesis/01_List_Insert.scala b/testcases/web/synthesis/01_List_Insert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..62e91d9b92c1d87008d1192f2f9e5c68580ef1ec
--- /dev/null
+++ b/testcases/web/synthesis/01_List_Insert.scala
@@ -0,0 +1,25 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Insert {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def insert(in1: List, v: BigInt) = {
+ choose { (out : List) =>
+ content(out) == content(in1) ++ Set(v)
+ }
+ }
+}
diff --git a/testcases/web/synthesis/02_List_Delete.scala b/testcases/web/synthesis/02_List_Delete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a548f46e2507bc4e95754bd1d512175260af1a49
--- /dev/null
+++ b/testcases/web/synthesis/02_List_Delete.scala
@@ -0,0 +1,25 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Delete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def delete(in1: List, v: BigInt) = {
+ choose { (out : List) =>
+ content(out) == content(in1) -- Set(v)
+ }
+ }
+}
diff --git a/testcases/web/synthesis/03_List_Union.scala b/testcases/web/synthesis/03_List_Union.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0b21dc0375c63b438f810acb9bdcd4f04ef25b36
--- /dev/null
+++ b/testcases/web/synthesis/03_List_Union.scala
@@ -0,0 +1,25 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Union {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def union(in1: List, in2: List) = {
+ choose { (out : List) =>
+ content(out) == content(in1) ++ content(in2)
+ }
+ }
+}
diff --git a/testcases/web/synthesis/04_List_Diff.scala b/testcases/web/synthesis/04_List_Diff.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0943955b170124ef788132a529ae0dd7ee9b55bb
--- /dev/null
+++ b/testcases/web/synthesis/04_List_Diff.scala
@@ -0,0 +1,38 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Diff {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def delete(in1: List, v: BigInt): List = {
+ in1 match {
+ case Cons(h,t) =>
+ if (h == v) {
+ delete(t, v)
+ } else {
+ Cons(h, delete(t, v))
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { content(_) == content(in1) -- Set(v) }
+
+ def diff(in1: List, in2: List) = {
+ choose { (out : List) =>
+ content(out) == content(in1) -- content(in2)
+ }
+ }
+}
diff --git a/testcases/web/synthesis/05_List_Split1.scala b/testcases/web/synthesis/05_List_Split1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..facbda843c5a6349cc6efca052bf104ec63f7156
--- /dev/null
+++ b/testcases/web/synthesis/05_List_Split1.scala
@@ -0,0 +1,30 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object List {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def abs(i: BigInt) : BigInt = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ def split(list: List): (List, List) = {
+ choose { (res: (List, List)) =>
+ (content(res._1) ++ content(res._2) == content(list))
+ }
+ }
+
+}
diff --git a/testcases/web/synthesis/06_List_Split2.scala b/testcases/web/synthesis/06_List_Split2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..38c07caf52566eb6f599e2557900b1ed83a53c37
--- /dev/null
+++ b/testcases/web/synthesis/06_List_Split2.scala
@@ -0,0 +1,31 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object List {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def abs(i: BigInt) : BigInt = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ def split(list: List): (List, List) = {
+ choose { (res : (List, List)) =>
+ (content(res._1) ++ content(res._2) == content(list)) &&
+ (abs(size(res._1) - size(res._2)) <= 1)
+ }
+ }
+
+}
diff --git a/testcases/web/synthesis/07_List_Split3.scala b/testcases/web/synthesis/07_List_Split3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..15c74190e1839abb484b375b28fea1582d8d58ea
--- /dev/null
+++ b/testcases/web/synthesis/07_List_Split3.scala
@@ -0,0 +1,36 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object List {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def abs(i: BigInt): BigInt = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ def tcons(h1: BigInt, h2: BigInt, tl: (List, List)) = {
+ (Cons(h1, tl._1), Cons(h2, tl._2))
+ }
+
+ def split(list : List): (List,List) = {
+ choose { (res: (List,List)) =>
+ (content(res._1) ++ content(res._2) == content(list)) &&
+ (abs(size(res._1) - size(res._2)) <= 1) &&
+ (size(res._1) + size(res._2) == size(list))
+ }
+ }
+
+}
diff --git a/testcases/web/synthesis/09_SortedList_Insert1.scala b/testcases/web/synthesis/09_SortedList_Insert1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..affc5b45512a0383b49d11ca2c008df3d28b8d06
--- /dev/null
+++ b/testcases/web/synthesis/09_SortedList_Insert1.scala
@@ -0,0 +1,34 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt) = {
+ require(isSorted(in1))
+ choose { (out: List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+ }
+ }
+
+}
diff --git a/testcases/web/synthesis/10_SortedList_Insert2.scala b/testcases/web/synthesis/10_SortedList_Insert2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e44eac286849ac69c19991168398ffad67726f5d
--- /dev/null
+++ b/testcases/web/synthesis/10_SortedList_Insert2.scala
@@ -0,0 +1,34 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt) = {
+ require(isSorted(in1))
+ choose { (out: List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out) && size(out) == size(in1) + 1
+ }
+ }
+
+}
diff --git a/testcases/web/synthesis/11_SortedList_Delete.scala b/testcases/web/synthesis/11_SortedList_Delete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..31305ca094ec78fa6896985fad04729879839baf
--- /dev/null
+++ b/testcases/web/synthesis/11_SortedList_Delete.scala
@@ -0,0 +1,33 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def delete(in1: List, v: BigInt) = {
+ require(isSorted(in1))
+ choose { (out: List) =>
+ (content(out) == content(in1) -- Set(v)) && isSorted(out)
+ }
+ }
+}
diff --git a/testcases/web/synthesis/12_SortedList_Diff.scala b/testcases/web/synthesis/12_SortedList_Diff.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9e4e32baeebb42ca25bd4dfec41e7b0303c80f53
--- /dev/null
+++ b/testcases/web/synthesis/12_SortedList_Diff.scala
@@ -0,0 +1,50 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def delete(in1: List, v: BigInt): List = {
+ require(isSorted(in1))
+ in1 match {
+ case Cons(h,t) =>
+ if (h < v) {
+ Cons(h, delete(t, v))
+ } else if (h == v) {
+ delete(t, v)
+ } else {
+ in1
+ }
+ case Nil =>
+ Nil
+ }
+ } ensuring { res => content(res) == content(in1) -- Set(v) && isSorted(res) }
+
+ def diff(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+ choose { (out: List) =>
+ (content(out) == content(in1) -- content(in2)) && isSorted(out)
+ }
+ }
+
+}
diff --git a/testcases/web/synthesis/13_SortedList_InsertSort.scala b/testcases/web/synthesis/13_SortedList_InsertSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8f5b78247b9877952f9a7e17cdf507f424d16b05
--- /dev/null
+++ b/testcases/web/synthesis/13_SortedList_InsertSort.scala
@@ -0,0 +1,51 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt): List = {
+ require(isSorted(in1))
+ in1 match {
+ case Cons(h, t) =>
+ if (v < h) {
+ Cons(v, in1)
+ } else if (v == h) {
+ in1
+ } else {
+ Cons(h, insert(t, v))
+ }
+ case Nil =>
+ Cons(v, Nil)
+ }
+
+ } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+ def sort(list: List): List = {
+ choose { (res: List) =>
+ isSorted(res) &&
+ content(list) == content(res)
+ }
+ }
+
+}
diff --git a/testcases/web/synthesis/14_SortedList_Union.scala b/testcases/web/synthesis/14_SortedList_Union.scala
new file mode 100644
index 0000000000000000000000000000000000000000..95d17bb61bb48927a2d189ccecf1b7330b4bb46e
--- /dev/null
+++ b/testcases/web/synthesis/14_SortedList_Union.scala
@@ -0,0 +1,50 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt): List = {
+ require(isSorted(in1))
+ in1 match {
+ case Cons(h, t) =>
+ if (v < h) {
+ Cons(v, in1)
+ } else if (v == h) {
+ in1
+ } else {
+ Cons(h, insert(t, v))
+ }
+ case Nil =>
+ Cons(v, Nil)
+ }
+
+ } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+ def union(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+ choose { (out: List) =>
+ (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ }
+ }
+}
diff --git a/testcases/web/synthesis/15_StrictSortedList_Insert.scala b/testcases/web/synthesis/15_StrictSortedList_Insert.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6c7543ad3847671bfc8657dc5c99e2bbd236ed93
--- /dev/null
+++ b/testcases/web/synthesis/15_StrictSortedList_Insert.scala
@@ -0,0 +1,34 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 >= x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt) = {
+ require(isSorted(in1))
+ choose { (out : List) =>
+ (content(out) == content(in1) ++ Set(v)) && isSorted(out)
+ }
+ }
+
+}
diff --git a/testcases/web/synthesis/16_StrictSortedList_Delete.scala b/testcases/web/synthesis/16_StrictSortedList_Delete.scala
new file mode 100644
index 0000000000000000000000000000000000000000..81827ed03b80beddf664e2b0c2beb62a43dad078
--- /dev/null
+++ b/testcases/web/synthesis/16_StrictSortedList_Delete.scala
@@ -0,0 +1,33 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Delete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 >= x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def delete(in1: List, v: BigInt) = {
+ require(isSorted(in1))
+ choose { (out : List) =>
+ (content(out) == content(in1) -- Set(v)) && isSorted(out)
+ }
+ }
+}
diff --git a/testcases/web/synthesis/17_StrictSortedList_Union.scala b/testcases/web/synthesis/17_StrictSortedList_Union.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cf2fcd727323d6b5c705522f3d37b884bdfd896d
--- /dev/null
+++ b/testcases/web/synthesis/17_StrictSortedList_Union.scala
@@ -0,0 +1,50 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Complete {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def content(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(_, Nil) => true
+ case Cons(x1, Cons(x2, _)) if(x1 >= x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def insert(in1: List, v: BigInt): List = {
+ require(isSorted(in1))
+ in1 match {
+ case Cons(h, t) =>
+ if (v < h) {
+ Cons(v, in1)
+ } else if (v == h) {
+ in1
+ } else {
+ Cons(h, insert(t, v))
+ }
+ case Nil =>
+ Cons(v, Nil)
+ }
+
+ } ensuring { res => (content(res) == content(in1) ++ Set(v)) && isSorted(res) }
+
+ def union(in1: List, in2: List) = {
+ require(isSorted(in1) && isSorted(in2))
+ choose { (out : List) =>
+ (content(out) == content(in1) ++ content(in2)) && isSorted(out)
+ }
+ }
+}
diff --git a/testcases/web/synthesis/18_UnaryNumerals_Add.scala b/testcases/web/synthesis/18_UnaryNumerals_Add.scala
new file mode 100644
index 0000000000000000000000000000000000000000..694f76a15a00b1fc666b372336f3d7baaa6b77d7
--- /dev/null
+++ b/testcases/web/synthesis/18_UnaryNumerals_Add.scala
@@ -0,0 +1,22 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Numerals {
+ sealed abstract class Num
+ case object Z extends Num
+ case class S(pred: Num) extends Num
+
+ def value(n: Num): BigInt = {
+ n match {
+ case Z => 0
+ case S(p) => 1 + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ def add(x: Num, y: Num): Num = {
+ choose { (r: Num) =>
+ value(r) == value(x) + value(y)
+ }
+ }
+}
diff --git a/testcases/web/synthesis/19_UnaryNumerals_Distinct.scala b/testcases/web/synthesis/19_UnaryNumerals_Distinct.scala
new file mode 100644
index 0000000000000000000000000000000000000000..827d8d70f8f5a860447897e86f62d5f5f19d529d
--- /dev/null
+++ b/testcases/web/synthesis/19_UnaryNumerals_Distinct.scala
@@ -0,0 +1,27 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Numerals {
+ sealed abstract class Num
+ case object Z extends Num
+ case class S(pred: Num) extends Num
+
+ def value(n: Num): BigInt = {
+ n match {
+ case Z => 0
+ case S(p) => 1 + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ def add(x: Num, y: Num): Num = (x match {
+ case Z => y
+ case S(p) => add(p, S(y))
+ }) ensuring (value(_) == value(x) + value(y))
+
+ def distinct(x: Num, y: Num): Num = {
+ choose { (r : Num) =>
+ r != x && r != y
+ }
+ }
+}
diff --git a/testcases/web/synthesis/20_UnaryNumerals_Mult.scala b/testcases/web/synthesis/20_UnaryNumerals_Mult.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1e58606d07d6bb78de617fa90d6129052007624b
--- /dev/null
+++ b/testcases/web/synthesis/20_UnaryNumerals_Mult.scala
@@ -0,0 +1,27 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Numerals {
+ sealed abstract class Num
+ case object Z extends Num
+ case class S(pred: Num) extends Num
+
+ def value(n: Num): BigInt = {
+ n match {
+ case Z => 0
+ case S(p) => 1 + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ def add(x: Num, y: Num): Num = (x match {
+ case Z => y
+ case S(p) => add(p, S(y))
+ }) ensuring (value(_) == value(x) + value(y))
+
+ def mult(x: Num, y: Num): Num = {
+ choose { (r: Num) =>
+ value(r) == value(x) * value(y)
+ }
+ }
+}
diff --git a/testcases/web/synthesis/21_UnaryNumerals_Squared.scala b/testcases/web/synthesis/21_UnaryNumerals_Squared.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d660c247ea4c68993dd4d59a7fc0f61e913935bc
--- /dev/null
+++ b/testcases/web/synthesis/21_UnaryNumerals_Squared.scala
@@ -0,0 +1,34 @@
+import leon.lang._
+import leon.lang.synthesis._
+import leon.annotation._
+
+object Numerals {
+ sealed abstract class Num
+ case object Z extends Num
+ case class S(pred: Num) extends Num
+
+ def value(n:Num) : BigInt = {
+ n match {
+ case Z => 0
+ case S(p) => 1 + value(p)
+ }
+ } ensuring (_ >= 0)
+
+ def add(x: Num, y: Num): Num = (x match {
+ case Z => y
+ case S(p) => add(p, S(y))
+ }) ensuring (value(_) == value(x) + value(y))
+
+ def mult(x: Num, y: Num): Num = (y match {
+ case S(p) =>
+ add(mult(x, p), x)
+ case Z =>
+ Z
+ }) ensuring { value(_) == value(x) * value(y) }
+
+ def squared(x: Num): Num = {
+ choose { (r: Num) =>
+ value(r) == value(x) * value(x)
+ }
+ }
+}
diff --git a/testcases/web/tutorials/01_Introduction.scala b/testcases/web/tutorials/01_Introduction.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ffe5264617df6bdf3a019c3afd197b4b2d6f5093
--- /dev/null
+++ b/testcases/web/tutorials/01_Introduction.scala
@@ -0,0 +1,94 @@
+import leon.Utils._
+
+/**
+ * Code should be contained in a single top-level object
+ */
+object Introduction {
+
+ /**
+ * You can define Algebraic Data Types using abstract classes and case classes.
+ */
+ abstract class Tree
+ case class Node(left: Tree, v: BigInt, right: Tree) extends Tree
+ case object Leaf extends Tree
+
+
+ /**
+ * You can define functions. Functions should be purely functionnal. Note
+ * that some imperative constructs such as 'var' or while loops will be handled.
+ */
+ def content(t: Tree): Set[BigInt] = t match {
+ case Node(l, v, r) => content(l) ++ content(r) ++ Set(v)
+ case Leaf => Set()
+ }
+
+ /**
+ * You can specify pre-conditions to a function using the "require" construct.
+ * You can use previously-defined functions in your precondition
+ */
+ def head(t: Tree) = {
+ require(t != Leaf)
+
+ val Node(_, v, _) = t
+
+ v
+ }
+
+
+ /**
+ * The following function uses head in unsafe ways:
+ *
+ * To verify a function, click on its name and select "verify". You can also
+ * hit Alt+v while within the body of a function.
+ *
+ * Verify whether test1, test2 and test3 are safe.
+ */
+
+ def simpleSorted(t: Tree) = {
+ require(t != Leaf)
+
+ val Node(l, v, r) = t
+
+ (head(l) < v) && (v < head(r))
+ }
+
+ /**
+ * You can specify post-conditions using "ensuring".
+ */
+ def contains(what: BigInt, t: Tree): Boolean = (t match {
+ case Leaf =>
+ false
+
+ case Node(l, v, r) =>
+ (v == what) || contains(what, l) || contains(what, r)
+
+ }) ensuring { res => res == (content(t) contains what) }
+
+ /**
+ * Can you spot the bug in this implementation of contains? Leon can.
+ */
+ def containsBuggy(what: BigInt, t: Tree): Boolean = (t match {
+ case Leaf =>
+ false
+
+ case Node(l, v, r) =>
+ (v == what) || contains(what, l) || contains(v, r)
+
+ }) ensuring { res => res == (content(t) contains what) }
+
+
+ /**
+ * Leon can also verify the completeness of the pattern matching:
+ */
+ def unsafeMatch(t: Tree) = t match {
+ case Node(l, v, r) if v == 0 =>
+ case Leaf =>
+ }
+
+ def unsafeHead(t: Tree) = {
+ val Node(_, v, _) = t // This translates to pattern matching
+
+ v
+ }
+
+}
diff --git a/testcases/web/tutorials/02_Ex1_Account.scala b/testcases/web/tutorials/02_Ex1_Account.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2001180737f5d0732fefb90ee8192d26165b6697
--- /dev/null
+++ b/testcases/web/tutorials/02_Ex1_Account.scala
@@ -0,0 +1,23 @@
+/*
+ Try to verify the toSavings function.
+ Use the returned counter-example to fix the precondition such that
+ Leon succeeds in showing the function correct.
+*/
+
+object Account2 {
+ sealed abstract class AccLike
+ case class Acc(checking : BigInt, savings : BigInt) extends AccLike
+
+ def toSavings(x : BigInt, a : Acc) : Acc = {
+ require (notRed(a) && a.checking >= x)
+ Acc(a.checking - x, a.savings + x)
+ } ensuring (res => (notRed(res) && sameTotal(a, res)))
+
+
+ def sameTotal(a1 : Acc, a2 : Acc) : Boolean = {
+ a1.checking + a1.savings == a2.checking + a2.savings
+ }
+ def notRed(a : Acc) : Boolean = {
+ a.checking >= 0 && a.savings >= 0
+ }
+}
diff --git a/testcases/web/tutorials/03_Ex2_Propositional_Logic.scala b/testcases/web/tutorials/03_Ex2_Propositional_Logic.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f5f1dd8eda867ec12166c5f461be928218d43a6a
--- /dev/null
+++ b/testcases/web/tutorials/03_Ex2_Propositional_Logic.scala
@@ -0,0 +1,74 @@
+import leon.Utils._
+import leon.Annotations._
+
+
+/*
+ Complete the two function stubs so that the simplify and nnf functions verify.
+*/
+
+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: BigInt) 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 {
+
+ }
+
+ 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 {
+
+ }
+
+ def evalLit(id : BigInt) : Boolean = (id == 42) // could be any function
+ def eval(f: Formula) : Boolean = f match {
+ case And(lhs, rhs) => eval(lhs) && eval(rhs)
+ case Or(lhs, rhs) => eval(lhs) || eval(rhs)
+ case Implies(lhs, rhs) => !eval(lhs) || eval(rhs)
+ case Not(f) => !eval(f)
+ case Literal(id) => evalLit(id)
+ }
+
+ @induct
+ def simplifySemantics(f: Formula) : Boolean = {
+ eval(f) == eval(simplify(f))
+ } holds
+
+ // Note that matching is exhaustive due to precondition.
+ def vars(f: Formula): Set[BigInt] = {
+ 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[BigInt](i)
+ case Literal(i) => Set[BigInt](i)
+ }
+ }
+
+
+}
diff --git a/testcases/web/tutorials/04_Ex3_List.scala b/testcases/web/tutorials/04_Ex3_List.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a49eba2cc66c1339a0d8e7a45448be801cb0ceed
--- /dev/null
+++ b/testcases/web/tutorials/04_Ex3_List.scala
@@ -0,0 +1,123 @@
+import leon.Annotations._
+import leon.Utils._
+
+/*
+ 1) Add pre- and postconditions, or fix the code such that the following
+ functions verify:
+ zip, sizesAreEquiv, reverse, concat0
+ The postconditions on these functions give what should be checked, i.e.
+ they should not be changed.
+
+ 2) find out what the function drunk does, and check provide a correct
+ postcondition that relates the sizes of the input list with the output list
+
+ 3) the function appendAssoc is meant to prove that the appending lists is
+ associative. Formulate this predicate and make sure Leon can verify it.
+*/
+
+object ListWithSize {
+ sealed abstract class List
+ case class Cons(head: BigInt, 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: BigInt, snd: BigInt) extends IntPair
+
+
+ def size(l: List) : BigInt = (l match {
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
+ })
+
+ def iplSize(l: IntPairList) : BigInt = (l match {
+ case IPNil() => 0
+ case IPCons(_, xs) => 1 + iplSize(xs)
+ })
+
+ // Verify
+ def zip(l1: List, l2: List) : IntPairList = {
+ 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 = {
+ l match {
+ case Nil() => acc
+ case Cons(_, xs) => sizeTailRecAcc(xs, acc+1)
+ }
+ }
+
+ // Verify
+ 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) == 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)))
+ }) // TODO: find postcondition
+
+
+ def funnyCons(x: BigInt, l: List) : List = (l match {
+ case Nil() => Cons(x, Nil())
+ case c @ Cons(_,_) => Cons(x, c)
+ }) ensuring(size(_) > 0)
+
+ // Verify
+ 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))
+ })
+
+ 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
+
+ // TODO: find predicate
+ //@induct
+ //def appendAssoc(xs : List, ys : List, zs : List) : Boolean =
+ // (...) 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(l2)
+ 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/testcases/web/tutorials/05_Ex4_InsertionSort.scala b/testcases/web/tutorials/05_Ex4_InsertionSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4ce5d723fa283cb31b790476203d15701e67cadf
--- /dev/null
+++ b/testcases/web/tutorials/05_Ex4_InsertionSort.scala
@@ -0,0 +1,62 @@
+import leon.Annotations._
+import leon.Utils._
+
+/*
+ Complete the code such that the sort function verifies.
+*/
+
+object InsertionSort {
+ sealed abstract class List
+ case class Cons(head:BigInt,tail:List) extends List
+ case class Nil() extends List
+
+ sealed abstract class OptInt
+ case class Some(value: BigInt) extends OptInt
+ case class None() extends OptInt
+
+ def size(l : List) : BigInt = (l match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + size(xs)
+ })
+
+ def contents(l: List): Set[BigInt] = l match {
+ case Nil() => Set.empty
+ case Cons(x,xs) => contents(xs) ++ Set(x)
+ }
+
+ def min(l : List) : OptInt = l match {
+ case Nil() => None()
+ case Cons(x, xs) => min(xs) match {
+ case None() => Some(x)
+ case Some(x2) => if(x < x2) Some(x) else Some(x2)
+ }
+ }
+
+ 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 sortedIns(e: BigInt, l: List): List = {
+ require(isSorted(l))
+ l match {
+ case Nil() => Cons(e,Nil())
+ case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
+ }
+ }
+
+
+ /* Insertion sort yields a sorted list of same size and content as the input
+ * list */
+ def sort(l: List): List = (l match {
+ case Nil() => Nil()
+ case Cons(x,xs) => sortedIns(x, sort(xs))
+ }) ensuring(res => contents(res) == contents(l)
+ && isSorted(res)
+ && size(res) == size(l)
+ )
+
+}
diff --git a/testcases/web/tutorials/06_Ex5_Add.scala b/testcases/web/tutorials/06_Ex5_Add.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e7245480c10733d5b7148b351e815b3f0f5a9681
--- /dev/null
+++ b/testcases/web/tutorials/06_Ex5_Add.scala
@@ -0,0 +1,29 @@
+import leon.Utils._
+
+/* VSTTE 2008 - Dafny paper */
+
+/*
+ Add the loop invariants so that Leon can verify this function.
+*/
+
+object Add {
+
+ def add(x : BigInt, y : BigInt): BigInt = ({
+ var r = x
+ if(y < 0) {
+ var n = y
+ (while(n != 0) {
+ r = r - 1
+ n = n + 1
+ }) //invariant(...)
+ } else {
+ var n = y
+ (while(n != 0) {
+ r = r + 1
+ n = n - 1
+ }) //invariant(...)
+ }
+ r
+ }) ensuring(_ == x+y)
+
+}
diff --git a/testcases/web/tutorials/07_Ex6_Mult.scala b/testcases/web/tutorials/07_Ex6_Mult.scala
new file mode 100644
index 0000000000000000000000000000000000000000..04bbcae47f23975bbc1137e385a2d1a2d3b9687e
--- /dev/null
+++ b/testcases/web/tutorials/07_Ex6_Mult.scala
@@ -0,0 +1,31 @@
+import leon.Utils._
+
+/* VSTTE 2008 - Dafny paper */
+
+/*
+ Add the loop invariants so that Leon can verify this function.
+*/
+
+object Mult {
+
+ def mult(x : BigInt, y : BigInt): BigInt = ({
+ var r = 0
+ if(y < 0) {
+ var n = y
+ (while(n != 0) {
+ r = r - x
+ n = n + 1
+ }) //invariant(...)
+ } else {
+ var n = y
+ (while(n != 0) {
+ r = r + x
+ n = n - 1
+ }) //invariant(...)
+ }
+ r
+ }) ensuring(_ == x*y)
+
+}
+
+
diff --git a/testcases/web/tutorials/08_Ex7_MaxSum.scala b/testcases/web/tutorials/08_Ex7_MaxSum.scala
new file mode 100644
index 0000000000000000000000000000000000000000..272dcc56adbf1673f5c6f38891744085801d3e9b
--- /dev/null
+++ b/testcases/web/tutorials/08_Ex7_MaxSum.scala
@@ -0,0 +1,43 @@
+import leon.Utils._
+
+/* VSTTE 2010 challenge 1 */
+
+/*
+ Find the loop invariant.
+*/
+
+
+object MaxSum {
+
+ def maxSum(a: Array[BigInt]): (BigInt, BigInt) = ({
+ 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, max)
+ }) ensuring(res => res._1 <= a.length * res._2)
+
+
+ def isPositive(a: Array[BigInt]): Boolean = {
+ require(a.length >= 0)
+ def rec(i: BigInt): Boolean = {
+ require(i >= 0)
+ if(i >= a.length)
+ true
+ else {
+ if(a(i) < 0)
+ false
+ else
+ rec(i+1)
+ }
+ }
+ rec(0)
+ }
+
+}
diff --git a/testcases/web/tutorials/09_Ex8_ListImp.scala b/testcases/web/tutorials/09_Ex8_ListImp.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4c10f9be1421f7c743d979ecb6b6163fdbc40371
--- /dev/null
+++ b/testcases/web/tutorials/09_Ex8_ListImp.scala
@@ -0,0 +1,53 @@
+import leon.Utils._
+
+/*
+ Find the loop invariants.
+*/
+
+object ListImp {
+
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case class Nil() extends List
+
+ def content(l: List) : Set[BigInt] = l match {
+ case Nil() => Set.empty[BigInt]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def size(l: List) : BigInt = {
+ var r = 0
+ (while(!l.isInstanceOf[Nil]) {
+ r = r+1
+ }) //invariant(...)
+ r
+ } ensuring(res => res >= 0)
+
+ def reverse(l: List): List = {
+ var r: List = Nil()
+ var l2: List = l
+
+ (while(!l2.isInstanceOf[Nil]) {
+ val Cons(head, tail) = l2
+ l2 = tail
+ r = Cons(head, r)
+ }) //invariant(...)
+
+ r
+ } ensuring(res => content(res) == content(l))
+
+ def append(l1 : List, l2 : List) : List = {
+ var r: List = l2
+ var tmp: List = reverse(l1)
+
+ (while(!tmp.isInstanceOf[Nil]) {
+ val Cons(head, tail) = tmp
+ tmp = tail
+ r = Cons(head, r)
+ }) //invariant(...)
+
+ r
+ } ensuring(content(_) == content(l1) ++ content(l2))
+
+
+}
diff --git a/testcases/web/tutorials/10_Ex9_RedBlackTree.scala b/testcases/web/tutorials/10_Ex9_RedBlackTree.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9dd7ad92bfbcfd18fc629468cab0aa81b05baa06
--- /dev/null
+++ b/testcases/web/tutorials/10_Ex9_RedBlackTree.scala
@@ -0,0 +1,100 @@
+import leon.Annotations._
+import leon.Utils._
+
+/*
+ You found an implementation of a Red-black tree and you want to verify that
+ the add method does the correct thing.
+ The only additional specification you should need is for the ins method.
+*/
+
+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 OptionInt
+ case class Some(v : BigInt) extends OptionInt
+ case class None() extends OptionInt
+
+ 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() => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* 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) : BigInt = 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: BigInt, t: Tree): Tree = {
+ //require(...)
+ 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 => )*/
+
+ 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: BigInt, 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 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))
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)))
+}
diff --git a/testcases/web/tutorials/11_Ex10_SearchLinkedList.scala b/testcases/web/tutorials/11_Ex10_SearchLinkedList.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f8ca2076af6f8803c986f1aaf0ef53e27fb15ea9
--- /dev/null
+++ b/testcases/web/tutorials/11_Ex10_SearchLinkedList.scala
@@ -0,0 +1,47 @@
+import leon.Utils._
+import leon.Annotations._
+
+/*
+ Add the missing postcondition.
+*/
+
+
+object SearchLinkedList {
+ sealed abstract class List
+ case class Cons(head : BigInt, tail : List) extends List
+ case class Nil() extends List
+
+ def size(list : List) : BigInt = (list match {
+ case Nil() => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def contains(list : List, elem : BigInt) : Boolean = (list match {
+ case Nil() => false
+ case Cons(x, xs) => x == elem || contains(xs, elem)
+ })
+
+ def firstZero(list : List) : BigInt = (list match {
+ case Nil() => 0
+ case Cons(x, xs) => if (x == 0) 0 else firstZero(xs) + 1
+ }) /*ensuring (res => )*/
+
+ 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 : BigInt) : Boolean = {
+ if(firstZero(list) == i) {
+ if(contains(list, 0)) {
+ firstZeroAtPos(list, i)
+ } else {
+ i == size(list)
+ }
+ } else {
+ true
+ }
+ } holds
+}
diff --git a/testcases/web/verification/01_Amortized_Queue.scala b/testcases/web/verification/01_Amortized_Queue.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e8190385a15d2bba453571671778d1e01850eeb0
--- /dev/null
+++ b/testcases/web/verification/01_Amortized_Queue.scala
@@ -0,0 +1,102 @@
+import leon.lang._
+import leon.annotation._
+
+object AmortizedQueue {
+ sealed abstract class List
+ case class Cons(head : BigInt, tail : List) extends List
+ case object Nil extends List
+
+ sealed abstract class AbsQueue
+ case class Queue(front : List, rear : List) extends AbsQueue
+
+ def size(list : List) : BigInt = (list match {
+ case Nil => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def content(l: List) : Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def asList(queue : AbsQueue) : List = queue match {
+ case Queue(front, rear) => concat(front, reverse(rear))
+ }
+
+ def concat(l1 : List, l2 : List) : List = (l1 match {
+ case Nil => l2
+ case Cons(x,xs) => Cons(x, concat(xs, l2))
+ }) ensuring (res => size(res) == size(l1) + size(l2) && content(res) == content(l1) ++ content(l2))
+
+ def isAmortized(queue : AbsQueue) : Boolean = queue match {
+ case Queue(front, rear) => size(front) >= size(rear)
+ }
+
+ def isEmpty(queue : AbsQueue) : Boolean = queue match {
+ case Queue(Nil, Nil) => true
+ case _ => false
+ }
+
+ def reverse(l : List) : List = (l match {
+ case Nil => Nil
+ case Cons(x, xs) => concat(reverse(xs), Cons(x, Nil))
+ }) ensuring (content(_) == content(l))
+
+ def amortizedQueue(front : List, rear : List) : AbsQueue = {
+ if (size(rear) <= size(front))
+ Queue(front, rear)
+ else
+ Queue(concat(front, reverse(rear)), Nil)
+ } ensuring(isAmortized(_))
+
+ def enqueue(queue : AbsQueue, elem : BigInt) : AbsQueue = (queue match {
+ case Queue(front, rear) => amortizedQueue(front, Cons(elem, rear))
+ }) ensuring(isAmortized(_))
+
+ def tail(queue : AbsQueue) : AbsQueue = {
+ require(isAmortized(queue) && !isEmpty(queue))
+ queue match {
+ case Queue(Cons(f, fs), rear) => amortizedQueue(fs, rear)
+ }
+ } ensuring (isAmortized(_))
+
+ def front(queue : AbsQueue) : BigInt = {
+ require(isAmortized(queue) && !isEmpty(queue))
+ queue match {
+ case Queue(Cons(f, _), _) => f
+ }
+ }
+
+ @induct
+ def propFront(queue : AbsQueue, list : List, elem : BigInt) : Boolean = {
+ require(!isEmpty(queue) && isAmortized(queue))
+ if (asList(queue) == list) {
+ list match {
+ case Cons(x, _) => front(queue) == x
+ }
+ } else
+ true
+ } holds
+
+ def enqueueAndFront(queue : AbsQueue, elem : BigInt) : Boolean = {
+ if (isEmpty(queue))
+ front(enqueue(queue, elem)) == elem
+ else
+ true
+ } holds
+
+ def enqueueDequeueThrice(queue : AbsQueue, e1 : BigInt, e2 : BigInt, e3 : BigInt) : Boolean = {
+ if (isEmpty(queue)) {
+ val q1 = enqueue(queue, e1)
+ val q2 = enqueue(q1, e2)
+ val q3 = enqueue(q2, e3)
+ val e1prime = front(q3)
+ val q4 = tail(q3)
+ val e2prime = front(q4)
+ val q5 = tail(q4)
+ val e3prime = front(q5)
+ e1 == e1prime && e2 == e2prime && e3 == e3prime
+ } else
+ true
+ } holds
+}
diff --git a/testcases/web/verification/02_Associative_List.scala b/testcases/web/verification/02_Associative_List.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7dea8f3edb778457621606bb13907d6d5ac24977
--- /dev/null
+++ b/testcases/web/verification/02_Associative_List.scala
@@ -0,0 +1,49 @@
+import leon.lang._
+import leon.annotation._
+
+object AssociativeList {
+ sealed abstract class KeyValuePairAbs
+ case class KeyValuePair(key: BigInt, value: BigInt) extends KeyValuePairAbs
+
+ sealed abstract class List
+ case class Cons(head: KeyValuePairAbs, tail: List) extends List
+ case object Nil extends List
+
+ sealed abstract class OptionInt
+ case class Some(i: BigInt) extends OptionInt
+ case object None extends OptionInt
+
+ def domain(l: List): Set[BigInt] = l match {
+ case Nil => Set.empty[BigInt]
+ case Cons(KeyValuePair(k,_), xs) => Set(k) ++ domain(xs)
+ }
+
+ def find(l: List, e: BigInt): OptionInt = l match {
+ case Nil => None
+ case Cons(KeyValuePair(k, v), xs) => if (k == e) Some(v) else find(xs, e)
+ }
+
+ def noDuplicates(l: List): Boolean = l match {
+ case Nil => true
+ case Cons(KeyValuePair(k, v), xs) => find(xs, k) == None && noDuplicates(xs)
+ }
+
+ def updateList(l1: List, l2: List): List = (l2 match {
+ case Nil => l1
+ case Cons(x, xs) => updateList(updateElem(l1, x), xs)
+ }) ensuring(domain(_) == domain(l1) ++ domain(l2))
+
+ def updateElem(l: List, e: KeyValuePairAbs): List = (l match {
+ case Nil => Cons(e, Nil)
+ case Cons(KeyValuePair(k, v), xs) => e match {
+ case KeyValuePair(ek, ev) => if (ek == k) Cons(KeyValuePair(ek, ev), xs) else Cons(KeyValuePair(k, v), updateElem(xs, e))
+ }
+ }) ensuring(res => e match {
+ case KeyValuePair(k, v) => domain(res) == domain(l) ++ Set[BigInt](k)
+ })
+
+ @induct
+ def readOverWrite(l: List, k1: BigInt, k2: BigInt, e: BigInt) : Boolean = {
+ find(updateElem(l, KeyValuePair(k2,e)), k1) == (if (k1 == k2) Some(e) else find(l, k1))
+ } holds
+}
diff --git a/testcases/web/verification/03_Insertion_Sort.scala b/testcases/web/verification/03_Insertion_Sort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a3a81d75338fdb5456664ce4e663101deb4cce02
--- /dev/null
+++ b/testcases/web/verification/03_Insertion_Sort.scala
@@ -0,0 +1,78 @@
+import leon.lang._
+import leon.annotation._
+
+object InsertionSort {
+ sealed abstract class List
+ case class Cons(head:BigInt,tail:List) extends List
+ case object Nil extends List
+
+ sealed abstract class OptInt
+ case class Some(value: BigInt) extends OptInt
+ case object None extends OptInt
+
+ def size(l : List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def contents(l: List): Set[BigInt] = 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 sortedIns(e: BigInt, l: List): List = {
+ require(isSorted(l))
+ l match {
+ case Nil => Cons(e,Nil)
+ case Cons(x,xs) => if (x <= e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
+ }
+ } ensuring(res => contents(res) == contents(l) ++ Set(e)
+ && isSorted(res)
+ && size(res) == size(l) + 1
+ )
+
+ /* A counterexample is found when we forget to specify the precondition */
+ def buggySortedIns(e: BigInt, l: List): List = {
+ 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
+ )
+
+ /* Insertion sort yields a sorted list of same size and content as the input
+ * list */
+ def sort(l: List): List = (l match {
+ case Nil => Nil
+ case Cons(x,xs) => sortedIns(x, sort(xs))
+ }) ensuring(res => contents(res) == contents(l)
+ && isSorted(res)
+ && size(res) == size(l)
+ )
+
+ /* Merges one (unsorted) list into another, sorted, list. */
+ def mergeInto(l1 : List, l2 : List) : List = {
+ require(isSorted(l2))
+ l1 match {
+ case Nil => l2
+ case Cons(x, xs) => mergeInto(xs, sortedIns(x, l2))
+ }
+ } ensuring(res => contents(res) == contents(l1) ++ contents(l2) && isSorted(res))
+
+ def main(args: Array[String]): Unit = {
+ val ls: List = Cons(5, Cons(2, Cons(4, Cons(5, Cons(1, Cons(8,Nil))))))
+
+ println(ls)
+ println(sort(ls))
+ }
+}
diff --git a/testcases/web/verification/04_List_Operations.scala b/testcases/web/verification/04_List_Operations.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f7e6d590c25882d51a51191547b03b3996dad8d1
--- /dev/null
+++ b/testcases/web/verification/04_List_Operations.scala
@@ -0,0 +1,106 @@
+import leon.lang._
+import leon.annotation._
+
+object ListOperations {
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case object Nil extends List
+
+ sealed abstract class IntPairList
+ case class IPCons(head: IntPair, tail: IntPairList) extends IntPairList
+ case object IPNil extends IntPairList
+
+ sealed abstract class IntPair
+ case class IP(fst: BigInt, snd: BigInt) extends IntPair
+
+ def size(l: List) : BigInt = (l match {
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
+ }) ensuring(res => res >= 0)
+
+ def iplSize(l: IntPairList) : BigInt = (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) : 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) == 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/testcases/web/verification/05_Propositional_Logic.scala b/testcases/web/verification/05_Propositional_Logic.scala
new file mode 100644
index 0000000000000000000000000000000000000000..455cef7ec5201fd17edee71059dc38c9d7afa3d8
--- /dev/null
+++ b/testcases/web/verification/05_Propositional_Logic.scala
@@ -0,0 +1,99 @@
+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: BigInt) 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) => nnf(Or(Not(lhs), 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) => false
+ case Not(Literal(_)) => true
+ case Not(_) => false
+ case Literal(_) => true
+ }
+
+ def evalLit(id : BigInt) : Boolean = (id == 42) // could be any function
+ def eval(f: Formula) : Boolean = f match {
+ case And(lhs, rhs) => eval(lhs) && eval(rhs)
+ case Or(lhs, rhs) => eval(lhs) || eval(rhs)
+ case Implies(lhs, rhs) => !eval(lhs) || eval(rhs)
+ case Not(f) => !eval(f)
+ case Literal(id) => evalLit(id)
+ }
+
+ @induct
+ def simplifySemantics(f: Formula) : Boolean = {
+ eval(f) == eval(simplify(f))
+ } holds
+
+ // Note that matching is exhaustive due to precondition.
+ def vars(f: Formula): Set[BigInt] = {
+ require(isNNF(f))
+ f match {
+ case And(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Or(lhs, rhs) => vars(lhs) ++ vars(rhs)
+ case Not(Literal(i)) => Set[BigInt](i)
+ case Literal(i) => Set[BigInt](i)
+ }
+ }
+
+ def fv(f : Formula) = { vars(nnf(f)) }
+
+ @induct
+ def wrongCommutative(f: Formula) : Boolean = {
+ nnf(simplify(f)) == simplify(nnf(f))
+ } holds
+
+ @induct
+ def simplifyPreservesNNF(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/testcases/web/verification/06_Red-Black_Tree.scala b/testcases/web/verification/06_Red-Black_Tree.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3adc6c8cb60135e6465d1f13da87a8baca24ce61
--- /dev/null
+++ b/testcases/web/verification/06_Red-Black_Tree.scala
@@ -0,0 +1,115 @@
+import leon.lang._
+import leon.annotation._
+
+object RedBlackTree {
+ sealed abstract class Color
+ case object Red extends Color
+ case object Black extends Color
+
+ sealed abstract class Tree
+ case object Empty extends Tree
+ case class Node(color: Color, left: Tree, value: BigInt, right: Tree) extends Tree
+
+ sealed abstract class OptionInt
+ case class Some(v : BigInt) extends OptionInt
+ case object None extends OptionInt
+
+ 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 => 0
+ case Node(_, l, v, r) => size(l) + 1 + size(r)
+ }
+
+ /* 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) : BigInt = 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: 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 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: BigInt, 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: BigInt, 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: 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)))
+
+ 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))
+ }
+ } ensuring (res => content(res) == content(Node(c,a,x,b)))
+}
diff --git a/testcases/web/verification/07_Search_Linked-List.scala b/testcases/web/verification/07_Search_Linked-List.scala
new file mode 100644
index 0000000000000000000000000000000000000000..16f1c550e6c620bce328e2ec31e5312838af0cfc
--- /dev/null
+++ b/testcases/web/verification/07_Search_Linked-List.scala
@@ -0,0 +1,47 @@
+import leon.lang._
+import leon.annotation._
+
+object SearchLinkedList {
+ sealed abstract class List
+ case class Cons(head : BigInt, tail : List) extends List
+ case object Nil extends List
+
+ def size(list : List) : BigInt = (list match {
+ case Nil => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def contains(list : List, elem : BigInt) : Boolean = (list match {
+ case Nil => false
+ case Cons(x, xs) => x == elem || contains(xs, elem)
+ })
+
+ def firstZero(list : List) : BigInt = (list match {
+ case Nil => 0
+ case Cons(x, xs) => if (x == 0) 0 else firstZero(xs) + 1
+ }) ensuring (res =>
+ res >= 0 && (if (contains(list, 0)) {
+ firstZeroAtPos(list, res)
+ } else {
+ res == size(list)
+ }))
+
+ 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 : BigInt) : Boolean = {
+ if(firstZero(list) == i) {
+ if(contains(list, 0)) {
+ firstZeroAtPos(list, i)
+ } else {
+ i == size(list)
+ }
+ } else {
+ true
+ }
+ } holds
+}
diff --git a/testcases/web/verification/08_Sum_and_Max.scala b/testcases/web/verification/08_Sum_and_Max.scala
new file mode 100644
index 0000000000000000000000000000000000000000..24d279515cdbc7fe7d3e3f6f056be53d25df61eb
--- /dev/null
+++ b/testcases/web/verification/08_Sum_and_Max.scala
@@ -0,0 +1,46 @@
+import leon.lang._
+import leon.annotation._
+
+object SumAndMax {
+ sealed abstract class List
+ case class Cons(head : BigInt, tail : List) extends List
+ case object Nil extends List
+
+ def max(list : List) : BigInt = {
+ require(list != Nil)
+ list match {
+ case Cons(x, Nil) => x
+ case Cons(x, xs) => {
+ val m2 = max(xs)
+ if(m2 > x) m2 else x
+ }
+ }
+ }
+
+ def sum(list : List) : BigInt = list match {
+ case Nil => 0
+ case Cons(x, xs) => x + sum(xs)
+ }
+
+ def size(list : List) : BigInt = (list match {
+ case Nil => 0
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def allPos(list : List) : Boolean = list match {
+ case Nil => true
+ case Cons(x, xs) => x >= 0 && allPos(xs)
+ }
+
+ def prop0(list : List) : Boolean = {
+ require(list != Nil)
+ !allPos(list) || max(list) >= 0
+ } holds
+
+ @induct
+ def property(list : List) : Boolean = {
+ // This precondition was given in the problem but isn't actually useful :D
+ // require(allPos(list))
+ sum(list) <= size(list) * (if(list == Nil) 0 else max(list))
+ } holds
+}
diff --git a/testcases/web/verification/09_Heap.scala b/testcases/web/verification/09_Heap.scala
new file mode 100644
index 0000000000000000000000000000000000000000..aa66ca2f2a5e40ce80165a9cf0f0db8e00aa4d43
--- /dev/null
+++ b/testcases/web/verification/09_Heap.scala
@@ -0,0 +1,147 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.annotation._
+import leon.lang._
+
+object Heaps {
+ /*~~~~~~~~~~~~~~~~~~~~~~~*/
+ /* Data type definitions */
+ /*~~~~~~~~~~~~~~~~~~~~~~~*/
+ private case class Node(rank : BigInt, elem : Int, 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 object None extends OptInt
+
+ /*~~~~~~~~~~~~~~~~~~~~~~~*/
+ /* Abstraction functions */
+ /*~~~~~~~~~~~~~~~~~~~~~~~*/
+ def heapContent(h : Heap) : Set[Int] = h match {
+ case Empty => Set.empty[Int]
+ case Nodes(n, ns) => nodeContent(n) ++ heapContent(ns)
+ }
+
+ def nodeContent(n : Node) : Set[Int] = n match {
+ case Node(_, e, h) => Set(e) ++ heapContent(h)
+ }
+
+ /*~~~~~~~~~~~~~~~~~~~~~~~~*/
+ /* Helper/local functions */
+ /*~~~~~~~~~~~~~~~~~~~~~~~~*/
+ private def reverse(h : Heap) : Heap = reverse0(h, Empty)
+ private def reverse0(h : Heap, acc : Heap) : Heap = (h match {
+ case Empty => acc
+ case Nodes(n, ns) => reverse0(ns, Nodes(n, acc))
+ }) ensuring(res => heapContent(res) == heapContent(h) ++ heapContent(acc))
+
+ private def link(t1 : Node, t2 : Node) = (t1, t2) match {
+ case (Node(r, e1, ns1), Node(_, e2, ns2)) =>
+ if(e1 <= e2) {
+ Node(r + 1, e1, Nodes(t2, ns1))
+ } else {
+ Node(r + 1, e2, Nodes(t1, ns2))
+ }
+ }
+
+ private def insertNode(t : Node, h : Heap) : Heap = (h match {
+ case Empty => Nodes(t, Empty)
+ case Nodes(t2, h2) =>
+ if(t.rank < t2.rank) {
+ Nodes(t, h)
+ } else {
+ insertNode(link(t, t2), h2)
+ }
+ }) ensuring(res => heapContent(res) == nodeContent(t) ++ heapContent(h))
+
+ private def getMin(h : Heap) : (Node, Heap) = {
+ require(h != Empty)
+ h match {
+ case Nodes(t, Empty) => (t, Empty)
+ case Nodes(t, ts) =>
+ val (t0, ts0) = getMin(ts)
+ if(t.elem < t0.elem) {
+ (t, ts)
+ } else {
+ (t0, Nodes(t, ts0))
+ }
+ }
+ } ensuring(_ match {
+ case (n,h2) => nodeContent(n) ++ heapContent(h2) == heapContent(h)
+ })
+
+ /*~~~~~~~~~~~~~~~~*/
+ /* Heap interface */
+ /*~~~~~~~~~~~~~~~~*/
+ def empty() : Heap = {
+ Empty
+ } ensuring(res => heapContent(res) == Set.empty[Int])
+
+ def isEmpty(h : Heap) : Boolean = {
+ (h == Empty)
+ } ensuring(res => res == (heapContent(h) == Set.empty[Int]))
+
+ def insert(e : Int, h : Heap) : Heap = {
+ insertNode(Node(0, e, Empty), h)
+ } ensuring(res => heapContent(res) == heapContent(h) ++ Set(e))
+
+ def merge(h1 : Heap, h2 : Heap) : Heap = ((h1,h2) match {
+ case (_, Empty) => h1
+ case (Empty, _) => h2
+ case (Nodes(t1, ts1), Nodes(t2, ts2)) =>
+ if(t1.rank < t2.rank) {
+ Nodes(t1, merge(ts1, h2))
+ } else if(t2.rank < t1.rank) {
+ Nodes(t2, merge(h1, ts2))
+ } else {
+ insertNode(link(t1, t2), merge(ts1, ts2))
+ }
+ }) ensuring(res => heapContent(res) == heapContent(h1) ++ heapContent(h2))
+
+ def findMin(h : Heap) : OptInt = (h match {
+ case Empty => None
+ case Nodes(Node(_, e, _), ns) =>
+ findMin(ns) match {
+ case None => Some(e)
+ case Some(e2) => Some(if(e < e2) e else e2)
+ }
+ }) ensuring(_ match {
+ case None => isEmpty(h)
+ case Some(v) => heapContent(h).contains(v)
+ })
+
+ def deleteMin(h : Heap) : Heap = (h match {
+ case Empty => Empty
+ case ts : Nodes =>
+ val (Node(_, e, ns1), ns2) = getMin(ts)
+ merge(reverse(ns1), ns2)
+ }) ensuring(res => heapContent(res).subsetOf(heapContent(h)))
+
+ def sanity0() : Boolean = {
+ val h0 : Heap = Empty
+ val h1 = insert(42, h0)
+ val h2 = insert(72, h1)
+ val h3 = insert(0, h2)
+ findMin(h0) == None &&
+ findMin(h1) == Some(42) &&
+ findMin(h2) == Some(42) &&
+ findMin(h3) == Some(0)
+ }.holds
+
+ def sanity1() : Boolean = {
+ val h0 = insert(42, Empty)
+ val h1 = insert(0, Empty)
+ val h2 = merge(h0, h1)
+ findMin(h2) == Some(0)
+ }.holds
+
+ def sanity3() : Boolean = {
+ val h0 = insert(42, insert(0, insert(12, Empty)))
+ val h1 = deleteMin(h0)
+ findMin(h1) == Some(12)
+ }.holds
+}
+
diff --git a/testcases/web/verification/10_FoldAssociative.scala b/testcases/web/verification/10_FoldAssociative.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ff0444f269dd6f9b2a2b7f2b54e13f54c6755ab2
--- /dev/null
+++ b/testcases/web/verification/10_FoldAssociative.scala
@@ -0,0 +1,103 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon._
+import leon.lang._
+
+object FoldAssociative {
+
+ sealed abstract class List
+ case class Cons(head: Int, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class Option
+ case class Some(x: Int) extends Option
+ case class None() extends Option
+
+ def foldRight[A](list: List, state: A, f: (Int, A) => A): A = list match {
+ case Cons(head, tail) =>
+ val tailState = foldRight(tail, state, f)
+ f(head, tailState)
+ case Nil() => state
+ }
+
+ def take(list: List, count: Int): List = {
+ require(count >= 0)
+ list match {
+ case Cons(head, tail) if count > 0 => Cons(head, take(tail, count - 1))
+ case _ => Nil()
+ }
+ }
+
+ def drop(list: List, count: Int): List = {
+ require(count >= 0)
+ list match {
+ case Cons(head, tail) if count > 0 => drop(tail, count - 1)
+ case _ => list
+ }
+ }
+
+ def append(l1: List, l2: List): List = {
+ l1 match {
+ case Cons(head, tail) => Cons(head, append(tail, l2))
+ case Nil() => l2
+ }
+ }
+
+ def lemma_split(list: List, x: Int): Boolean = {
+ require(x >= 0)
+ val f = (x: Int, s: Int) => x + s
+ val l1 = take(list, x)
+ val l2 = drop(list, x)
+ foldRight(list, 0, f) == foldRight(l1, foldRight(l2, 0, f), f)
+ }
+
+ def lemma_split_induct(list: List, x: Int): Boolean = {
+ require(x >= 0)
+ val f = (x: Int, s: Int) => x + s
+ val l1 = take(list, x)
+ val l2 = drop(list, x)
+ lemma_split(list, x) && (list match {
+ case Cons(head, tail) if x > 0 =>
+ lemma_split_induct(tail, x - 1)
+ case _ => true
+ })
+ }.holds
+
+ def lemma_reassociative(list: List, x: Int): Boolean = {
+ require(x >= 0)
+ val f = (x: Int, s: Int) => x + s
+ val l1 = take(list, x)
+ val l2 = drop(list, x)
+
+ foldRight(list, 0, f) == foldRight(l1, 0, f) + foldRight(l2, 0, f)
+ }
+
+ def lemma_reassociative_induct(list: List, x: Int): Boolean = {
+ require(x >= 0)
+ val f = (x: Int, s: Int) => x + s
+ val l1 = take(list, x)
+ val l2 = drop(list, x)
+ lemma_reassociative(list, x) && (list match {
+ case Cons(head, tail) if x > 0 =>
+ lemma_reassociative_induct(tail, x - 1)
+ case _ => true
+ })
+ }.holds
+
+ def lemma_reassociative_presplit(l1: List, l2: List): Boolean = {
+ val f = (x: Int, s: Int) => x + s
+ val list = append(l1, l2)
+ foldRight(list, 0, f) == foldRight(l1, 0, f) + foldRight(l2, 0, f)
+ }
+
+ def lemma_reassociative_presplit_induct(l1: List, l2: List): Boolean = {
+ val f = (x: Int, s: Int) => x + s
+ val list = append(l1, l2)
+ lemma_reassociative_presplit(l1, l2) && (l1 match {
+ case Cons(head, tail) =>
+ lemma_reassociative_presplit_induct(tail, l2)
+ case Nil() => true
+ })
+ }.holds
+
+}
diff --git a/testcases/web/verification/11_MergeSort.scala b/testcases/web/verification/11_MergeSort.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9a1cb71fe0368c6b2ef6021b4f11a2eac961fea5
--- /dev/null
+++ b/testcases/web/verification/11_MergeSort.scala
@@ -0,0 +1,122 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.annotation._
+import leon.lang._
+
+object MergeSort {
+ // Data types
+ sealed abstract class List
+ case class Cons(head : Int, 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]
+ case Cons(x, xs) => Set(x) ++ content(xs)
+ }
+
+ def lContent(llist : LList) : Set[Int] = llist match {
+ case LNil() => Set.empty[Int]
+ case LCons(x, xs) => content(x) ++ lContent(xs)
+ }
+
+ def size(list : List) : BigInt = (list match {
+ case Nil() => BigInt(0)
+ case Cons(_, xs) => 1 + size(xs)
+ }) ensuring(_ >= 0)
+
+ def isSorted(list : List) : Boolean = list match {
+ case Nil() => true
+ case Cons(_, Nil()) => true
+ case Cons(x1, Cons(x2, _)) if(x1 > x2) => false
+ case Cons(_, xs) => isSorted(xs)
+ }
+
+ def lIsSorted(llist : LList) : Boolean = llist match {
+ case LNil() => true
+ case LCons(x, xs) => isSorted(x) && lIsSorted(xs)
+ }
+
+ def abs(i : BigInt) : BigInt = {
+ if(i < 0) -i else i
+ } ensuring(_ >= 0)
+
+ def mergeSpec(list1 : List, list2 : List, res : List) : Boolean = {
+ isSorted(res) && content(res) == content(list1) ++ content(list2)
+ }
+
+ def mergeFast(list1 : List, list2 : List) : List = {
+ require(isSorted(list1) && isSorted(list2))
+
+ (list1, list2) match {
+ case (_, Nil()) => list1
+ case (Nil(), _) => list2
+ case (Cons(x, xs), Cons(y, ys)) =>
+ if(x <= y) {
+ Cons(x, mergeFast(xs, list2))
+ } else {
+ Cons(y, mergeFast(list1, ys))
+ }
+ }
+ } ensuring(res => mergeSpec(list1, list2, res))
+
+ def splitSpec(list : List, res : (List,List)) : Boolean = {
+ val s1 = size(res._1)
+ val s2 = size(res._2)
+ abs(s1 - s2) <= 1 && s1 + s2 == size(list) &&
+ content(res._1) ++ content(res._2) == content(list)
+ }
+
+ def split(list : List) : (List,List) = (list match {
+ case Nil() => (Nil(), Nil())
+ case Cons(x, Nil()) => (Cons(x, Nil()), Nil())
+ case Cons(x1, Cons(x2, xs)) =>
+ val (s1,s2) = split(xs)
+ (Cons(x1, s1), Cons(x2, s2))
+ }) ensuring(res => splitSpec(list, res))
+
+ def sortSpec(in : List, out : List) : Boolean = {
+ content(out) == content(in) && isSorted(out)
+ }
+
+ // Not really quicksort, neither mergesort.
+ def weirdSort(in : List) : List = (in match {
+ case Nil() => Nil()
+ case Cons(x, Nil()) => Cons(x, Nil())
+ case _ =>
+ val (s1,s2) = split(in)
+ mergeFast(weirdSort(s1), weirdSort(s2))
+ }) ensuring(res => sortSpec(in, res))
+
+ def toLList(list : List) : LList = (list match {
+ case Nil() => LNil()
+ case Cons(x, xs) => LCons(Cons(x, Nil()), toLList(xs))
+ }) ensuring(res => lContent(res) == content(list) && lIsSorted(res))
+
+ def mergeMap(llist : LList) : LList = {
+ require(lIsSorted(llist))
+
+ llist match {
+ case LNil() => LNil()
+ case o @ LCons(x, LNil()) => o
+ case LCons(x, LCons(y, ys)) => LCons(mergeFast(x, y), mergeMap(ys))
+ }
+ } ensuring(res => lContent(res) == lContent(llist) && lIsSorted(res))
+
+ def mergeReduce(llist : LList) : List = {
+ require(lIsSorted(llist))
+
+ llist match {
+ case LNil() => Nil()
+ case LCons(x, LNil()) => x
+ case _ => mergeReduce(mergeMap(llist))
+ }
+ } ensuring(res => content(res) == lContent(llist) && isSorted(res))
+
+ def mergeSort(in : List) : List = {
+ mergeReduce(toLList(in))
+ } ensuring(res => sortSpec(in, res))
+}
diff --git a/testcases/web/verification/12_ParBalance.scala b/testcases/web/verification/12_ParBalance.scala
new file mode 100644
index 0000000000000000000000000000000000000000..d1ddfd3f69baee993c9e01a622217236e27226ca
--- /dev/null
+++ b/testcases/web/verification/12_ParBalance.scala
@@ -0,0 +1,208 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon._
+import leon.lang._
+
+object ParBalance {
+
+ sealed abstract class List
+ case class Cons(head: BigInt, tail: List) extends List
+ case class Nil() extends List
+
+ sealed abstract class Option
+ case class Some(x: BigInt) extends Option
+ case class None() extends Option
+
+ val openPar : BigInt = BigInt(1)
+ val closePar : BigInt = BigInt(2)
+
+ def balanced(list: List, counter: BigInt): Boolean = {
+ if (counter < 0) false else list match {
+ case Cons(head, tail) =>
+ val c = if (head == openPar) counter + 1
+ else if (head == closePar) counter - 1
+ else counter
+ balanced(tail, c)
+ case Nil() => counter == 0
+ }
+ }
+
+ def balanced_nonEarly(list: List, counter: BigInt): Boolean = {
+ list match {
+ case Cons(head, tail) =>
+ if (counter < 0) balanced_nonEarly(tail, counter) else {
+ val c = if (head == openPar) counter + 1
+ else if (head == closePar) counter - 1
+ else counter
+ balanced_nonEarly(tail, c)
+ }
+ case Nil() => counter == 0
+ }
+ } ensuring { res => res == balanced(list, counter) }
+
+ def balanced_withFailure(list: List, counter: BigInt, failed: Boolean): Boolean = {
+ require(counter >= 0 || failed)
+ list match {
+ case Cons(head, tail) =>
+ val c = if (head == openPar) counter + 1
+ else if (head == closePar) counter - 1
+ else counter
+ balanced_withFailure(tail, c, failed || c < 0)
+ case Nil() => !failed && counter == 0
+ }
+ } ensuring { res =>
+ if (failed) {
+ res == balanced_nonEarly(list, -1)
+ } else {
+ res == balanced_nonEarly(list, counter)
+ }
+ }
+
+ def balanced_withReduce(list: List, p: (BigInt, BigInt)): Boolean = {
+ require(p._1 >= 0 && p._2 >= 0)
+ list match {
+ case Cons(head, tail) =>
+ val p2 = reduce(p, parPair(head))
+ balanced_withReduce(tail, p2)
+ case Nil() =>
+ p._1 == 0 && p._2 == 0
+ }
+ } ensuring { res => res == balanced_withFailure(list, p._1 - p._2, p._2 > 0) }
+
+ def balanced_foldLeft_equivalence(list: List, p: (BigInt, BigInt)): Boolean = {
+ require(p._1 >= 0 && p._2 >= 0)
+ val f = (s: (BigInt, BigInt), x: BigInt) => reduce(s, parPair(x))
+ (foldLeft(list, p, f) == (BigInt(0), BigInt(0))) == balanced_withReduce(list, p) && (list match {
+ case Cons(head, tail) =>
+ val p2 = f(p, head)
+ balanced_foldLeft_equivalence(tail, p2)
+ case Nil() => true
+ })
+ }.holds
+
+ def foldRight[A](list: List, state: A, f: (BigInt, A) => A): A = list match {
+ case Cons(head, tail) =>
+ val tailState = foldRight(tail, state, f)
+ f(head, tailState)
+ case Nil() => state
+ }
+
+ def foldLeft[A](list: List, state: A, f: (A, BigInt) => A): A = list match {
+ case Cons(head, tail) =>
+ val nextState = f(state, head)
+ foldLeft(tail, nextState, f)
+ case Nil() => state
+ }
+
+ def reduce(p1: (BigInt, BigInt), p2: (BigInt, BigInt)): (BigInt, BigInt) = {
+ if (p1._1 >= p2._2) {
+ (p1._1 - p2._2 + p2._1, p1._2)
+ } else {
+ (p2._1, p2._2 - p1._1 + p1._2)
+ }
+ }
+
+ def reduce_associative(p1: (BigInt, BigInt), p2: (BigInt, BigInt), p3: (BigInt, BigInt)): Boolean = {
+ reduce(p1, reduce(p2, p3)) == reduce(reduce(p1, p2), p3)
+ }.holds
+
+ def swap(p: (BigInt, BigInt)): (BigInt, BigInt) = (p._2, p._1)
+
+ def reduce_inverse(p1: (BigInt, BigInt), p2: (BigInt, BigInt)): Boolean = {
+ reduce(p1, p2) == swap(reduce(swap(p2), swap(p1)))
+ }.holds
+
+ def reduce_associative_inverse(p1: (BigInt, BigInt), p2: (BigInt, BigInt), p3: (BigInt, BigInt)): Boolean = {
+ reduce(p1, reduce(p2, p3)) == swap(reduce(reduce(swap(p3), swap(p2)), swap(p1)))
+ }.holds
+
+ def reduce_associative_inverse2(p1: (BigInt, BigInt), p2: (BigInt, BigInt), p3: (BigInt, BigInt)): Boolean = {
+ reduce(reduce(p1, p2), p3) == swap(reduce(swap(p3), reduce(swap(p2), swap(p1))))
+ }.holds
+
+ def parPair(x: BigInt): (BigInt, BigInt) = {
+ if (x == openPar) (1, 0) else if (x == closePar) (0, 1) else (0, 0)
+ }
+
+ def headOption(list: List): Option = list match {
+ case Cons(head, tail) => Some(head)
+ case Nil() => None()
+ }
+
+ def lastOption(list: List): Option = list match {
+ case Cons(head, Nil()) => Some(head)
+ case Cons(head, tail) => lastOption(tail)
+ case Nil() => None()
+ }
+
+ def init(list: List): List = list match {
+ case Cons(head, Nil()) => Nil()
+ case Cons(head, tail) => Cons(head, init(tail))
+ case Nil() => Nil()
+ }
+
+ def tail(list: List): List = list match {
+ case Cons(head, tail) => tail
+ case Nil() => Nil()
+ }
+
+ def addLast(list: List, x: BigInt): List = {
+ list match {
+ case Cons(head, tail) => Cons(head, addLast(tail, x))
+ case Nil() => Cons(x, Nil())
+ }
+ } ensuring { res => lastOption(res) == Some(x) && init(res) == list }
+
+ def reverse(list: List): List = {
+ list match {
+ case Cons(head, tail) => addLast(reverse(tail), head)
+ case Nil() => Nil()
+ }
+ } ensuring { res =>
+ lastOption(res) == headOption(list) &&
+ lastOption(list) == headOption(res)
+ }
+
+ def reverse_tail_equivalence(list: List): Boolean = {
+ reverse(tail(list)) == init(reverse(list))
+ }.holds
+
+ def reverse_init_equivalence(list: List): Boolean = {
+ reverse(init(list)) == tail(reverse(list)) && (list match {
+ case Cons(head, tail) => reverse_init_equivalence(tail)
+ case Nil() => true
+ })
+ }.holds
+
+ def reverse_equality_equivalence(l1: List, l2: List): Boolean = {
+ (l1 == l2) == (reverse(l1) == reverse(l2)) && ((l1, l2) match {
+ case (Cons(h1, t1), Cons(h2, t2)) => reverse_equality_equivalence(t1, t2)
+ case _ => true
+ })
+ }.holds
+
+ def reverse_reverse_equivalence(list: List): Boolean = {
+ reverse(reverse(list)) == list && ((list, reverse(list)) match {
+ case (Cons(h1, t1), Cons(h2, t2)) =>
+ reverse_reverse_equivalence(t1) && reverse_reverse_equivalence(t2)
+ case _ => true
+ })
+ }.holds
+
+ /*
+ def fold_equivalence(list: List): Boolean = {
+ val s = (0, 0)
+ val fl = (s: (BigInt, BigInt), x: BigInt) => reduce(s, parPair(x))
+ val fr = (x: BigInt, s: (BigInt, BigInt)) => reduce(parPair(x), s)
+
+ foldLeft(list, s, fl) == foldRight(list, s, fr)
+ }.holds
+
+ def lemma(list: List): Boolean = {
+ val f = (x: BigInt, s: (BigInt, BigInt)) => reduce(parPair(x), s)
+ fold_equivalence(list) && balanced_foldLeft_equivalence(list, (0, 0)) &&
+ (foldRight(list, (0, 0), f) == (0, 0)) == balanced(list, 0)
+ }.holds
+ */
+
+}
diff --git a/testcases/web/verification/13_Monads.scala b/testcases/web/verification/13_Monads.scala
new file mode 100644
index 0000000000000000000000000000000000000000..05b46ceb0f02a96811b7ca8a4606b4b4b30de3e3
--- /dev/null
+++ b/testcases/web/verification/13_Monads.scala
@@ -0,0 +1,79 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+import leon.lang._
+import leon.collection._
+
+object Monads3 {
+
+ def append[T](l1: List[T], l2: List[T]): List[T] = {
+ l1 match {
+ case Cons(head, tail) => Cons(head, append(tail, l2))
+ case Nil() => l2
+ }
+ } ensuring { res => (res == l1) || (l2 != Nil[T]()) }
+
+ def flatMap[T,U](list: List[T], f: T => List[U]): List[U] = list match {
+ case Cons(head, tail) => append(f(head), flatMap(tail, f))
+ case Nil() => Nil()
+ }
+
+ def associative_lemma[T,U,V](list: List[T], f: T => List[U], g: U => List[V]): Boolean = {
+ flatMap(flatMap(list, f), g) == flatMap(list, (x: T) => flatMap(f(x), g))
+ }
+
+ def associative_lemma_induct[T,U,V](list: List[T], flist: List[U], glist: List[V], f: T => List[U], g: U => List[V]): Boolean = {
+ associative_lemma(list, f, g) &&
+ append(glist, flatMap(append(flist, flatMap(list, f)), g)) == append(append(glist, flatMap(flist, g)), flatMap(list, (x: T) => flatMap(f(x), g))) &&
+ (glist match {
+ case Cons(ghead, gtail) =>
+ associative_lemma_induct(list, flist, gtail, f, g)
+ case Nil() => flist match {
+ case Cons(fhead, ftail) =>
+ associative_lemma_induct(list, ftail, g(fhead), f, g)
+ case Nil() => list match {
+ case Cons(head, tail) => associative_lemma_induct(tail, f(head), Nil(), f, g)
+ case Nil() => true
+ }
+ }
+ })
+ }.holds
+
+ def left_unit_law[T,U](x: T, f: T => List[U]): Boolean = {
+ flatMap(Cons(x, Nil()), f) == f(x)
+ }.holds
+
+ def right_unit_law[T](list: List[T]): Boolean = {
+ flatMap(list, (x: T) => Cons(x, Nil())) == list
+ }
+
+ def right_unit_induct[T,U](list: List[T]): Boolean = {
+ right_unit_law(list) && (list match {
+ case Cons(head, tail) => right_unit_induct(tail)
+ case Nil() => true
+ })
+ }.holds
+
+ def flatMap_zero_law[T,U](f: T => List[U]): Boolean = {
+ flatMap(Nil[T](), f) == Nil[U]()
+ }.holds
+
+ def flatMap_to_zero_law[T](list: List[T]): Boolean = {
+ flatMap(list, (x: T) => Nil[T]()) == Nil[T]()
+ }
+
+ def flatMap_to_zero_induct[T,U](list: List[T]): Boolean = {
+ flatMap_to_zero_law(list) && (list match {
+ case Cons(head, tail) => flatMap_to_zero_induct(tail)
+ case Nil() => true
+ })
+ }.holds
+
+ def add_zero_law[T](list: List[T]): Boolean = {
+ append(list, Nil()) == list
+ }.holds
+
+ def zero_add_law[T](list: List[T]): Boolean = {
+ append(Nil(), list) == list
+ }.holds
+
+}