From 37bc9723be6d6ae510073fec535a51b79fbb999a Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 29 Apr 2016 16:07:25 +0200
Subject: [PATCH] io directory for tests
---
.../verification/xlang/GuessNumber.scala | 35 -------------------
.../GuessNumber.scala} | 2 +-
2 files changed, 1 insertion(+), 36 deletions(-)
delete mode 100644 testcases/verification/xlang/GuessNumber.scala
rename testcases/verification/xlang/{GuessNumberInteractive.scala => io/GuessNumber.scala} (98%)
diff --git a/testcases/verification/xlang/GuessNumber.scala b/testcases/verification/xlang/GuessNumber.scala
deleted file mode 100644
index ca1ea724a..000000000
--- a/testcases/verification/xlang/GuessNumber.scala
+++ /dev/null
@@ -1,35 +0,0 @@
-import leon.lang._
-import leon.lang.xlang._
-import leon.util.Random
-
-object GuessNumber {
-
- def pickRandomly(min: BigInt, max: BigInt): BigInt = {
- require(min >= 0 && max >= min)
- Random.nextBigInt(max - min + 1) + min
- }
-
- def main(): Unit = {
- val choice = pickRandomly(0, 10)
-
- var guess = pickRandomly(0, 10)
- var top: BigInt = 10
- var bot: BigInt = 0
-
- (while(bot < top) {
- if(isGreater(guess, choice)) {
- top = guess-1
- guess = pickRandomly(bot, top)
- } else if(isSmaller(guess, choice)) {
- bot = guess+1
- guess = pickRandomly(bot, top)
- }
- }) invariant(guess >= bot && guess <= top && bot >= 0 && top <= 10 && bot <= top && choice >= bot && choice <= top)
- val answer = bot
- assert(answer == choice)
- }
-
- def isGreater(guess: BigInt, choice: BigInt): Boolean = guess > choice
- def isSmaller(guess: BigInt, choice: BigInt): Boolean = guess < choice
-
-}
diff --git a/testcases/verification/xlang/GuessNumberInteractive.scala b/testcases/verification/xlang/io/GuessNumber.scala
similarity index 98%
rename from testcases/verification/xlang/GuessNumberInteractive.scala
rename to testcases/verification/xlang/io/GuessNumber.scala
index 85b083bba..46bf0d99a 100644
--- a/testcases/verification/xlang/GuessNumberInteractive.scala
+++ b/testcases/verification/xlang/io/GuessNumber.scala
@@ -4,7 +4,7 @@ import leon.io.StdIn
import leon.annotation._
-object GuessNumberInteractive {
+object GuessNumber {
@extern
def pickBetween(bot: BigInt, top: BigInt): BigInt = {
--
GitLab