# Labs 02: Using the Leon Verification System (continued)

In this second lab, you will use the web-interface of leon to try to verify programs. You can use an experimental version of the Leon interface available at: http://laraquad1.epfl.ch:9000/sav15

You should also install Leon locally, on your (preferably linux) machine. Please follow the instructions on https://github.com/epfl-lara/leon#building-leon and tell us if something fails.

### Deliverable

You are given 1 week for this assignment.

You must use the interface on http://larasrv09.epfl.ch:9000/sav15/repository as follows:

1. Click on the “Deliverables” tab
2. Click “Deliver this version” on the commit corresponding to the version of your code you want to submit

Note: We recommend that you consider the second exercise first, because it is shorter and easier.

### Exercise 6

In this exercise you will be able to use part of the Leon library, notably Option and List.

```import leon.lang._
import leon.collection._
import leon._
/**
* 1) Implement the isSearchTree property that checks bounds of elements in a
*    search tree. Assume that the tree is strictly sorted (no dupplicates)
*
* 2) Implement operations on Binary Search Trees as efficiently as you can.
*    These operations will likely not verify, but make sure that leon does not
*    find counter-examples within a reasonnable timeout (e.g. --timeout=5 )
*
*    You do not need to change the pre-/post-conditions
*
* 3) Implement toList to return a sorted list from a search tree.
*/

object BinaryTree {

abstract class Tree {
def content: Set[BigInt] = {
this match {
case Empty => Set()
case Node(l, v, r) => l.content ++ Set(v) ++ r.content
}
}

def size: BigInt = {
this match {
case Empty => 0
case Node(l, _, r) => l.size + r.size + 1
}
} ensuring { _ >= 0 }

def +(x: BigInt): Tree = {
require(isBT)
this // TODO
} ensuring {
res => res.isBT &&
res.content == this.content ++ Set(x) &&
res.size >= this.size &&
res.size <= this.size + 1
}

def -(x: BigInt): Tree = {
require(isBT)
this // TODO
} ensuring {
res => res.isBT &&
res.content == this.content -- Set(x) &&
res.size <= this.size &&
res.size >= this.size - 1
}

def ++(that: Tree): Tree = {
require(this.isBT && that.isBT)
this // TODO
} ensuring {
res => res.isBT && res.content == this.content ++ that.content
}

def contains(x: BigInt): Boolean = {
require(isBT)
false // TODO
} ensuring {
res => res == (content contains x)
}

def toList: List[BigInt] = {
require(isBT)
Nil() // TODO
} ensuring {
res => res.content == this.content && isSorted(res)
}

// Properties

def isBT: Boolean = {
isSearchTree(None(), None())
}

def isSearchTree(min: Option[BigInt], max: Option[BigInt]): Boolean = {
this match {
case Empty => true
case Node(l, v, r) =>
true // TODO
}
}
}

case object Empty extends Tree
case class Node(l: Tree, v: BigInt, r: Tree) extends Tree

def isSorted(l: List[BigInt]): Boolean = {
l match {
case Cons(v1, t @ Cons(v2, _)) if v1 >= v2 => false
case Cons(h, t) => isSorted(t)
case Nil() => true
}
}
}```

### Exercise 7

```import leon.lang._

/**
* 1) Implement operations on rationals: addition, substraction, multiplication and division
*    Ensure that the results are rationals, add necessary preconditions.
* 2) Implement rational equivalence (~).
* 3) Write lemmas that show that if a1 ~ a2, and b1 ~ b2, then (a1 <op> b1) ~ (a2 <op> b2), for each <op>
*/
object Rationals {
// Represents n/d
case class Q(n: BigInt, d: BigInt) {

def +(that: Q):Q = this // TODO

def -(that: Q):Q = this // TODO

def *(that: Q):Q = this // TODO

def /(that: Q):Q = this // TODO

// Equivalence of two rationals, true if they represent the same real number
def ~(that: Q): Boolean = false // TODO

def isRational = !(d == 0)
def nonZero    = !(n == 0)
}

def lemma1(a1: Q, a2: Q, b1: Q, b2: Q): Boolean = {
true // TODO
}.holds
}```