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 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195
|
; Copyright (C) 2000 Panagiotis Manolios and J Strother Moore
; This program is free software; you can redistribute it and/or modify
; it under the terms of the GNU General Public License as published by
; the Free Software Foundation; either version 2 of the License, or
; (at your option) any later version.
; This program is distributed in the hope that it will be useful,
; but WITHOUT ANY WARRANTY; without even the implied warranty of
; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
; GNU General Public License for more details.
; You should have received a copy of the GNU General Public License
; along with this program; if not, write to the Free Software
; Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
; Written by Panagiotis Manolios who can be reached as follows.
; Email: pete@cs.utexas.edu, moore@cs.utexas.edu
; Postal Mail:
; Department of Computer Science
; The University of Texas at Austin
; Austin, TX 78701 USA
; (include-book "/v/hank/v104/text/tjvm/examples")
; (certify-book "tjvm-examples" 1)
(in-package "TJVM")
(include-book "defpun")
(defmacro defpun (&rest rest) (cons 'acl2::defpun rest))
(defun haltedp (s) (equal s (step s)))
(defpun stepw (s)
(if (haltedp s)
s
(stepw (step s))))
(defun == (a b)(equal (stepw a) (stepw b)))
(defequiv ==)
(in-theory (disable step-opener))
(defthm stepw-step
(equal (stepw s) (stepw (step s)))
:rule-classes nil)
; This event is here only so we can exhibit it in the paper.
(defthm ==-step
(== (make-state call-stack heap class-table)
(step (make-state call-stack heap class-table)))
:rule-classes nil)
(defthm ==-stepper
(implies (and (consp (NTH (PC (TOP call-stack))
(PROGRAM (TOP call-stack))))
(not (equal (car (NTH (PC (TOP call-stack))
(PROGRAM (TOP call-stack))))
'invokestatic)))
(== (make-state
call-stack
heap
class-table)
(step (make-state
call-stack
heap
class-table))))
:hints (("Goal" :in-theory (disable step))))
(defthm general-==-stepper
(implies (equal call-stack call-stack) ; not an abbreviation rule!
(== (make-state call-stack
heap
class-table)
(step (make-state call-stack
heap
class-table)))))
(defun stepn (s n)
(if (zp n)
s
(stepn (step s) (- n 1))))
(defthm ==-stepn
(== (stepn s n) s))
(defthm ==-Y
(implies (== (stepn s1 n)
(stepn s2 m))
(== s1 s2))
:rule-classes nil)
(in-theory (disable general-==-stepper ==))
(in-theory (enable step))
(defun next-instruction (call-stack)
(nth (pc (top call-stack))
(program (top call-stack))))
; A consequence of this setup is that for every primitive instruction
; except for invokestatic we have a theorem like:
(defthm ==-load
(implies (and (equal (next-instruction call-stack)
`(load ,var)))
(== (make-state call-stack
heap
class-table)
(make-state
(push (make-frame (+ 1 (pc (top call-stack)))
(locals (top call-stack))
(push (binding var (locals (top call-stack)))
(stack (top call-stack)))
(program (top call-stack)))
(pop call-stack))
heap
class-table)))
:rule-classes nil)
; Ok, that completes the general work. Now let's deal with fact.
(defun fact-==-hint (call-stack heap table n)
(if (zp n)
(list call-stack heap table)
(fact-==-hint
(push (make-frame 6
(list (cons 'n (top (stack (top call-stack)))))
(push (- (top (stack (top call-stack))) 1)
(push (top (stack (top call-stack)))
nil))
(method-program (\bf_fact)))
(push (make-frame (+ 1 (pc (top call-stack)))
(locals (top call-stack))
(pop (stack (top call-stack)))
(program (top call-stack)))
(pop call-stack)))
heap
table
(- n 1))))
(defun Math-class-loadedp (class-table)
(equal (assoc-equal "Math" class-table)
(\bfMath-class)))
; The following lemma is proved just so we can prove the next
; theorem without any hints. The hintless version is shown in the paper.
(defthm ==-invokestatic-fact-lemma
(implies (and (equal (next-instruction call-stack)
'(invokestatic "Math" "fact" 1))
(Math-class-loadedp class-table)
(equal n (top (stack (top call-stack))))
(natp n))
(== (make-state call-stack
heap
class-table)
(make-state
(push (make-frame (+ 1 (pc (top call-stack)))
(locals (top call-stack))
(push (fact n)
(pop (stack (top call-stack))))
(program (top call-stack)))
(pop call-stack))
heap
class-table)))
:hints (("Goal" :in-theory (enable general-==-stepper top-frame)
:restrict ((general-==-STEPPER
((call-stack call-stack)
(heap heap)
(class-table class-table))))
:induct (fact-==-hint call-stack heap class-table n))))
(defthm ==-invokestatic-fact
(implies (and (equal (next-instruction call-stack)
'(invokestatic "Math" "fact" 1))
(Math-class-loadedp class-table)
(equal n (top (stack (top call-stack))))
(natp n))
(== (make-state call-stack
heap
class-table)
(make-state
(push (make-frame (+ 1 (pc (top call-stack)))
(locals (top call-stack))
(push (fact n)
(pop (stack (top call-stack))))
(program (top call-stack)))
(pop call-stack))
heap
class-table))))
|