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))))
|