File: consistent-state-step.lisp

package info (click to toggle)
acl2 8.6%2Bdfsg-2
  • links: PTS
  • area: main
  • in suites: trixie
  • size: 1,111,420 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,976; makefile: 3,833; ruby: 2,633; yacc: 1,126; ml: 763; awk: 295; csh: 233; lex: 197; php: 178; tcl: 49; asm: 23; haskell: 17
file content (99 lines) | stat: -rw-r--r-- 3,204 bytes parent folder | download | duplicates (2)
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
(in-package "ACL2")
(include-book "jvm-model")
(include-book "consistent-state")

(defun consistent-state-step (st)
  (let*  ((method-table (g 'method-table st))
          (call-stack   (g 'call-stack st)))
    (and (pc-in-range st)
         (wff-method-table (g 'method-table st))
         (consistent-call-stack call-stack method-table)
         (all-method-verified method-table))))



;; (defun consistent-state-step (st) 
;;   (let*  ((method-table (g 'method-table st))
;;           (call-stack   (g 'call-stack st)))
;;     (and (consistent-call-stack call-stack method-table)
;;          (all-method-verified method-table))))

(defthm consistent-state-step-implies-implies-consistent-state
  (implies (consistent-state-step s)
           (consistent-state s))
  :rule-classes nil)

;--- EXPORT --- 
(defthm consistent-call-stack-implied-by-consistent-state
  (implies (consistent-state st)
           (consistent-call-stack (g 'call-stack st)
                                  (g 'method-table st)))
  :hints (("Goal" :in-theory (enable consistent-state)))
  :rule-classes :forward-chaining)


(defthm consistent-state-all-method-verified
  (implies (consistent-state st)
           (all-method-verified (g 'method-table st)))
  :hints (("Goal" :in-theory (enable consistent-state)))
  :rule-classes :forward-chaining)


(defthm consistent-state-pc-in-range
  (implies (consistent-state st)
           (pc-in-range st))
  :hints (("Goal" :in-theory (enable consistent-state)))
  :rule-classes :forward-chaining)



(defthm consistent-state-wff-method-table
  (implies (consistent-state st)
           (wff-method-table (g 'method-table st)))
  :hints (("Goal" :in-theory (enable consistent-state)))
  :rule-classes :forward-chaining)


(defthm consistent-call-stack-implied-by-consistent-state-b
  (implies (consistent-state st)
           (consistent-call-stack (g 'call-stack st)
                                  (g 'method-table st)))
  :hints (("Goal" :in-theory (enable consistent-state))))

(defthm consistent-state-all-method-verified-b
  (implies (consistent-state st)
           (all-method-verified (g 'method-table st)))
  :hints (("Goal" :in-theory (enable consistent-state))))


(defthm consistent-state-pc-in-range-b
  (implies (consistent-state st)
           (pc-in-range st))
  :hints (("Goal" :in-theory (enable consistent-state))))



(defthm consistent-state-wff-method-table-b
  (implies (consistent-state st)
           (wff-method-table (g 'method-table st)))
  :hints (("Goal" :in-theory (enable consistent-state))))


;----------------------------------------------------------------------

(defthm consistent-state-current-method-bound
  (implies (consistent-state st)
           (bound? (G 'METHOD-NAME
                      (topx (G 'CALL-STACK ST)))
                   (G 'METHOD-TABLE ST)))
  :rule-classes :forward-chaining
  :hints (("Goal" :in-theory (enable consistent-state))))


(defthm consistent-state-current-method-bound-b
  (implies (consistent-state st)
           (assoc-equal (G 'METHOD-NAME
                           (car (G 'CALL-STACK ST)))
                        (G 'METHOD-TABLE ST)))
  :hints (("Goal" :in-theory (enable consistent-state))))