110 "append_name" ("\"append\"") |
110 "append_name" ("\"append\"") |
111 "makelist_name" ("\"makelist\"") |
111 "makelist_name" ("\"makelist\"") |
112 "val_nam" ("\"val\"") |
112 "val_nam" ("\"val\"") |
113 "next_nam" ("\"next\"") |
113 "next_nam" ("\"next\"") |
114 |
114 |
115 code_type cnam and vnam and mname and loc_ |
|
116 (SML "string" and "string" and "string" and "IntInf.int") |
|
117 |
|
118 instance cnam :: eq |
|
119 and cname :: eq |
|
120 and vname :: eq |
|
121 and mname :: eq |
|
122 and ty :: eq |
|
123 and val :: eq |
|
124 and instr :: eq .. |
|
125 |
|
126 definition |
|
127 arbitrary_val :: val where |
|
128 [symmetric, code inline]: "arbitrary_val = arbitrary" |
|
129 definition |
|
130 arbitrary_cname :: cname where |
|
131 [symmetric, code inline]: "arbitrary_cname = arbitrary" |
|
132 |
|
133 definition "unit' = Unit" |
|
134 definition "object' = Object" |
|
135 |
|
136 code_axioms |
|
137 arbitrary_val \<equiv> unit' |
|
138 arbitrary_cname \<equiv> object' |
|
139 |
|
140 code_const list_nam and test_nam and append_name and makelist_name and val_nam and next_nam |
|
141 (SML "\"list\"" and "\"test\"" and "\"append\"" |
|
142 and "\"makelist\"" and "\"val\"" and "\"next\"") |
|
143 |
|
144 axiomatization |
|
145 incr_loc :: "loc_ \<Rightarrow> loc_" |
|
146 and zero_loc :: "loc_" |
|
147 |
|
148 code_const incr_loc and zero_loc |
|
149 (SML "(op +)/ (_, 1)" and "0") |
|
150 |
|
151 axiomatization |
|
152 test_loc :: "(loc_ \<Rightarrow> bool) \<Rightarrow> (loc_ \<Rightarrow> 'a) \<Rightarrow> loc_ \<Rightarrow> 'a" where |
|
153 "test_loc p v l = (if p l then v l else test_loc p v (incr l))" |
|
154 |
|
155 definition |
|
156 new_addr' :: "(loc \<Rightarrow> (cname \<times> (vname \<times> cname \<Rightarrow> val option)) option) \<Rightarrow> loc \<times> val option" where |
|
157 "new_addr' hp = |
|
158 test_loc (\<lambda>i. hp (Loc i) = None) (\<lambda>i. (Loc i, None)) zero_loc" |
|
159 |
|
160 lemma [code func]: |
|
161 "wf_class = wf_class" .. |
|
162 |
|
163 code_const |
|
164 wf_class (SML "(fn `_ => true)") |
|
165 |
|
166 code_axioms |
|
167 new_Addr \<equiv> new_addr' |
|
168 |
|
169 definition |
115 definition |
170 "test = exec (E, start_state E test_name makelist_name)" |
116 "test = exec (E, start_state E test_name makelist_name)" |
171 |
117 |
172 |
118 |
173 subsection {* Single step execution *} |
119 subsection {* Single step execution *} |
174 |
120 |
175 code_module JVM |
121 code_module JVM |
176 contains |
122 contains |
177 test = "exec (E, start_state E test_name makelist_name)" |
123 exec = exec |
|
124 test = test |
178 |
125 |
179 ML {* |
126 ML {* |
180 JVM.test; |
127 JVM.test; |
181 JVM.exec (JVM.E, JVM.the it); |
128 JVM.exec (JVM.E, JVM.the it); |
182 JVM.exec (JVM.E, JVM.the it); |
129 JVM.exec (JVM.E, JVM.the it); |