From ff6111c140a1b473dbc2aa1d2e8f82e16772a08c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Sat, 16 Apr 2016 00:36:15 +0200
Subject: [PATCH] Random library isabelle.noBody
---
library/util/Random.scala | 5 +++++
1 file changed, 5 insertions(+)
diff --git a/library/util/Random.scala b/library/util/Random.scala
index 8a942e31b..e8efac0bd 100644
--- a/library/util/Random.scala
+++ b/library/util/Random.scala
@@ -8,21 +8,26 @@ import leon.lang.xlang._
object Random {
@library
+ @isabelle.noBody()
def nextBoolean(): Boolean = epsilon((x: Boolean) => true)
@library
+ @isabelle.noBody()
def nextInt(): Int = epsilon((x: Int) => true)
@library
+ @isabelle.noBody()
def nextInt(max: Int): Int = {
require(max > 0)
epsilon((x: Int) => x >= 0 && x < max)
} ensuring(res => res >= 0 && res < max)
@library
+ @isabelle.noBody()
def nextBigInt(): BigInt = epsilon((x: BigInt) => true)
@library
+ @isabelle.noBody()
def nextBigInt(max: BigInt): BigInt = {
require(max > 0)
epsilon((x: BigInt) => x >= 0 && x < max)
--
GitLab