equal
deleted
inserted
replaced
|
1 (* Title: HOL/MicroJava/JVM/JVMState.thy |
|
2 ID: $Id$ |
|
3 Author: Cornelia Pusch |
|
4 Copyright 1999 Technische Universitaet Muenchen |
|
5 |
|
6 State of the JVM |
|
7 *) |
|
8 |
|
9 JVMState = Store + |
|
10 |
|
11 |
|
12 (** frame stack **) |
|
13 |
|
14 types |
|
15 opstack = "val list" |
|
16 locvars = "val list" |
|
17 p_count = nat |
|
18 |
|
19 frame = "opstack \\<times> |
|
20 locvars \\<times> |
|
21 cname \\<times> |
|
22 sig \\<times> |
|
23 p_count" |
|
24 |
|
25 (* operand stack *) |
|
26 (* local variables *) |
|
27 (* name of def. class defined *) |
|
28 (* meth name+param_desc *) |
|
29 (* program counter within frame *) |
|
30 |
|
31 |
|
32 (** exceptions **) |
|
33 |
|
34 constdefs |
|
35 raise_xcpt :: "bool \\<Rightarrow> xcpt \\<Rightarrow> xcpt option" |
|
36 "raise_xcpt c x \\<equiv> (if c then Some x else None)" |
|
37 |
|
38 heap_update :: "[xcpt option,aheap,aheap] \\<Rightarrow> aheap" |
|
39 "heap_update xp hp' hp \\<equiv> if xp=None then hp' else hp" |
|
40 |
|
41 stk_update :: "[xcpt option,opstack,opstack] \\<Rightarrow> opstack" |
|
42 "stk_update xp stk' stk \\<equiv> if xp=None then stk' else stk" |
|
43 |
|
44 xcpt_update :: "[xcpt option,'a,'a] \\<Rightarrow> 'a" |
|
45 "xcpt_update xp y' y \\<equiv> if xp=None then y' else y" |
|
46 |
|
47 (** runtime state **) |
|
48 |
|
49 types |
|
50 jvm_state = "xcpt option \\<times> |
|
51 aheap \\<times> |
|
52 frame list" |
|
53 |
|
54 |
|
55 |
|
56 (** dynamic method lookup **) |
|
57 |
|
58 constdefs |
|
59 dyn_class :: "'code prog \\<times> sig \\<times> cname \\<Rightarrow> cname" |
|
60 "dyn_class \\<equiv> \\<lambda>(G,sig,C). fst(the(cmethd(G,C) sig))" |
|
61 end |