import leon.Utils._ /** * Code should be contained in a single top-level object */ object Test1 { /** * You can define Algebraic Data Types using abstract classes and case classes. */ abstract class List case class Cons(head: Int, tail: List) extends List case class Nil() extends List def size(l: List): Int = (l match { case Nil() => 0 case Cons(h, t) => 1+size(t) }) ensuring { _ >= 0 } def contains(l: List, v: Int): Boolean = (l match { case Nil() => false case Cons(h, t) => v == h || contains(t, v) }) ensuring { res => time < 7*(size(l)+3) } abstract class Tree case class Node(l: Tree, v: Int, r: Tree) extends Tree case class Leaf() extends Tree def treeHeight(t: Tree): Int = (t match { case Node(l, v, r) => val lh = treeHeight(l) val rh = treeHeight(r) if (lh > rh) 1 + lh else 1 + rh case Leaf() => 0 }) ensuring { _ >= 0 } def treeSize(t: Tree): Int = (t match { case Node(l, v, r) => 1 + treeSize(l) + treeSize(r) case Leaf() => 0 }) ensuring { _ >= 0 } def treeContains(t: Tree, v: Int): Boolean = (t match { case Node(l, v2, r) => v == v2 || treeContains(l, v) || treeContains(r, v) case Leaf() => false }) ensuring{ res => time < treeSize(t)*10+2 } def treeLeftMost(t: Tree): Int = (t match { case Node(l, v, r) => l match { case Leaf() => v case _ => treeLeftMost(l) } case Leaf() => -1 }) ensuring{ res => time < treeHeight(t)*10+10 } def treeContains0(t: Tree): Boolean = { treeContains(t, 0) } ensuring{ res => time < treeSize(t)*10+3 } }