| author | kleing |
| Mon, 07 Aug 2000 14:34:03 +0200 | |
| changeset 9550 | 19a6d1289f5e |
| parent 9376 | c32c5696ec2a |
| child 10057 | 8c8d2d0d3ef8 |
| permissions | -rw-r--r-- |
| 9376 | 1 |
(* Title: HOL/MicroJava/JVM/JVMInstructions.thy |
2 |
ID: $Id$ |
|
3 |
Author: Gerwin Klein |
|
4 |
Copyright 2000 Technische Universitaet Muenchen |
|
5 |
||
6 |
Instructions of the JVM |
|
7 |
*) |
|
8 |
||
9 |
JVMInstructions = JVMState + |
|
10 |
||
|
9550
19a6d1289f5e
Invoke instruction gets fully qualified method name (class+name+sig) as
kleing
parents:
9376
diff
changeset
|
11 |
|
| 9376 | 12 |
datatype |
13 |
instr = Load nat (* load from local variable *) |
|
14 |
| Store nat (* store into local variable *) |
|
15 |
| Bipush int (* push int *) |
|
16 |
| Aconst_null (* push null *) |
|
17 |
| New cname (* create object *) |
|
18 |
| Getfield vname cname (* Fetch field from object *) |
|
19 |
| Putfield vname cname (* Set field in object *) |
|
20 |
| Checkcast cname (* Check whether object is of given type *) |
|
|
9550
19a6d1289f5e
Invoke instruction gets fully qualified method name (class+name+sig) as
kleing
parents:
9376
diff
changeset
|
21 |
| Invoke cname mname "(ty list)" (* inv. instance meth of an object *) |
| 9376 | 22 |
| Return |
23 |
| Pop |
|
24 |
| Dup |
|
25 |
| Dup_x1 |
|
26 |
| Dup_x2 |
|
27 |
| Swap |
|
28 |
| IAdd |
|
29 |
| Goto int |
|
30 |
| Ifcmpeq int (* Branch if int/ref comparison succeeds *) |
|
31 |
||
32 |
||
33 |
types |
|
34 |
bytecode = "instr list" |
|
35 |
jvm_prog = "(nat \\<times> bytecode) prog" |
|
36 |
||
37 |
end |