Lab for Automated Reasoning and Analysis LARA

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.

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.

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
}
 
sav15/labs_02.txt · Last modified: 2015/02/25 16:16 by ekneuss
 
© EPFL 2018 - Legal notice