Skip to content
Snippets Groups Projects
Commit 0a83bd39 authored by Régis Blanc's avatar Régis Blanc Committed by Ravi
Browse files

util.Random as a library

parent 9267248b
No related branches found
No related tags found
No related merge requests found
/* Copyright 2009-2016 EPFL, Lausanne */
package leon.util
import leon.annotation._
import leon.lang.xlang._
object Random {
@library
def nextBoolean(): Boolean = epsilon((x: Boolean) => true)
@library
def nextInt(): Int = epsilon((x: Int) => true)
@library
def nextInt(max: Int): Int = {
require(max > 0)
epsilon((x: Int) => x >= 0 && x < max)
} ensuring(res => res >= 0 && res < max)
@library
def nextBigInt(): BigInt = epsilon((x: BigInt) => true)
@library
def nextBigInt(max: BigInt): BigInt = {
require(max > 0)
epsilon((x: BigInt) => x >= 0 && x < max)
} ensuring(res => res >= 0 && res < max)
}
import leon.lang._ import leon.lang._
import leon.lang.xlang._ import leon.lang.xlang._
import leon.util.Random
object GuessNumber { object GuessNumber {
def random(min: Int, max: Int): Int = epsilon((x: Int) => x >= min && x <= max) def pickRandomly(min: BigInt, max: BigInt): BigInt = {
require(min >= 0 && max >= min)
Random.nextBigInt(max - min + 1) + min
}
def main(): Unit = { def main(): Unit = {
val choice = random(0, 10) val choice = pickRandomly(0, 10)
var guess = random(0, 10) var guess = pickRandomly(0, 10)
var top = 10 var top: BigInt = 10
var bot = 0 var bot: BigInt = 0
(while(bot < top) { (while(bot < top) {
if(isGreater(guess, choice)) { if(isGreater(guess, choice)) {
top = guess-1 top = guess-1
guess = random(bot, top) guess = pickRandomly(bot, top)
} else if(isSmaller(guess, choice)) { } else if(isSmaller(guess, choice)) {
bot = guess+1 bot = guess+1
guess = random(bot, top) guess = pickRandomly(bot, top)
} }
}) invariant(guess >= bot && guess <= top && bot >= 0 && top <= 10 && bot <= top && choice >= bot && choice <= top && }) invariant(guess >= bot && guess <= top && bot >= 0 && top <= 10 && bot <= top && choice >= bot && choice <= top)
true)
val answer = bot val answer = bot
assert(answer == choice) assert(answer == choice)
} }
def isGreater(guess: Int, choice: Int): Boolean = guess > choice def isGreater(guess: BigInt, choice: BigInt): Boolean = guess > choice
def isSmaller(guess: Int, choice: Int): Boolean = guess < choice def isSmaller(guess: BigInt, choice: BigInt): Boolean = guess < choice
} }
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment