From 7ae01ef79dd8a207a05bea7cbbafb2fa0ae37b47 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?R=C3=A9gis=20Blanc?= <regwblanc@gmail.com>
Date: Thu, 7 Apr 2016 18:32:56 +0200
Subject: [PATCH] guess a number with espilons
---
.../xlang/valid/GuessNumber.scala | 32 +++++++++++++++++++
.../verification/xlang/GuessNumber.scala | 32 +++++++++++++++++++
2 files changed, 64 insertions(+)
create mode 100644 src/test/resources/regression/verification/xlang/valid/GuessNumber.scala
create mode 100644 testcases/verification/xlang/GuessNumber.scala
diff --git a/src/test/resources/regression/verification/xlang/valid/GuessNumber.scala b/src/test/resources/regression/verification/xlang/valid/GuessNumber.scala
new file mode 100644
index 000000000..806948060
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/GuessNumber.scala
@@ -0,0 +1,32 @@
+import leon.lang._
+import leon.lang.xlang._
+
+object GuessNumber {
+
+ def random(min: Int, max: Int): Int = epsilon((x: Int) => x >= min && x <= max)
+
+ def main(): Unit = {
+ val choice = random(0, 10)
+
+ var guess = random(0, 10)
+ var top = 10
+ var bot = 0
+
+ (while(bot < top) {
+ if(isGreater(guess, choice)) {
+ top = guess-1
+ guess = random(bot, top)
+ } else if(isSmaller(guess, choice)) {
+ bot = guess+1
+ guess = random(bot, top)
+ }
+ }) invariant(guess >= bot && guess <= top && bot >= 0 && top <= 10 && bot <= top && choice >= bot && choice <= top &&
+ true)
+ val answer = bot
+ assert(answer == choice)
+ }
+
+ def isGreater(guess: Int, choice: Int): Boolean = guess > choice
+ def isSmaller(guess: Int, choice: Int): Boolean = guess < choice
+
+}
diff --git a/testcases/verification/xlang/GuessNumber.scala b/testcases/verification/xlang/GuessNumber.scala
new file mode 100644
index 000000000..806948060
--- /dev/null
+++ b/testcases/verification/xlang/GuessNumber.scala
@@ -0,0 +1,32 @@
+import leon.lang._
+import leon.lang.xlang._
+
+object GuessNumber {
+
+ def random(min: Int, max: Int): Int = epsilon((x: Int) => x >= min && x <= max)
+
+ def main(): Unit = {
+ val choice = random(0, 10)
+
+ var guess = random(0, 10)
+ var top = 10
+ var bot = 0
+
+ (while(bot < top) {
+ if(isGreater(guess, choice)) {
+ top = guess-1
+ guess = random(bot, top)
+ } else if(isSmaller(guess, choice)) {
+ bot = guess+1
+ guess = random(bot, top)
+ }
+ }) invariant(guess >= bot && guess <= top && bot >= 0 && top <= 10 && bot <= top && choice >= bot && choice <= top &&
+ true)
+ val answer = bot
+ assert(answer == choice)
+ }
+
+ def isGreater(guess: Int, choice: Int): Boolean = guess > choice
+ def isSmaller(guess: Int, choice: Int): Boolean = guess < choice
+
+}
--
GitLab