/
fib.imp
65 lines (57 loc) · 1.79 KB
/
fib.imp
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
; A logic programming-style definition of fibonacci
(axiom {FIB 0 0})
(axiom {FIB 1 1})
(axiom {impl (>= i 0) (FIB i a) (FIB (+ i 1) b) (FIB (+ i 2) (+ a b))})
; A recursive procedure. Note that if an argument is a variable, it is
; given by reference. If you want to give the value of a variable x,
; use (val x) as the argument.
(define* (fib n res)
{and (>= n 0) (init n)} ; precondition
{FIB init-n res} ; postcondition
n ; variant (a value that decreases for each recursive call)
(if (= n 0) (res := 0)
(if (= n 1) (res := 1)
(begin
(fib (- n 2) a)
(fib (- n 1) b)
; Z3 needs a little help here
(assert {and (>= n 2) (= n init-n) (FIB (- n 2) a) (FIB (- n 1) b)})
(res := (+ a b))))))
; An iterative version of fib
(define* (swap x y)
{init x y}
{and (= x init-y) (= y init-x)}
0
(begin
(tmp := x)
(x := y)
(y := tmp)))
(define* (fib-iter n res)
{and (>= n 0) (init n)}
{FIB init-n res}
n
(begin
(res := 0)
(aux := 1)
(while*
{and (>= n 0)
(>= (- init-n n) 0)
(FIB (- init-n n) res)
(FIB (+ (- init-n n) 1) aux)}
n
(not (= n 0))
(begin
(swap res aux) ; the default is by reference
(aux := (+ res aux))
(n := (- n 1))))))
; Let's call our procedures. Note that if we remove the val annotation
; from fib, the postcondition does not hold, as the specification of
; fib does not guarantee that it does not change n. But with the val
; annotation, we're safe! (Otherwie, we could add (init n) and then
; call fib without any annotation, but formulate the postcondition as
; (FIB init-n res-rec).)
(begin
(assert {>= n 0})
(fib-iter (val n) res-iter)
(fib (val n) res-rec)
(assert {and (FIB n res-iter) (FIB n res-rec)}))