From 68830dc92c56f438ff92b91d704595cf94430e31 Mon Sep 17 00:00:00 2001 From: Etienne Kneuss <ekneuss@gmail.com> Date: Wed, 31 Oct 2012 13:49:30 +0100 Subject: [PATCH] Add complicated synthesis test case --- .../scala/leon/purescala/ScalaPrinter.scala | 4 +- testcases/synthesis/SortedList.scala | 133 ++++++++++++++++++ 2 files changed, 135 insertions(+), 2 deletions(-) create mode 100644 testcases/synthesis/SortedList.scala diff --git a/src/main/scala/leon/purescala/ScalaPrinter.scala b/src/main/scala/leon/purescala/ScalaPrinter.scala index feff130ee..aa192763c 100644 --- a/src/main/scala/leon/purescala/ScalaPrinter.scala +++ b/src/main/scala/leon/purescala/ScalaPrinter.scala @@ -240,7 +240,7 @@ object ScalaPrinter { case FiniteMultiset(rs) => ppNary(sb, rs, "{|", ", ", "|}", lvl) case EmptySet(bt) => sb.append("Set()") // Ø case EmptyMultiset(_) => sys.error("Not Valid Scala") - case Not(ElementOfSet(s,e)) => sys.error("TODO") + case ElementOfSet(s,e) => ppBinary(sb, s, e, " contains ", lvl) //case ElementOfSet(s,e) => ppBinary(sb, s, e, " \u2208 ", lvl) // \in //case SubsetOf(l,r) => ppBinary(sb, l, r, " \u2286 ", lvl) // \subseteq //case Not(SubsetOf(l,r)) => ppBinary(sb, l, r, " \u2288 ", lvl) // \notsubseteq @@ -422,7 +422,7 @@ object ScalaPrinter { case ResultVariable() => sb.append("res") case EpsilonVariable((row, col)) => sb.append("x" + row + "_" + col) - case Not(expr) => ppUnary(sb, expr, "\u00AC(", ")", lvl) // \neg + case Not(expr) => ppUnary(sb, expr, "!(", ")", lvl) // \neg case e @ Error(desc) => { var nsb = sb diff --git a/testcases/synthesis/SortedList.scala b/testcases/synthesis/SortedList.scala new file mode 100644 index 000000000..af05150bf --- /dev/null +++ b/testcases/synthesis/SortedList.scala @@ -0,0 +1,133 @@ +import scala.collection.immutable.Set +import leon.Annotations._ +import leon.Utils._ + +object SortedList { + sealed abstract class List + case class Cons(head: Int, tail: List) extends List + case class Nil() extends List + + // proved with unrolling=0 + def size(l: List) : Int = (l match { + case Nil() => 0 + case Cons(_, t) => 1 + size(t) + }) ensuring(res => res >= 0) + + def sizeSynth(l: List): Int = choose{ (i: Int) => i >= 0 && sizeSynth(Cons(0, l)) == i + 1} + + def content(l: List): Set[Int] = l match { + case Nil() => Set() + case Cons(i, t) => Set(i) ++ content(t) + } + + def insertSynth(in: List, v: Int) = choose{ (out: List) => content(out) == content(in) ++ Set(v) } + + def insert1(l: List, v: Int) = ( + Cons(v, l) + ) ensuring(res => content(res) == content(l) ++ Set(v) && size(res) >= size(l)) + + def insert2(l: List, v: Int): List = (l match { + case Nil() => Cons(v, Nil()) + case Cons(x, tail) => if (x == v) l else Cons(x, insert2(tail, v)) + }) ensuring(res => content(res) == content(l) ++ Set(v) && size(res) >= size(l)) + + def insert3(l: List, v: Int): List = { + require(isStrictlySorted(l)) + + l match { + case Nil() => Cons(v, Nil()) + case Cons(x, tail) => + if (v < x) { + Cons(v, l) + } else if (v == x) { + l + } else { + Cons(x, insert3(tail, v)) + } + } + } ensuring(res => content(res) == content(l) ++ Set(v) && size(res) >= size(l)) + + def deleteSynth(in: List, v: Int) = choose{ (out: List) => !(content(out) contains v) } + + def delete1(l: List, v: Int): List = (l match { + case Nil() => Nil() + case Cons(x, tail) => if (x == v) delete1(tail, v) else Cons(x, delete1(tail, v)) + }) ensuring(res => !(content(res) contains v) && size(res) <= size(l)) + + //def delete2(l: List, v: Int): List = { + // require(isStrictlySorted(l)) + + // l match { + // case Nil() => Nil() + // case Cons(x, tail) => + // if (x == v) { + // tail + // } else { + // Cons(x, delete2(tail, v)) + // } + // } + //} ensuring(res => !(content(res) contains v) && size(res) <= size(l)) + + def contains(list : List, elem : Int) : Boolean = (list match { + case Nil() => false + case Cons(x, xs) => if(elem == x) true else contains(xs, elem) + }) ensuring(res => res == content(list).contains(elem)) + + def deleteMagic(head: Int, tail: List, toDelete: Int): List = ({ + //require(isStrictlySorted(Cons(head, tail)) && toDelete < head); + require(isStrictlySorted(Cons(toDelete, Cons(head, tail)))) + + Cons(head, tail) + })ensuring(res => !(content(res) contains toDelete)) + + def delete3(l: List, v: Int): List = { + require(isStrictlySorted(l)) + + l match { + case Nil() => Nil() + case Cons(x, tail) => + if (x == v) { + tail + } else if (v < x) { + deleteMagic(x, tail, v) + } else { + Cons(x, delete3(tail, v)) + } + } + } ensuring(res => !(content(res) contains v) && size(res) <= size(l)) + + @induct + def isStrictlySorted(l: List): Boolean = (l match { + case Nil() => true + case Cons(x, Nil()) => true + case Cons(x, xs @ Cons(y, ys)) => { + if(x < y) { + if(isStrictlySorted(xs)) discard(ltaLemma(x, y, ys)) else false + } else { + false + } + } + }) ensuring(res => !res || (l match { + case Nil() => true + case Cons(x, xs) => lessThanAll(x, xs) + })) + + def lessThanAll(x : Int, l : List) : Boolean = (l match { + case Nil() => true + case Cons(y, ys) => if(x < y) lessThanAll(x, ys) else false + }) ensuring(res => !res || !contains(l, x)) + + def discard(value : Boolean) = true + + @induct + def ltaLemma(x : Int, y : Int, l : List) : Boolean = { + require(lessThanAll(y, l) && x < y) + lessThanAll(x, Cons(y, l)) + } holds + + 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)) + } +} -- GitLab