From fad0ae765d8c64a7c40f6fe0526af6b3e3502770 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Mon, 15 Oct 2012 14:35:54 +0200
Subject: [PATCH] Add tests in main branch
---
testcases/SortedList.scala | 127 ++++++++++++++++++++++++
testcases/SortedTree.scala | 195 +++++++++++++++++++++++++++++++++++++
2 files changed, 322 insertions(+)
create mode 100644 testcases/SortedList.scala
create mode 100644 testcases/SortedTree.scala
diff --git a/testcases/SortedList.scala b/testcases/SortedList.scala
new file mode 100644
index 000000000..882dbe2a7
--- /dev/null
+++ b/testcases/SortedList.scala
@@ -0,0 +1,127 @@
+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 content(l: List): Set[Int] = l match {
+ case Nil() => Set()
+ case Cons(i, t) => Set(i) ++ content(t)
+ }
+
+ 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 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))
+ }
+}
diff --git a/testcases/SortedTree.scala b/testcases/SortedTree.scala
new file mode 100644
index 000000000..3b69626ec
--- /dev/null
+++ b/testcases/SortedTree.scala
@@ -0,0 +1,195 @@
+import scala.collection.immutable.Set
+import leon.Annotations._
+import leon.Utils._
+
+object SortedTree {
+ sealed abstract class Tree
+ case class Node(v: Int, left: Tree, right: Tree) extends Tree
+ case class Leaf() extends Tree
+
+ def depth(t: Tree) : Int = (t match {
+ case Leaf() => 0
+ case Node(_, l, r) =>
+ if (depth(l) > depth(r)) {
+ depth(l)+1
+ } else {
+ depth(r)+1
+ }
+ }) ensuring(res => res >= 0)
+
+ def size(t: Tree) : Int = (t match {
+ case Leaf() => 0
+ case Node(_, l, r) => 1 + size(l) + size(r)
+ }) ensuring(res => res >= 0)
+
+ def content(t: Tree): Set[Int] = t match {
+ case Leaf() => Set()
+ case Node(v, l, r) => Set(v) ++ content(l) ++ content(r)
+ }
+
+ @induct
+ def sizeDepthLemma(t: Tree) = (
+ (depth(t) <= size(t))
+ ).holds
+
+ def isMostlySorted(t: Tree): Boolean = (t match {
+ case Node(v, l @ Node(v1, l1, r1), r @ Node(v2, l2, r2)) =>
+ isMostlySorted(l) &&
+ isMostlySorted(r) &&
+ v1 < v &&
+ v2 > v
+ case Node(v, Leaf(), r @ Node(v2, l2, r2)) =>
+ isMostlySorted(r) &&
+ v2 > v
+ case Node(v, l @ Node(v1, l1, r1), Leaf()) =>
+ isMostlySorted(l) &&
+ v1 < v
+ case _ => true
+ })
+
+ def isSortedMinMax(t: Tree, min: Int, max: Int): Boolean = (t match {
+ case Node(v, l, r) =>
+ isSortedMinMax(l, min, v) &&
+ isSortedMinMax(r, v, max) &&
+ v < max &&
+ v > min
+ case _ => true
+ })
+
+ def isSortedMin(t: Tree, min: Int): Boolean = (t match {
+ case Node(v, l, r) =>
+ isSortedMinMax(l, min, v) &&
+ isSortedMin(r, v) &&
+ v > min
+ case _ => true
+ })
+
+ def isSortedMax(t: Tree, max: Int): Boolean = (t match {
+ case Node(v, l, r) =>
+ isSortedMax(l, v) &&
+ isSortedMinMax(r, v, max) &&
+ v < max
+ case _ => true
+ })
+
+ def isSorted(t: Tree): Boolean = (t match {
+ case Node(v, l, r) =>
+ isSortedMin(r, v) &&
+ isSortedMax(l, v)
+ case _ => true
+ }) ensuring ( res => !res || (t match {
+ case Node(v, l, r) =>
+ allSmallerThan(l, v) &&
+ allGreaterThan(r, v)
+ case Leaf() => true
+ }))
+
+ def allSmallerThan(t: Tree, max: Int): Boolean = (t match {
+ case Node(v, l, r) =>
+ allSmallerThan(l, max) &&
+ allSmallerThan(r, max) &&
+ v < max
+ case Leaf() => true
+ })
+
+ def allGreaterThan(t: Tree, min: Int): Boolean = (t match {
+ case Node(v, l, r) =>
+ allGreaterThan(l, min) &&
+ allGreaterThan(r, min) &&
+ v > min
+ case Leaf() => true
+ })
+
+ @induct
+ def sortedLemma1(t: Tree) = ({
+ require(isSorted(t))
+
+ t match {
+ case Node(v, l, r) =>
+ allGreaterThan(r, v) &&
+ allSmallerThan(l, v)
+ case Leaf() => true
+ }
+ }).holds
+
+ //
+ // OPERATIONS:
+ //
+
+ def insert1(t: Tree, newV: Int): Tree = (t match {
+ case Leaf() => Node(newV, Leaf(), Leaf())
+ case Node(v, l, r) => Node(v, insert1(l, newV), r)
+ }) ensuring(res => content(res) == content(t) ++ Set(newV))
+
+ def insert2(t: Tree, newV: Int): Tree = (t match {
+ case Leaf() => Node(newV, Leaf(), Leaf())
+ case Node(v, l, r) =>
+ if (v == newV)
+ t
+ else
+ Node(v, insert2(l, newV), r)
+ }) ensuring(res => content(res) == content(t) ++ Set(newV))
+
+ def insert3(t: Tree, newV: Int): Tree = (t match {
+ case Leaf() => Node(newV, Leaf(), Leaf())
+ case Node(v, l, r) =>
+ if (v == newV)
+ t
+ else if (newV > v)
+ Node(v, l, insert3(r, newV))
+ else
+ Node(v, insert3(l, newV), r)
+ }) ensuring(res => content(res) == content(t) ++ Set(newV) && ((content(t) contains newV) || (size(res) > size(t))))
+
+ def insert4(t: Tree, newV: Int): Tree = {
+ require(isMostlySorted(t));
+
+ (t match {
+ case Leaf() => Node(newV, Leaf(), Leaf())
+ case Node(v, l, r) =>
+ if (v == newV)
+ t
+ else if (newV > v)
+ Node(v, l, insert4(r, newV))
+ else
+ Node(v, insert4(l, newV), r)
+ })} ensuring(res => content(res) == content(t) ++ Set(newV) && ((content(t) contains newV) || (size(res) > size(t))) && isMostlySorted(res))
+
+ def contains1(t: Tree, searchV: Int): Boolean = (t match {
+ case Leaf() => false
+ case Node(v, l, r) =>
+ (v == searchV) ||
+ contains1(l, searchV) ||
+ contains1(r, searchV)
+ }) ensuring(res => !res || (content(t) contains searchV))
+
+ def contains2(t: Tree, searchV: Int): Boolean = {
+ require(isMostlySorted(t))
+
+ (t match {
+ case Leaf() => false
+ case Node(v, l, r) =>
+ if (searchV > v) {
+ contains2(r, searchV)
+ } else if (searchV < v) {
+ contains2(l, searchV)
+ } else {
+ true
+ }
+ })} ensuring(res => !res || (content(t) contains searchV))
+
+ def containsBuggy(t: Tree, searchV: Int): Boolean = {
+ require(isMostlySorted(t))
+
+ (t match {
+ case Leaf() => false
+ case Node(v, l, r) =>
+ if (searchV > v) {
+ contains2(l, searchV)
+ } else if (searchV < v) {
+ contains2(r, searchV)
+ } else {
+ true
+ }
+ })} ensuring(res => !res || (content(t) contains searchV))
+}
--
GitLab