Commit 15666988 authored by Martin Clochard's avatar Martin Clochard

(examples with Fibonacci numbers) Incomplete specification fixed

parent 17544ccd
......@@ -86,7 +86,7 @@ module SmallestFibAbove
let smallest_fib_above (x: int) : int
requires { 0 <= x }
ensures { exists k: int. 0 <= k /\ fib k <= x < fib (k+1) }
ensures { exists k: int. 0 <= k /\ fib k <= x < fib (k+1) = result }
=
let a = ref 0 in
let b = ref 1 in
......
......@@ -973,16 +973,16 @@
locfile="../fibonacci.mlw"
loclnum="80" loccnumb="7" loccnume="23"
verified="true"
expanded="true">
expanded="false">
<goal
name="WP_parameter smallest_fib_above"
locfile="../fibonacci.mlw"
loclnum="87" loccnumb="6" loccnume="24"
expl="VC for smallest_fib_above"
sum="7bdaa701ec5bc772f1185ea7cfdd7e21"
sum="2cb037e236a8b011db9f700e744e18ce"
proved="true"
expanded="true"
shape="iainfix &lt;V0afibainfix +V3c1Aainfix &lt;=afibV3V0Aainfix &lt;=c0V3Eainfix &lt;ainfix -ainfix *c2V0ainfix +V4V5ainfix -ainfix *c2V0ainfix +V2V1Aainfix &lt;=c0ainfix -ainfix *c2V0ainfix +V2V1Aainfix =V5afibainfix +V6c1Aainfix &lt;=afibV6V0Aainfix =V4afibV6Aainfix &lt;=c0V6EIainfix =V5ainfix +V2V1FIainfix =V4V1Fainfix &lt;=V1V0Iainfix =V1afibainfix +V7c1Aainfix &lt;=afibV7V0Aainfix =V2afibV7Aainfix &lt;=c0V7EFAainfix =c1afibainfix +V8c1Aainfix &lt;=afibV8V0Aainfix =c0afibV8Aainfix &lt;=c0V8EIainfix &lt;=c0V0F">
expanded="false"
shape="iainfix =afibainfix +V3c1V1Aainfix &lt;V0afibainfix +V3c1Aainfix &lt;=afibV3V0Aainfix &lt;=c0V3Eainfix &lt;ainfix -ainfix *c2V0ainfix +V4V5ainfix -ainfix *c2V0ainfix +V2V1Aainfix &lt;=c0ainfix -ainfix *c2V0ainfix +V2V1Aainfix =V5afibainfix +V6c1Aainfix &lt;=afibV6V0Aainfix =V4afibV6Aainfix &lt;=c0V6EIainfix =V5ainfix +V2V1FIainfix =V4V1Fainfix &lt;=V1V0Iainfix =V1afibainfix +V7c1Aainfix &lt;=afibV7V0Aainfix =V2afibV7Aainfix &lt;=c0V7EFAainfix =c1afibainfix +V8c1Aainfix &lt;=afibV8V0Aainfix =c0afibV8Aainfix &lt;=c0V8EIainfix &lt;=c0V0F">
<label
name="expl:VC for smallest_fib_above"/>
<proof
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment