fibonacci.mlw 3.33 KB
 MARCHE Claude committed Apr 07, 2011 1 `````` `````` Jean-Christophe Filliâtre committed Apr 11, 2011 2 ``````theory Fibonacci "Fibonacci numbers" `````` MARCHE Claude committed Apr 07, 2011 3 `````` `````` Jean-Christophe Filliâtre committed Apr 11, 2011 4 `````` use export int.Int `````` MARCHE Claude committed Apr 07, 2011 5 `````` `````` Andrei Paskevich committed Jun 29, 2011 6 `````` function fib int : int `````` MARCHE Claude committed Apr 07, 2011 7 `````` `````` Jean-Christophe Filliâtre committed Apr 11, 2011 8 9 `````` axiom fib0: fib 0 = 0 axiom fib1: fib 1 = 1 `````` MARCHE Claude committed May 04, 2011 10 `````` axiom fibn: forall n:int. n >= 2 -> fib n = fib (n-1) + fib (n-2) `````` Jean-Christophe Filliâtre committed Apr 11, 2011 11 12 13 14 15 16 17 `````` end theory FibonacciTest use import Fibonacci `````` Jean-Christophe Filliâtre committed May 20, 2011 18 `````` lemma isfib_2_1 : fib 2 = 1 `````` Jean-Christophe Filliâtre committed Apr 11, 2011 19 20 21 `````` lemma isfib_6_8 : fib 6 = 8 lemma not_isfib_2_2 : fib 2 <> 2 `````` MARCHE Claude committed Apr 07, 2011 22 23 24 25 26 27 28 `````` end module FibonacciLinear use import Fibonacci use import int.Int `````` Andrei Paskevich committed Oct 13, 2012 29 `````` use import ref.Ref `````` MARCHE Claude committed Apr 07, 2011 30 `````` `````` Andrei Paskevich committed Oct 13, 2012 31 32 33 34 `````` let fib (n:int) : int requires { n >= 0 } ensures { fib n = result} = let y = ref 0 in `````` MARCHE Claude committed Apr 07, 2011 35 `````` let x = ref 1 in `````` Jean-Christophe Filliâtre committed Apr 11, 2011 36 `````` for i = 0 to n - 1 do `````` Andrei Paskevich committed Jun 29, 2011 37 `````` invariant { 0 <= i <= n /\ fib (i+1) = !x /\ fib i = !y } `````` MARCHE Claude committed Apr 07, 2011 38 `````` let aux = !y in `````` Jean-Christophe Filliâtre committed May 20, 2011 39 `````` y := !x; `````` MARCHE Claude committed Apr 07, 2011 40 41 42 43 44 `````` x := !x + aux done; !y end `````` Jean-Christophe Filliâtre committed Apr 08, 2011 45 `````` `````` Jean-Christophe Filliâtre committed Sep 12, 2013 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 ``````module FibRecGhost "recursive version, using ghost code" use import Fibonacci use import int.Int let rec fib_aux (ghost n: int) (a b k: int) : int requires { 0 <= n && a = fib n && b = fib (n+1) } ensures { result = fib (n+k) } = if k = 0 then a else fib_aux (n+1) b (a+b) (k-1) let fib (n: int) : int requires { 0 <= n } ensures { result = fib n } = fib_aux 0 0 1 n end module FibRecNoGhost "recursive version, without ghost code" use import Fibonacci use import int.Int let rec fib_aux (a b k: int) : int requires { exists n: int. 0 <= n && a = fib n && b = fib (n+1) } ensures { forall n: int. 0 <= n && a = fib n && b = fib (n+1) -> result = fib (n+k) } = if k = 0 then a else fib_aux b (a+b) (k-1) let fib (n: int) : int requires { 0 <= n } ensures { result = fib n } = fib_aux 0 1 n end `````` Jean-Christophe Filliâtre committed Apr 08, 2011 81 82 83 84 ``````theory Mat22 "2x2 integer matrices" use import int.Int `````` Andrei Paskevich committed Oct 13, 2012 85 `````` type t = { a11: int; a12: int; a21: int; a22: int } `````` Jean-Christophe Filliâtre committed Apr 08, 2011 86 `````` `````` Andrei Paskevich committed Oct 13, 2012 87 `````` constant id : t = { a11 = 1; a12 = 0; a21 = 0; a22 = 1 } `````` Jean-Christophe Filliâtre committed Apr 08, 2011 88 `````` `````` Andrei Paskevich committed Jun 29, 2011 89 `````` function mult (x: t) (y: t) : t = `````` Andrei Paskevich committed Oct 13, 2012 90 `````` { `````` Jean-Christophe Filliâtre committed Apr 08, 2011 91 `````` a11 = x.a11 * y.a11 + x.a12 * y.a21; a12 = x.a11 * y.a12 + x.a12 * y.a22; `````` Jean-Christophe Filliâtre committed Apr 11, 2011 92 `````` a21 = x.a21 * y.a11 + x.a22 * y.a21; a22 = x.a21 * y.a12 + x.a22 * y.a22; `````` Andrei Paskevich committed Oct 13, 2012 93 `````` } `````` Jean-Christophe Filliâtre committed Apr 08, 2011 94 `````` `````` Jean-Christophe Filliâtre committed Apr 11, 2011 95 `````` (* holds, but not useful *) `````` Andrei Paskevich committed Jun 29, 2011 96 `````` (* clone algebra.Assoc with type t = t, function op = mult, lemma Assoc *) `````` Jean-Christophe Filliâtre committed Apr 08, 2011 97 `````` `````` Jean-Christophe Filliâtre committed May 20, 2011 98 `````` clone export `````` Andrei Paskevich committed Jun 29, 2011 99 `````` int.Exponentiation with type t = t, function one = id, function (*) = mult `````` Jean-Christophe Filliâtre committed Apr 08, 2011 100 101 102 103 104 105 106 `````` end module FibonacciLogarithmic use import Fibonacci use import int.EuclideanDivision `````` Jean-Christophe Filliâtre committed Apr 08, 2011 107 `````` use import Mat22 `````` Jean-Christophe Filliâtre committed Apr 08, 2011 108 `````` `````` Andrei Paskevich committed Oct 13, 2012 109 110 `````` constant m1110 : t = { a11 = 1; a12 = 1; a21 = 1; a22 = 0 } `````` Jean-Christophe Filliâtre committed Apr 08, 2011 111 `````` `````` Jean-Christophe Filliâtre committed Apr 08, 2011 112 113 `````` (* computes ((1 1) (1 0))^n in O(log(n)) time `````` Jean-Christophe Filliâtre committed May 20, 2011 114 `````` since it is a matrix of the shape ((a+b b) (b a)), `````` Jean-Christophe Filliâtre committed Apr 08, 2011 115 116 `````` we only return the pair (a, b) *) `````` Andrei Paskevich committed Oct 13, 2012 117 118 119 120 121 `````` let rec logfib n variant { n } requires { n >= 0 } ensures { let a, b = result in power m1110 n = { a11 = a+b; a12 = b; a21 = b; a22 = a } } = if n = 0 then `````` Jean-Christophe Filliâtre committed Apr 08, 2011 122 `````` (1, 0) `````` Jean-Christophe Filliâtre committed Apr 08, 2011 123 124 125 126 `````` else begin let a, b = logfib (div n 2) in let c = a + b in if mod n 2 = 0 then `````` Jean-Christophe Filliâtre committed Apr 11, 2011 127 `````` (a*a + b*b, b*(a + c)) `````` Jean-Christophe Filliâtre committed Apr 08, 2011 128 `````` else `````` Jean-Christophe Filliâtre committed Apr 11, 2011 129 `````` (b*(a + c), c*c + b*b) `````` Jean-Christophe Filliâtre committed Apr 08, 2011 130 131 `````` end `````` Jean-Christophe Filliâtre committed Apr 08, 2011 132 133 134 135 136 137 138 139 `````` (* by induction, we easily prove that (1 1)^n = (F(n+1) F(n) ) (1 0) (F(n) F(n-1)) thus, we can compute F(n) in O(log(n)) using funtion logfib above *) `````` Jean-Christophe Filliâtre committed May 20, 2011 140 `````` lemma fib_m : `````` Jean-Christophe Filliâtre committed Apr 08, 2011 141 `````` forall n: int. n >= 0 -> `````` Andrei Paskevich committed Jun 29, 2011 142 `````` let p = power m1110 n in fib (n+1) = p.a11 /\ fib n = p.a21 `````` Jean-Christophe Filliâtre committed Apr 08, 2011 143 `````` `````` Andrei Paskevich committed Oct 13, 2012 144 `````` let fibo n requires { n >= 0 } ensures { result = fib n } = `````` Jean-Christophe Filliâtre committed Apr 08, 2011 145 146 `````` let _, b = logfib n in b `````` MARCHE Claude committed Sep 14, 2013 147 148 149 150 151 152 `````` let test0 () = fibo 0 let test1 () = fibo 1 let test7 () = fibo 7 let test42 () = fibo 42 `````` Jean-Christophe Filliâtre committed Apr 08, 2011 153 ``end``