util.Random as a library

library/util/Random.scala

+/* 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)
+
+}
+

testcases/verification/xlang/GuessNumber.scala

 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
 
 }