From 0a83bd39822e5630a941e4edc10b8b83fea6d480 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 7 Apr 2016 21:33:35 +0200
Subject: [PATCH] util.Random as a library
---
library/util/Random.scala | 32 +++++++++++++++++++
.../verification/xlang/GuessNumber.scala | 25 ++++++++-------
2 files changed, 46 insertions(+), 11 deletions(-)
create mode 100644 library/util/Random.scala
diff --git a/library/util/Random.scala b/library/util/Random.scala
new file mode 100644
index 000000000..e055dc51b
--- /dev/null
+++ b/library/util/Random.scala
@@ -0,0 +1,32 @@
+/* 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)
+
+}
+
diff --git a/testcases/verification/xlang/GuessNumber.scala b/testcases/verification/xlang/GuessNumber.scala
index 806948060..ca1ea724a 100644
--- a/testcases/verification/xlang/GuessNumber.scala
+++ b/testcases/verification/xlang/GuessNumber.scala
@@ -1,32 +1,35 @@
import leon.lang._
import leon.lang.xlang._
+import leon.util.Random
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 = {
- val choice = random(0, 10)
+ val choice = pickRandomly(0, 10)
- var guess = random(0, 10)
- var top = 10
- var bot = 0
+ var guess = pickRandomly(0, 10)
+ var top: BigInt = 10
+ var bot: BigInt = 0
(while(bot < top) {
if(isGreater(guess, choice)) {
top = guess-1
- guess = random(bot, top)
+ guess = pickRandomly(bot, top)
} else if(isSmaller(guess, choice)) {
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 &&
- true)
+ }) invariant(guess >= bot && guess <= top && bot >= 0 && top <= 10 && bot <= top && choice >= bot && choice <= top)
val answer = bot
assert(answer == choice)
}
- def isGreater(guess: Int, choice: Int): Boolean = guess > choice
- def isSmaller(guess: Int, choice: Int): Boolean = guess < choice
+ def isGreater(guess: BigInt, choice: BigInt): Boolean = guess > choice
+ def isSmaller(guess: BigInt, choice: BigInt): Boolean = guess < choice
}
--
GitLab