4 Copyright 1999 Technische Universitaet Muenchen |
4 Copyright 1999 Technische Universitaet Muenchen |
5 |
5 |
6 Java expressions and statements |
6 Java expressions and statements |
7 *) |
7 *) |
8 |
8 |
9 Term = Type + |
9 Term = Value + |
10 |
|
11 types loc (* locations, i.e. abstract references on objects *) |
|
12 arities loc :: term |
|
13 |
|
14 datatype val_ (* name non 'val' because of clash with ML token *) |
|
15 = Unit (* dummy result value of void methods *) |
|
16 | Null (* null reference *) |
|
17 | Bool bool (* Boolean value *) |
|
18 | Intg int (* integer value *) (* Name Intg instead of Int because |
|
19 of clash with HOL/Set.thy *) |
|
20 | Addr loc (* addresses, i.e. locations of objects *) |
|
21 types val = val_ |
|
22 translations "val" <= (type) "val_" |
|
23 |
10 |
24 datatype binop = Eq | Add (* function codes for binary operation *) |
11 datatype binop = Eq | Add (* function codes for binary operation *) |
25 |
12 |
26 datatype expr |
13 datatype expr |
27 = NewC cname (* class instance creation *) |
14 = NewC cname (* class instance creation *) |
28 | Cast ty expr (* type cast *) |
15 | Cast ref_ty expr (* type cast *) |
29 | Lit val (* literal value, also references *) |
16 | Lit val (* literal value, also references *) |
30 | BinOp binop expr expr (* binary operation *) |
17 | BinOp binop expr expr (* binary operation *) |
31 | LAcc vname (* local (incl. parameter) access *) |
18 | LAcc vname (* local (incl. parameter) access *) |
32 | LAss vname expr (* local assign *) ("_\\<Colon>=_" [ 90,90]90) |
19 | LAss vname expr (* local assign *) ("_\\<Colon>=_" [ 90,90]90) |
33 | FAcc cname expr vname (* field access *) ("{_}_.._"[10,90,99 ]90) |
20 | FAcc cname expr vname (* field access *) ("{_}_.._"[10,90,99 ]90) |
34 | FAss cname expr vname |
21 | FAss cname expr vname |
35 expr (* field ass. *)("{_}_.._\\<in>=_"[10,90,99,90]90) |
22 expr (* field ass. *)("{_}_.._:=_"[10,90,99,90]90) |
36 | Call expr mname (ty list) (expr list)(* method call*) |
23 | Call expr mname (ty list) (expr list)(* method call*) |
37 ("_.._'({_}_')" [90,99,10,10] 90) |
24 ("_.._'({_}_')" [90,99,10,10] 90) |
38 and stmt |
25 and stmt |
39 = Skip (* empty statement *) |
26 = Skip (* empty statement *) |
40 | Expr expr (* expression statement *) |
27 | Expr expr (* expression statement *) |