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