File: talk1-input.lsp

package info (click to toggle)
acl2 8.6%2Bdfsg-3
  • links: PTS
  • area: main
  • in suites: sid
  • size: 1,138,276 kB
  • sloc: lisp: 17,818,294; java: 125,359; python: 28,122; javascript: 23,458; cpp: 18,851; ansic: 11,569; perl: 7,678; xml: 5,591; sh: 3,978; makefile: 3,840; ruby: 2,633; yacc: 1,126; ml: 763; awk: 295; csh: 233; lex: 197; php: 178; tcl: 49; asm: 23; haskell: 17
file content (111 lines) | stat: -rw-r--r-- 2,393 bytes parent folder | download | duplicates (5)
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))