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
|
; Formalizing Machine Semantics and Proving Code Correct
; (with ACL2)
; J Strother Moore
; Start up ACL2 and do:
(set-gag-mode nil)
(set-irrelevant-formals-ok t)
; --- cut here ---
(+ 2 3)
(cons 'monday (cons 'tuesday (cons 'wednesday nil)))
(include-book "models/jvm/m1/m1" :dir :system)
(in-package "M1")
(defun sq (x) (* x x))
(sq 7)
(defun ^ (i j)
(if (zp j)
1
(* i (^ i (- j 1)))))
(^ 2 5)
(thm (implies (and (natp i) (natp j) (natp k))
(equal (^ i (+ j k))
(* (^ i j) (^ i k)))))
(quote (end of demo 1))
(defconst *p*
; Register numbers: 0, 1, 2
; My names: i, j, k
'((ILOAD 1) ; 0
(IFEQ 10) ; 1 if j=0, goto 1+10
(ILOAD 0) ; 2
(ILOAD 2) ; 3
(IMUL) ; 4
(ISTORE 2) ; 5 k := i*k;
(ILOAD 1) ; 6
(ICONST -1) ; 7
(IADD) ; 8
(ISTORE 1) ; 9 j := j-1
(GOTO -10) ;10 goto 10-10
(ILOAD 2) ;11
(HALT)) ;12 ``return'' k
)
(defun ms (i j k)
(make-state 0 ; program counter
(list i j k) ; registers
nil ; stack
*p* ; program
))
(top (stack (m1 (ms 2 5 1) 1000)))
(top (stack (m1 (ms 2 64 1) 1000)))
(^ 2 64)
(defun clk (i j k)
(if (zp j)
3
(clk+ 11
(clk i (- j 1) (* i k)))))
(clk 2 5 1)
(clk 2 1000 1)
(top (stack (m1 (ms 2 1000 1) (clk 2 1000 1))))
(defthm code-is-correct
(implies (and (natp i)
(natp j)
(natp k))
(equal (m1 (ms i j k) (clk i j k))
(make-state 12
(list i 0 (* k (^ i j)))
(push (* k (^ i j)) nil)
*p*))))
(defthm corr
(implies (and (natp i)
(natp j)
(natp k))
(let ((fin-st (m1 (ms i j k) (clk i j k))))
(and (haltedp fin-st)
(equal (top (stack fin-st))
(* k (^ i j)))))))
(quote (demo of symbolic execuation))
(defthm this-is-not-a-theorem
(implies (and (natp i)
(natp j)
(natp k))
(equal (m1 (ms i j k) 11) xxx)))
(quote (end of demo 2))
|
