Add tests in main branch

testcases/SortedList.scala

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

testcases/SortedTree.scala

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