Attention une mise à jour du serveur va être effectuée le vendredi 16 avril entre 12h et 12h30. Cette mise à jour va générer une interruption du service de quelques minutes.

new example with Fibonacci numbers

parent 4243f4c8
......@@ -77,6 +77,30 @@ module FibRecNoGhost "recursive version, without ghost code"
end
module SmallestFibAbove
use import int.Fibonacci
use import int.Int
use import int.MinMax
use import ref.Ref
let smallest_fib_above (x: int) : int
requires { 0 <= x }
ensures { exists k: int. 0 <= k /\ fib k <= x < fib (k+1) }
=
let a = ref 0 in
let b = ref 1 in
while !b <= x do
invariant { exists k: int. 0 <= k /\ !a = fib k <= x /\ !b = fib (k+1) }
variant { 2*x - (!a + !b) }
let f = !a + !b in
a := !b;
b := f
done;
!b
end
theory Mat22 "2x2 integer matrices"
use import int.Int
......
This diff is collapsed.
......@@ -461,5 +461,7 @@ theory Fibonacci "Fibonacci numbers"
axiom fib1: fib 1 = 1
axiom fibn: forall n:int. n >= 2 -> fib n = fib (n-1) + fib (n-2)
lemma fib_pos: forall i: int. 1 <= i -> 0 < fib i
end
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