Skip to content
Snippets Groups Projects
Commit 46b4a943 authored by Manos Koukoutos's avatar Manos Koukoutos
Browse files

Get rid of invalid benchmark

parent 85003922
No related branches found
No related tags found
No related merge requests found
/* Copyright 2009-2014 EPFL, Lausanne */
import leon.annotation._
import leon.lang.synthesis._
import leon.lang._
object Choose1 {
sealed abstract class List
case class Cons(head: Int, tail: List) extends List
case class Nil() extends List
def size(l: List) : BigInt = (l match {
case Nil() => BigInt(0)
case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List) : Set[Int] = l match {
case Nil() => Set.empty[Int]
case Cons(x, xs) => Set(x) ++ content(xs)
}
def listOfSize(i: BigInt): List = {
require(i >= 0)
if (i == BigInt(0)) {
Nil()
} else {
choose { (res: List) => size(res) == i }
}
} ensuring ( size(_) == i )
def listOfSize2(i: BigInt): List = {
require(i >= 0)
if (i > 0) {
Cons(0, listOfSize(i-1))
} else {
Nil()
}
} ensuring ( size(_) == i )
}
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment