src/HOL/MicroJava/JVM/JVMListExample.thy
changeset 12951 a9fdcb71d252
parent 12911 704713ca07ea
child 12973 8040cce614e5
     1.1 --- a/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Feb 26 13:47:19 2002 +0100
     1.2 +++ b/src/HOL/MicroJava/JVM/JVMListExample.thy	Tue Feb 26 15:45:32 2002 +0100
     1.3 @@ -5,49 +5,56 @@
     1.4  
     1.5  header {* \isaheader{Example for generating executable code from JVM semantics} *}
     1.6  
     1.7 -theory JVMListExample = JVMExec:
     1.8 +theory JVMListExample = SystemClasses + JVMExec:
     1.9  
    1.10  consts
    1.11 -  list_name :: cname
    1.12 -  test_name :: cname
    1.13 +  list_nam :: cnam
    1.14 +  test_nam :: cnam
    1.15    append_name :: mname
    1.16    makelist_name :: mname
    1.17    val_nam :: vnam
    1.18    next_nam :: vnam
    1.19 +  test_name_loc :: loc_
    1.20  
    1.21  constdefs
    1.22 +  list_name :: cname
    1.23 +  "list_name == Cname list_nam"
    1.24 +  
    1.25 +  test_name :: cname
    1.26 +  "test_name == Cname test_nam"
    1.27 +
    1.28    val_name :: vname
    1.29    "val_name == VName val_nam"
    1.30  
    1.31    next_name :: vname
    1.32    "next_name == VName next_nam"
    1.33  
    1.34 -  list_class :: "jvm_method class"
    1.35 -  "list_class ==
    1.36 -    (Object,
    1.37 -     [(val_name, PrimT Integer), (next_name, RefT (ClassT list_name))],
    1.38 -     [((append_name, [RefT (ClassT list_name)]), PrimT Integer,
    1.39 -      (0, 0,
    1.40 +  append_ins :: bytecode
    1.41 +  "append_ins == 
    1.42         [Load 0,
    1.43          Getfield next_name list_name,
    1.44          Dup,
    1.45          LitPush Null,
    1.46          Ifcmpeq 4,
    1.47 -        Load 1,
    1.48 -        Invoke list_name append_name [RefT (ClassT list_name)],
    1.49 +        Load 1,       
    1.50 +        Invoke list_name append_name [Class list_name],
    1.51          Return,
    1.52          Pop,
    1.53          Load 0,
    1.54          Load 1,
    1.55          Putfield next_name list_name,
    1.56          LitPush Unit,
    1.57 -        Return],[]))])"
    1.58 +        Return]"
    1.59  
    1.60 -  test_class :: "jvm_method class"
    1.61 -  "test_class ==
    1.62 -    (Object, [],
    1.63 -     [((makelist_name, []), PrimT Integer,
    1.64 -      (0, 3,
    1.65 +  list_class :: "jvm_method class"
    1.66 +  "list_class ==
    1.67 +    (Object,
    1.68 +     [(val_name, PrimT Integer), (next_name, Class list_name)],
    1.69 +     [((append_name, [Class list_name]), PrimT Void,
    1.70 +        (3, 0, append_ins,[(1,2,8,Xcpt NullPointer)]))])"
    1.71 +
    1.72 +  make_list_ins :: bytecode
    1.73 +  "make_list_ins ==
    1.74         [New list_name,
    1.75          Dup,
    1.76          Store 0,
    1.77 @@ -65,22 +72,33 @@
    1.78          Putfield val_name list_name,
    1.79          Load 0,
    1.80          Load 1,
    1.81 -        Invoke list_name append_name [RefT (ClassT list_name)],
    1.82 +        Invoke list_name append_name [Class list_name],
    1.83          Load 0,
    1.84          Load 2,
    1.85 -        Invoke list_name append_name [RefT (ClassT list_name)],
    1.86 +        Invoke list_name append_name [Class list_name],
    1.87          LitPush Unit,
    1.88 -        Return],[]))])"
    1.89 +        Return]"
    1.90 +
    1.91 +  test_class :: "jvm_method class"
    1.92 +  "test_class ==
    1.93 +    (Object, [],
    1.94 +     [((makelist_name, []), PrimT Void, (3, 2, make_list_ins,[]))])"
    1.95  
    1.96 -  example_prg :: jvm_prog
    1.97 -  "example_prg == [ObjectC, (list_name, list_class), (test_name, test_class)]"
    1.98 +  E :: jvm_prog
    1.99 +  "E == SystemClasses @ [(list_name, list_class), (test_name, test_class)]"
   1.100 +
   1.101 +  start_heap :: aheap
   1.102 +  "start_heap == empty (XcptRef NullPointer \<mapsto> (Xcpt NullPointer, empty))
   1.103 +                       (XcptRef ClassCast \<mapsto> (Xcpt ClassCast, empty))
   1.104 +                       (XcptRef OutOfMemory \<mapsto> (Xcpt OutOfMemory, empty))
   1.105 +                       (Loc test_name_loc \<mapsto> (test_name, empty))"
   1.106  
   1.107    start_state :: jvm_state
   1.108    "start_state ==
   1.109 -    (None, empty, [([], Unit # Unit # Unit # [], test_name, (makelist_name, []), 0)])"
   1.110 +    (None, start_heap, [([], [Addr (Loc test_name_loc), arbitrary, arbitrary], test_name, (makelist_name, []), 0)])"
   1.111  
   1.112  types_code
   1.113 -  cname ("string")
   1.114 +  cnam ("string")
   1.115    vnam ("string")
   1.116    mname ("string")
   1.117    loc_ ("int")
   1.118 @@ -92,11 +110,12 @@
   1.119  
   1.120    "arbitrary" ("(raise ERROR)")
   1.121    "arbitrary" :: "val" ("{* Unit *}")
   1.122 -  "arbitrary" :: "cname" ("\"\"")
   1.123 +  "arbitrary" :: "cname" ("Object")
   1.124  
   1.125 -  "Object" ("\"Object\"")
   1.126 -  "list_name" ("\"list\"")
   1.127 -  "test_name" ("\"test\"")
   1.128 +  "test_name_loc" ("0")
   1.129 +
   1.130 +  "list_nam" ("\"list\"")
   1.131 +  "test_nam" ("\"test\"")
   1.132    "append_name" ("\"append\"")
   1.133    "makelist_name" ("\"makelist\"")
   1.134    "val_nam" ("\"val\"")
   1.135 @@ -110,62 +129,62 @@
   1.136  
   1.137  subsection {* Single step execution *}
   1.138  
   1.139 -generate_code
   1.140 -  test = "exec (example_prg, start_state)"
   1.141 +generate_code 
   1.142 +  test = "exec (E, start_state)"
   1.143  
   1.144  ML {* test *}
   1.145 -ML {* exec (example_prg, the it) *}
   1.146 -ML {* exec (example_prg, the it) *}
   1.147 -ML {* exec (example_prg, the it) *}
   1.148 -ML {* exec (example_prg, the it) *}
   1.149 -ML {* exec (example_prg, the it) *}
   1.150 -ML {* exec (example_prg, the it) *}
   1.151 -ML {* exec (example_prg, the it) *}
   1.152 -ML {* exec (example_prg, the it) *}
   1.153 -ML {* exec (example_prg, the it) *}
   1.154 -ML {* exec (example_prg, the it) *}
   1.155 -ML {* exec (example_prg, the it) *}
   1.156 -ML {* exec (example_prg, the it) *}
   1.157 -ML {* exec (example_prg, the it) *}
   1.158 -ML {* exec (example_prg, the it) *}
   1.159 -ML {* exec (example_prg, the it) *}
   1.160 -ML {* exec (example_prg, the it) *}
   1.161 -ML {* exec (example_prg, the it) *}
   1.162 -ML {* exec (example_prg, the it) *}
   1.163 -ML {* exec (example_prg, the it) *}
   1.164 -ML {* exec (example_prg, the it) *}
   1.165 -ML {* exec (example_prg, the it) *}
   1.166 -ML {* exec (example_prg, the it) *}
   1.167 -ML {* exec (example_prg, the it) *}
   1.168 -ML {* exec (example_prg, the it) *}
   1.169 -ML {* exec (example_prg, the it) *}
   1.170 -ML {* exec (example_prg, the it) *}
   1.171 -ML {* exec (example_prg, the it) *}
   1.172 -ML {* exec (example_prg, the it) *}
   1.173 -ML {* exec (example_prg, the it) *}
   1.174 -ML {* exec (example_prg, the it) *}
   1.175 -ML {* exec (example_prg, the it) *}
   1.176 -ML {* exec (example_prg, the it) *}
   1.177 -ML {* exec (example_prg, the it) *}
   1.178 -ML {* exec (example_prg, the it) *}
   1.179 -ML {* exec (example_prg, the it) *}
   1.180 -ML {* exec (example_prg, the it) *}
   1.181 -ML {* exec (example_prg, the it) *}
   1.182 -ML {* exec (example_prg, the it) *}
   1.183 -ML {* exec (example_prg, the it) *}
   1.184 -ML {* exec (example_prg, the it) *}
   1.185 -ML {* exec (example_prg, the it) *}
   1.186 -ML {* exec (example_prg, the it) *}
   1.187 -ML {* exec (example_prg, the it) *}
   1.188 -ML {* exec (example_prg, the it) *}
   1.189 -ML {* exec (example_prg, the it) *}
   1.190 -ML {* exec (example_prg, the it) *}
   1.191 -ML {* exec (example_prg, the it) *}
   1.192 -ML {* exec (example_prg, the it) *}
   1.193 -ML {* exec (example_prg, the it) *}
   1.194 -ML {* exec (example_prg, the it) *}
   1.195 -ML {* exec (example_prg, the it) *}
   1.196 -ML {* exec (example_prg, the it) *}
   1.197 -ML {* exec (example_prg, the it) *}
   1.198 +ML {* exec (E, the it) *}
   1.199 +ML {* exec (E, the it) *}
   1.200 +ML {* exec (E, the it) *}
   1.201 +ML {* exec (E, the it) *}
   1.202 +ML {* exec (E, the it) *}
   1.203 +ML {* exec (E, the it) *}
   1.204 +ML {* exec (E, the it) *}
   1.205 +ML {* exec (E, the it) *}
   1.206 +ML {* exec (E, the it) *}
   1.207 +ML {* exec (E, the it) *}
   1.208 +ML {* exec (E, the it) *}
   1.209 +ML {* exec (E, the it) *}
   1.210 +ML {* exec (E, the it) *}
   1.211 +ML {* exec (E, the it) *}
   1.212 +ML {* exec (E, the it) *}
   1.213 +ML {* exec (E, the it) *}
   1.214 +ML {* exec (E, the it) *}
   1.215 +ML {* exec (E, the it) *}
   1.216 +ML {* exec (E, the it) *}
   1.217 +ML {* exec (E, the it) *}
   1.218 +ML {* exec (E, the it) *}
   1.219 +ML {* exec (E, the it) *}
   1.220 +ML {* exec (E, the it) *}
   1.221 +ML {* exec (E, the it) *}
   1.222 +ML {* exec (E, the it) *}
   1.223 +ML {* exec (E, the it) *}
   1.224 +ML {* exec (E, the it) *}
   1.225 +ML {* exec (E, the it) *}
   1.226 +ML {* exec (E, the it) *}
   1.227 +ML {* exec (E, the it) *}
   1.228 +ML {* exec (E, the it) *}
   1.229 +ML {* exec (E, the it) *}
   1.230 +ML {* exec (E, the it) *}
   1.231 +ML {* exec (E, the it) *}
   1.232 +ML {* exec (E, the it) *}
   1.233 +ML {* exec (E, the it) *}
   1.234 +ML {* exec (E, the it) *}
   1.235 +ML {* exec (E, the it) *}
   1.236 +ML {* exec (E, the it) *}
   1.237 +ML {* exec (E, the it) *}
   1.238 +ML {* exec (E, the it) *}
   1.239 +ML {* exec (E, the it) *}
   1.240 +ML {* exec (E, the it) *}
   1.241 +ML {* exec (E, the it) *}
   1.242 +ML {* exec (E, the it) *}
   1.243 +ML {* exec (E, the it) *}
   1.244 +ML {* exec (E, the it) *}
   1.245 +ML {* exec (E, the it) *}
   1.246 +ML {* exec (E, the it) *}
   1.247 +ML {* exec (E, the it) *}
   1.248 +ML {* exec (E, the it) *}
   1.249 +ML {* exec (E, the it) *}
   1.250 +ML {* exec (E, the it) *}
   1.251  
   1.252  end
   1.253 \ No newline at end of file