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.

You are given 1 week for this assignment.

Deadline: Sunday, Mar. 8, 25:59.

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.

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

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
}