6 |
6 |
7 header "Statements and expression emulations" |
7 header "Statements and expression emulations" |
8 |
8 |
9 theory Term = Main: |
9 theory Term = Main: |
10 |
10 |
11 typedecl cname (* class name *) |
11 typedecl cname --{* class name *} |
12 typedecl vnam (* variable or field name *) |
12 typedecl mname --{* method name *} |
13 typedecl mname (* method name *) |
13 typedecl fname --{* field name *} |
|
14 typedecl vname --{* variable name *} |
14 |
15 |
15 datatype vname (* variable for special names *) |
16 consts |
16 = This (* This pointer *) |
17 This :: vname --{* This pointer *} |
17 | Param (* method parameter *) |
18 Par :: vname --{* method parameter *} |
18 | Res (* method result *) |
19 Res :: vname --{* method result *} |
19 | VName vnam |
20 |
|
21 text {* Inequality axioms not required here *} |
|
22 (* |
|
23 axioms |
|
24 This_neq_Par [simp]: "This \<noteq> Par" |
|
25 Par_neq_Res [simp]: "Par \<noteq> Res" |
|
26 Res_neq_This [simp]: "Res \<noteq> This" |
|
27 *) |
20 |
28 |
21 datatype stmt |
29 datatype stmt |
22 = Skip (* empty statement *) |
30 = Skip --{* empty statement *} |
23 | Comp stmt stmt ("_;; _" [91,90 ] 90) |
31 | Comp stmt stmt ("_;; _" [91,90 ] 90) |
24 | Cond expr stmt stmt ("If '(_') _ Else _" [99,91,91] 91) |
32 | Cond expr stmt stmt ("If '(_') _ Else _" [99,91,91] 91) |
25 | Loop vname stmt ("While '(_') _" [99,91 ] 91) |
33 | Loop vname stmt ("While '(_') _" [99,91 ] 91) |
26 | LAss vname expr ("_ :== _" [99, 95] 94) (* local ass. *) |
34 | LAss vname expr ("_ :== _" [99, 95] 94) --{* local ass.*} |
27 | FAss expr vnam expr ("_.._:==_" [95,99,95] 94) (* field ass. *) |
35 | FAss expr fname expr ("_.._:==_" [95,99,95] 94) --{* field ass.*} |
28 | Meth "cname \<times> mname" (* virtual method *) |
36 | Meth "cname \<times> mname" --{* virtual method *} |
29 | Impl "cname \<times> mname" (* method implementation *) |
37 | Impl "cname \<times> mname" --{* method implementation *} |
30 and expr |
38 and expr |
31 = NewC cname ("new _" [ 99] 95) (* object creation *) |
39 = NewC cname ("new _" [ 99] 95) --{* object creation *} |
32 | Cast cname expr (* type cast *) |
40 | Cast cname expr --{* type cast *} |
33 | LAcc vname (* local access *) |
41 | LAcc vname --{* local access *} |
34 | FAcc expr vnam ("_.._" [95,99] 95) (* field access *) |
42 | FAcc expr fname ("_.._" [95,99] 95) --{* field access *} |
35 | Call cname expr mname expr (* method call *) |
43 | Call cname expr mname expr |
36 ("{_}_.._'(_')" [99,95,99,95] 95) |
44 ("{_}_.._'(_')" [99,95,99,95] 95) --{* method call *} |
37 |
45 |
38 end |
46 end |
39 |
47 |