From 4c7edb7ec136ccadf04934734fcf981317c1bfaa Mon Sep 17 00:00:00 2001
From: Regis Blanc <regwblanc@gmail.com>
Date: Fri, 22 Apr 2016 18:43:43 +0200
Subject: [PATCH] working guess number example
---
.../xlang/GuessNumberInteractive.scala | 28 ++++++++-----------
1 file changed, 12 insertions(+), 16 deletions(-)
diff --git a/testcases/verification/xlang/GuessNumberInteractive.scala b/testcases/verification/xlang/GuessNumberInteractive.scala
index eb6e07081..85b083bba 100644
--- a/testcases/verification/xlang/GuessNumberInteractive.scala
+++ b/testcases/verification/xlang/GuessNumberInteractive.scala
@@ -5,35 +5,31 @@ import leon.io.StdIn
import leon.annotation._
object GuessNumberInteractive {
-
- //def pickRandomly(min: BigInt, max: BigInt): BigInt = {
- // require(min >= 0 && max >= min)
- // StdIn.readBigInt
- //}
+ @extern
def pickBetween(bot: BigInt, top: BigInt): BigInt = {
require(bot <= top)
- bot + (top - bot)/2
+ bot + (top - bot)/2 //works for execution
} ensuring(res => res >= bot && res <= top)
def guessNumber(choice: Option[BigInt])(implicit state: StdIn.State): BigInt = {
require(choice match { case Some(c) => c >= 0 && c <= 10 case None() => true })
- var top: BigInt = 10
var bot: BigInt = 0
- var guess: BigInt = pickBetween(bot, top)
+ var top: BigInt = 10
(while(bot < top) {
- if(isGreater(guess, choice)) {
- top = guess-1
- if(bot <= top)
- guess = pickBetween(bot, top)
+ val prevDec = top - bot
+
+ val guess = pickBetween(bot, top-1) //never pick top, wouldn't learn anyting if pick top and if guess >= choice
+ if(isSmaller(guess, choice)) {
+ bot = guess+1
} else {
- bot = guess
- if(bot <= top)
- guess = pickBetween(bot, top)
+ top = guess
}
+ val dec = top - bot
+ assert(dec >= 0 && dec < prevDec)
}) invariant(choice match {
- case Some(c) => guess >= bot && guess <= top && bot >= 0 && top <= 10 && bot <= top && c >= bot && c <= top
+ case Some(c) => bot >= 0 && top <= 10 && bot <= top && c >= bot && c <= top
case None() => true
})
bot
--
GitLab