example fibonacci.SmallestFibAbove simplified using ghost code

parent b4b7fb39
......@@ -90,17 +90,19 @@ module SmallestFibAbove
let smallest_fib_above (x: int) : int
requires { 0 <= x }
ensures { exists k: int. 0 <= k /\ fib k <= x < fib (k+1) = result }
ensures { exists k. 0 <= k /\ fib k <= x < fib (k+1) = result }
=
let a = ref 0 in
let b = ref 1 in
let ghost k = ref 0 in
while !b <= x do
invariant { exists k: int. 0 <= k /\ !a = fib k <= x /\ !b = fib (k+1) }
invariant { 0 <= !k /\ !a = fib !k <= x /\ !b = fib (!k+1) }
invariant { 0 <= !a /\ 1 <= !b }
variant { 2*x - (!a + !b) }
let f = !a + !b in
a := !b;
b := f
b := f;
k := !k + 1
done;
!b
......
......@@ -47,7 +47,7 @@
</theory>
<theory name="SmallestFibAbove" proved="true">
<goal name="VC smallest_fib_above" expl="VC for smallest_fib_above" proved="true">
<proof prover="2"><result status="valid" time="0.12"/></proof>
<proof prover="4"><result status="valid" time="0.04"/></proof>
</goal>
</theory>
<theory name="Zeckendorf" proved="true">
......
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