1(* Title: HOL/MicroJava/JVM/JVMListExample.thy 2 Author: Stefan Berghofer 3*) 4 5section \<open>Example for generating executable code from JVM semantics \label{sec:JVMListExample}\<close> 6 7theory JVMListExample 8imports "../J/SystemClasses" JVMExec 9begin 10 11text \<open> 12 Since the types @{typ cnam}, \<open>vnam\<close>, and \<open>mname\<close> are 13 anonymous, we describe distinctness of names in the example by axioms: 14\<close> 15axiomatization list_nam test_nam :: cnam 16 where distinct_classes: "list_nam \<noteq> test_nam" 17 18axiomatization append_name makelist_name :: mname 19 where distinct_methods: "append_name \<noteq> makelist_name" 20 21axiomatization val_nam next_nam :: vnam 22 where distinct_fields: "val_nam \<noteq> next_nam" 23 24axiomatization 25 where nat_to_loc'_inject: "nat_to_loc' l = nat_to_loc' l' \<longleftrightarrow> l = l'" 26 27definition list_name :: cname 28 where "list_name = Cname list_nam" 29 30definition test_name :: cname 31 where "test_name = Cname test_nam" 32 33definition val_name :: vname 34 where "val_name = VName val_nam" 35 36definition next_name :: vname 37 where "next_name = VName next_nam" 38 39definition append_ins :: bytecode where 40 "append_ins = 41 [Load 0, 42 Getfield next_name list_name, 43 Dup, 44 LitPush Null, 45 Ifcmpeq 4, 46 Load 1, 47 Invoke list_name append_name [Class list_name], 48 Return, 49 Pop, 50 Load 0, 51 Load 1, 52 Putfield next_name list_name, 53 LitPush Unit, 54 Return]" 55 56definition list_class :: "jvm_method class" where 57 "list_class = 58 (Object, 59 [(val_name, PrimT Integer), (next_name, Class list_name)], 60 [((append_name, [Class list_name]), PrimT Void, 61 (3, 0, append_ins,[(1,2,8,Xcpt NullPointer)]))])" 62 63definition make_list_ins :: bytecode where 64 "make_list_ins = 65 [New list_name, 66 Dup, 67 Store 0, 68 LitPush (Intg 1), 69 Putfield val_name list_name, 70 New list_name, 71 Dup, 72 Store 1, 73 LitPush (Intg 2), 74 Putfield val_name list_name, 75 New list_name, 76 Dup, 77 Store 2, 78 LitPush (Intg 3), 79 Putfield val_name list_name, 80 Load 0, 81 Load 1, 82 Invoke list_name append_name [Class list_name], 83 Pop, 84 Load 0, 85 Load 2, 86 Invoke list_name append_name [Class list_name], 87 Return]" 88 89definition test_class :: "jvm_method class" where 90 "test_class = 91 (Object, [], 92 [((makelist_name, []), PrimT Void, (3, 2, make_list_ins,[]))])" 93 94definition E :: jvm_prog where 95 "E = SystemClasses @ [(list_name, list_class), (test_name, test_class)]" 96 97code_datatype list_nam test_nam 98lemma equal_cnam_code [code]: 99 "HOL.equal list_nam list_nam \<longleftrightarrow> True" 100 "HOL.equal test_nam test_nam \<longleftrightarrow> True" 101 "HOL.equal list_nam test_nam \<longleftrightarrow> False" 102 "HOL.equal test_nam list_nam \<longleftrightarrow> False" 103 by(simp_all add: distinct_classes distinct_classes[symmetric] equal_cnam_def) 104 105code_datatype append_name makelist_name 106lemma equal_mname_code [code]: 107 "HOL.equal append_name append_name \<longleftrightarrow> True" 108 "HOL.equal makelist_name makelist_name \<longleftrightarrow> True" 109 "HOL.equal append_name makelist_name \<longleftrightarrow> False" 110 "HOL.equal makelist_name append_name \<longleftrightarrow> False" 111 by(simp_all add: distinct_methods distinct_methods[symmetric] equal_mname_def) 112 113code_datatype val_nam next_nam 114lemma equal_vnam_code [code]: 115 "HOL.equal val_nam val_nam \<longleftrightarrow> True" 116 "HOL.equal next_nam next_nam \<longleftrightarrow> True" 117 "HOL.equal val_nam next_nam \<longleftrightarrow> False" 118 "HOL.equal next_nam val_nam \<longleftrightarrow> False" 119 by(simp_all add: distinct_fields distinct_fields[symmetric] equal_vnam_def) 120 121 122lemma equal_loc'_code [code]: 123 "HOL.equal (nat_to_loc' l) (nat_to_loc' l') \<longleftrightarrow> l = l'" 124 by(simp add: equal_loc'_def nat_to_loc'_inject) 125 126definition undefined_cname :: cname 127 where [code del]: "undefined_cname = undefined" 128code_datatype Object Xcpt Cname undefined_cname 129declare undefined_cname_def[symmetric, code_unfold] 130 131definition undefined_val :: val 132 where [code del]: "undefined_val = undefined" 133declare undefined_val_def[symmetric, code_unfold] 134code_datatype Unit Null Bool Intg Addr undefined_val 135 136definition 137 "test = exec (E, start_state E test_name makelist_name)" 138 139ML_val \<open> 140 @{code test}; 141 @{code exec} (@{code E}, @{code the} it); 142 @{code exec} (@{code E}, @{code the} it); 143 @{code exec} (@{code E}, @{code the} it); 144 @{code exec} (@{code E}, @{code the} it); 145 @{code exec} (@{code E}, @{code the} it); 146 @{code exec} (@{code E}, @{code the} it); 147 @{code exec} (@{code E}, @{code the} it); 148 @{code exec} (@{code E}, @{code the} it); 149 @{code exec} (@{code E}, @{code the} it); 150 @{code exec} (@{code E}, @{code the} it); 151 @{code exec} (@{code E}, @{code the} it); 152 @{code exec} (@{code E}, @{code the} it); 153 @{code exec} (@{code E}, @{code the} it); 154 @{code exec} (@{code E}, @{code the} it); 155 @{code exec} (@{code E}, @{code the} it); 156 @{code exec} (@{code E}, @{code the} it); 157 @{code exec} (@{code E}, @{code the} it); 158 @{code exec} (@{code E}, @{code the} it); 159 @{code exec} (@{code E}, @{code the} it); 160 @{code exec} (@{code E}, @{code the} it); 161 @{code exec} (@{code E}, @{code the} it); 162 @{code exec} (@{code E}, @{code the} it); 163 @{code exec} (@{code E}, @{code the} it); 164 @{code exec} (@{code E}, @{code the} it); 165 @{code exec} (@{code E}, @{code the} it); 166 @{code exec} (@{code E}, @{code the} it); 167 @{code exec} (@{code E}, @{code the} it); 168 @{code exec} (@{code E}, @{code the} it); 169 @{code exec} (@{code E}, @{code the} it); 170 @{code exec} (@{code E}, @{code the} it); 171 @{code exec} (@{code E}, @{code the} it); 172 @{code exec} (@{code E}, @{code the} it); 173 @{code exec} (@{code E}, @{code the} it); 174 @{code exec} (@{code E}, @{code the} it); 175 @{code exec} (@{code E}, @{code the} it); 176 @{code exec} (@{code E}, @{code the} it); 177 @{code exec} (@{code E}, @{code the} it); 178 @{code exec} (@{code E}, @{code the} it); 179 @{code exec} (@{code E}, @{code the} it); 180 @{code exec} (@{code E}, @{code the} it); 181 @{code exec} (@{code E}, @{code the} it); 182 @{code exec} (@{code E}, @{code the} it); 183 @{code exec} (@{code E}, @{code the} it); 184 @{code exec} (@{code E}, @{code the} it); 185 @{code exec} (@{code E}, @{code the} it); 186 @{code exec} (@{code E}, @{code the} it); 187 @{code exec} (@{code E}, @{code the} it); 188 @{code exec} (@{code E}, @{code the} it); 189 @{code exec} (@{code E}, @{code the} it); 190 @{code exec} (@{code E}, @{code the} it); 191 @{code exec} (@{code E}, @{code the} it); 192 @{code exec} (@{code E}, @{code the} it); 193 @{code exec} (@{code E}, @{code the} it); 194\<close> 195 196end 197