Commit f3f49b3b authored by Jean-Christophe Filliâtre's avatar Jean-Christophe Filliâtre
Browse files

new library int.Fibonacci

parent 496c8a36
(* Fibonacci function with memoisation *)
module M
module FibMemo
use import int.Int
use import int.Fibonacci
use import ref.Ref
function fib int : int
axiom Fib_def : forall n:int. fib n =
if n <= 1 then 1 else fib (n-1) + fib (n-2)
type option 'a = None | Some 'a
use import map.Map as M
......@@ -36,7 +32,7 @@ module M
ensures { result = fib n /\ inv !table }
variant { 2*n }
if n <= 1 then
1
n
else
memo_fibo (n-1) + memo_fibo (n-2)
......
......@@ -7,6 +7,10 @@
version="0.95.1"/>
<prover
id="1"
name="Alt-Ergo"
version="0.95.2"/>
<prover
id="2"
name="CVC3"
version="2.4.1"/>
<file
......@@ -14,7 +18,7 @@
verified="true"
expanded="true">
<theory
name="M"
name="FibMemo"
locfile="../fib_memo.mlw"
loclnum="3" loccnumb="7" loccnume="8"
verified="true"
......@@ -22,18 +26,18 @@
<goal
name="WP_parameter fibo"
locfile="../fib_memo.mlw"
loclnum="34" loccnumb="10" loccnume="14"
loclnum="30" loccnumb="10" loccnume="14"
expl="VC for fibo"
sum="1c92730ae7a166108cdfa6c2c6409c1e"
sum="a3a8eda4fb2be551467fdd49b1e76c6e"
proved="true"
expanded="true"
shape="iainvV5Aainfix =ainfix +afibV4afibV2afibV0IainvV5FAainvV3Aainfix &lt;=c0V4Aainfix &lt;ainfix +ainfix *c2V4c1ainfix *c2V0Aainfix &lt;=c0ainfix *c2V0Lainfix -V0c1IainvV3FAainvV1Aainfix &lt;=c0V2Aainfix &lt;ainfix +ainfix *c2V2c1ainfix *c2V0Aainfix &lt;=c0ainfix *c2V0Lainfix -V0c2ainvV1Aainfix =c1afibV0ainfix &lt;=V0c1IainvV1Aainfix &lt;=c0V0FF">
shape="iainvV5Aainfix =ainfix +afibV4afibV2afibV0IainvV5FAainvV3Aainfix &lt;=c0V4Aainfix &lt;ainfix +ainfix *c2V4c1ainfix *c2V0Aainfix &lt;=c0ainfix *c2V0Lainfix -V0c1IainvV3FAainvV1Aainfix &lt;=c0V2Aainfix &lt;ainfix +ainfix *c2V2c1ainfix *c2V0Aainfix &lt;=c0ainfix *c2V0Lainfix -V0c2ainvV1Aainfix =V0afibV0ainfix &lt;=V0c1IainvV1Aainfix &lt;=c0V0FF">
<label
name="expl:VC for fibo"/>
<proof
prover="0"
timelimit="10"
memlimit="0"
prover="1"
timelimit="6"
memlimit="1000"
obsolete="false"
archived="false">
<result status="valid" time="0.02"/>
......@@ -42,9 +46,9 @@
<goal
name="WP_parameter memo_fibo"
locfile="../fib_memo.mlw"
loclnum="43" loccnumb="7" loccnume="16"
loclnum="39" loccnumb="7" loccnume="16"
expl="VC for memo_fibo"
sum="b018158e5afc0812ef7e860f41f89dff"
sum="3acd9e9482cadd41f279143eec17329d"
proved="true"
expanded="true"
shape="ainvV4Aainfix =V3afibV0Iainfix =V4asetV2V0aSomeV3FIainvV2LafibV0FAainvV1Aainfix &lt;=c0V0Aainfix &lt;ainfix *c2V0ainfix +ainfix *c2V0c1Aainfix &lt;=c0ainfix +ainfix *c2V0c1Iainfix =agetV1V0aNoneAainvV1Aainfix =V5afibV0Iainfix =agetV1V0aSomeV5FIainvV1Aainfix &lt;=c0V0FF">
......@@ -57,9 +61,9 @@
<goal
name="WP_parameter memo_fibo.1"
locfile="../fib_memo.mlw"
loclnum="43" loccnumb="7" loccnume="16"
loclnum="39" loccnumb="7" loccnume="16"
expl="1. postcondition"
sum="316195b57b9a183f6b6c75aacee91777"
sum="721b426fbf3f2646870759e3930c9806"
proved="true"
expanded="true"
shape="postconditionainvV1Aainfix =V2afibV0Iainfix =agetV1V0aSomeV2FIainvV1Aainfix &lt;=c0V0FF">
......@@ -77,9 +81,9 @@
<goal
name="WP_parameter memo_fibo.2"
locfile="../fib_memo.mlw"
loclnum="43" loccnumb="7" loccnume="16"
loclnum="39" loccnumb="7" loccnume="16"
expl="2. variant decrease"
sum="9d90acbce96fa42b719eaf6aca980e50"
sum="1df4dba295e92068f22a2d699f92e0de"
proved="true"
expanded="false"
shape="variant decreaseainfix &lt;ainfix *c2V0ainfix +ainfix *c2V0c1Aainfix &lt;=c0ainfix +ainfix *c2V0c1Iainfix =agetV1V0aNoneIainvV1Aainfix &lt;=c0V0FF">
......@@ -97,9 +101,9 @@
<goal
name="WP_parameter memo_fibo.3"
locfile="../fib_memo.mlw"
loclnum="43" loccnumb="7" loccnume="16"
loclnum="39" loccnumb="7" loccnume="16"
expl="3. precondition"
sum="b9069385630ec027acb3fe9c6f6c7a4d"
sum="11605f571d7d37e1a881c8932a63c25a"
proved="true"
expanded="true"
shape="preconditionainvV1Aainfix &lt;=c0V0Iainfix =agetV1V0aNoneIainvV1Aainfix &lt;=c0V0FF">
......@@ -117,16 +121,16 @@
<goal
name="WP_parameter memo_fibo.4"
locfile="../fib_memo.mlw"
loclnum="43" loccnumb="7" loccnume="16"
loclnum="39" loccnumb="7" loccnume="16"
expl="4. postcondition"
sum="15172e65467ccc671126b6844ce65ef5"
sum="b904ccf2d4702a4d58f8fd5a49c03549"
proved="true"
expanded="true"
shape="postconditionainvV4Aainfix =V3afibV0Iainfix =V4asetV2V0aSomeV3FIainvV2LafibV0FIainvV1Aainfix &lt;=c0V0Iainfix =agetV1V0aNoneIainvV1Aainfix &lt;=c0V0FF">
<label
name="expl:VC for memo_fibo"/>
<proof
prover="1"
prover="2"
timelimit="10"
memlimit="0"
obsolete="false"
......
theory Fibonacci "Fibonacci numbers"
use export int.Int
function fib int : int
axiom fib0: fib 0 = 0
axiom fib1: fib 1 = 1
axiom fibn: forall n:int. n >= 2 -> fib n = fib (n-1) + fib (n-2)
end
theory FibonacciTest
use import Fibonacci
use import int.Fibonacci
lemma isfib_2_1 : fib 2 = 1
lemma isfib_6_8 : fib 6 = 8
......@@ -24,7 +12,7 @@ end
module FibonacciLinear
use import Fibonacci
use import int.Fibonacci
use import int.Int
use import ref.Ref
......@@ -45,7 +33,7 @@ end
module FibRecGhost "recursive version, using ghost code"
use import Fibonacci
use import int.Fibonacci
use import int.Int
let rec fib_aux (ghost n: int) (a b k: int) : int
......@@ -71,7 +59,7 @@ end
module FibRecNoGhost "recursive version, without ghost code"
use import Fibonacci
use import int.Fibonacci
use import int.Int
let rec fib_aux (a b k: int) : int
......@@ -113,7 +101,7 @@ end
module FibonacciLogarithmic
use import Fibonacci
use import int.Fibonacci
use import int.EuclideanDivision
use import Mat22
......
This diff is collapsed.
......@@ -444,3 +444,16 @@ theory Induction
forall n:int. bound <= n -> p n
end
theory Fibonacci "Fibonacci numbers"
use export Int
function fib int : int
axiom fib0: fib 0 = 0
axiom fib1: fib 1 = 1
axiom fibn: forall n:int. n >= 2 -> fib n = fib (n-1) + fib (n-2)
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