equal
deleted
inserted
replaced
30 |
30 |
31 |
31 |
32 (** exceptions **) |
32 (** exceptions **) |
33 |
33 |
34 constdefs |
34 constdefs |
35 raise_xcpt :: "bool \\<Rightarrow> xcpt \\<Rightarrow> xcpt option" |
35 raise_xcpt :: "bool => xcpt => xcpt option" |
36 "raise_xcpt c x \\<equiv> (if c then Some x else None)" |
36 "raise_xcpt c x == (if c then Some x else None)" |
37 |
37 |
38 (** runtime state **) |
38 (** runtime state **) |
39 |
39 |
40 types |
40 types |
41 jvm_state = "xcpt option \\<times> aheap \\<times> frame list" |
41 jvm_state = "xcpt option \\<times> aheap \\<times> frame list" |
43 |
43 |
44 |
44 |
45 (** dynamic method lookup **) |
45 (** dynamic method lookup **) |
46 |
46 |
47 constdefs |
47 constdefs |
48 dyn_class :: "'code prog \\<times> sig \\<times> cname \\<Rightarrow> cname" |
48 dyn_class :: "'code prog \\<times> sig \\<times> cname => cname" |
49 "dyn_class \\<equiv> \\<lambda>(G,sig,C). fst(the(method(G,C) sig))" |
49 "dyn_class == \\<lambda>(G,sig,C). fst(the(method(G,C) sig))" |
50 end |
50 end |