10 typedecl pname --{* package name *} |
10 typedecl pname --{* package name *} |
11 typedecl mname --{* method name *} |
11 typedecl mname --{* method name *} |
12 typedecl vname --{* variable or field name *} |
12 typedecl vname --{* variable or field name *} |
13 typedecl label --{* label as destination of break or continue *} |
13 typedecl label --{* label as destination of break or continue *} |
14 |
14 |
15 datatype ename --{* expression name *} |
15 datatype_new ename --{* expression name *} |
16 = VNam vname |
16 = VNam vname |
17 | Res --{* special name to model the return value of methods *} |
17 | Res --{* special name to model the return value of methods *} |
18 |
18 |
19 datatype lname --{* names for local variables and the This pointer *} |
19 datatype_new lname --{* names for local variables and the This pointer *} |
20 = EName ename |
20 = EName ename |
21 | This |
21 | This |
22 abbreviation VName :: "vname \<Rightarrow> lname" |
22 abbreviation VName :: "vname \<Rightarrow> lname" |
23 where "VName n == EName (VNam n)" |
23 where "VName n == EName (VNam n)" |
24 |
24 |
25 abbreviation Result :: lname |
25 abbreviation Result :: lname |
26 where "Result == EName Res" |
26 where "Result == EName Res" |
27 |
27 |
28 datatype xname --{* names of standard exceptions *} |
28 datatype_new xname --{* names of standard exceptions *} |
29 = Throwable |
29 = Throwable |
30 | NullPointer | OutOfMemory | ClassCast |
30 | NullPointer | OutOfMemory | ClassCast |
31 | NegArrSize | IndOutBound | ArrStore |
31 | NegArrSize | IndOutBound | ArrStore |
32 |
32 |
33 lemma xn_cases: |
33 lemma xn_cases: |