• English only

# Lab for Automated Reasoning and Analysis LARA

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 }

}