1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
(* Euler Project, problem 2
Each new term in the Fibonacci sequence is generated by adding the
previous two terms. By starting with 1 and 2, the first 10 terms will
be:
1, 2, 3, 5, 8, 13, 21, 34, 55, 89, ...
By considering the terms in the Fibonacci sequence whose values do not
exceed four million, find the sum of the even-valued terms. *)
(** {2 Sum of even-valued Fibonacci numbers} *)
theory FibSumEven
use int.Int
use int.Fibonacci
use int.ComputerDivision
(* [fib_sum_even m n] is the sum of even-valued terms of the
Fibonacci sequence from index 0 to n-1, that do not exceed m *)
function fib_sum_even int int : int
axiom SumZero: forall m:int. fib_sum_even m 0 = 0
axiom SumEvenLe: forall n m:int.
n >= 0 -> fib n <= m -> mod (fib n) 2 = 0 ->
fib_sum_even m (n+1) = fib_sum_even m n + fib n
axiom SumEvenGt: forall n m:int.
n >= 0 -> fib n > m -> mod (fib n) 2 = 0 ->
fib_sum_even m (n+1) = fib_sum_even m n
axiom SumOdd: forall n m:int.
n >= 0 -> mod (fib n) 2 <> 0 ->
fib_sum_even m (n+1) = fib_sum_even m n
predicate is_fib_sum_even (m:int) (sum:int) =
exists n:int.
sum = fib_sum_even m n /\ fib n > m
(* Note: we take for granted that [fib] is an
increasing sequence *)
end
module FibOnlyEven
use int.Int
use int.ComputerDivision
use int.Fibonacci
let rec lemma fib_even_3n (n:int)
requires { n >= 0 }
variant { n }
ensures { mod (fib n) 2 = 0 <-> mod n 3 = 0 }
= if n > 2 then fib_even_3n (n-3)
function fib_even (n: int) : int = fib (3 * n)
lemma fib_even0: fib_even 0 = 0
lemma fib_even1: fib_even 1 = 2
lemma fib_evenn: forall n:int [fib_even n].
n >= 2 -> fib_even n = 4 * fib_even (n-1) + fib_even (n-2)
end
module Solve
use int.Int
use ref.Ref
use int.Fibonacci
use FibSumEven
use FibOnlyEven
let f m : int
requires { m >= 0 }
ensures { exists n:int. result = fib_sum_even m n /\ fib n > m }
= let x = ref 0 in
let y = ref 2 in
let sum = ref 0 in
let ghost n = ref 0 in
let ghost k = ref 0 in
while !x <= m do
invariant { !n >= 0 }
invariant { !k >= 0 }
invariant { !x = fib_even !n }
invariant { !x = fib !k }
invariant { !y = fib_even (!n+1) }
invariant { !y = fib (!k+3) }
invariant { !sum = fib_sum_even m !k }
invariant { 0 <= !x < !y }
variant { m - !x }
let tmp = !x in
x := !y;
y := 4 * !y + tmp;
sum := !sum + tmp;
n := !n + 1;
k := !k + 3
done;
!sum
let run () = f 4_000_000 (* should be 4613732 *)
exception BenchFailure
let bench () raises { BenchFailure -> true } =
let x = run () in
if x <> 4613732 then raise BenchFailure;
x
end
|
