12857
|
1 |
(* Title: HOL/Bali/Term.thy
|
12854
|
2 |
ID: $Id$
|
|
3 |
Author: David von Oheimb
|
12858
|
4 |
License: GPL (GNU GENERAL PUBLIC LICENSE)
|
12854
|
5 |
*)
|
|
6 |
|
|
7 |
header {* Java expressions and statements *}
|
|
8 |
|
|
9 |
theory Term = Value:
|
|
10 |
|
|
11 |
text {*
|
|
12 |
design issues:
|
|
13 |
\begin{itemize}
|
|
14 |
\item invocation frames for local variables could be reduced to special static
|
|
15 |
objects (one per method). This would reduce redundancy, but yield a rather
|
|
16 |
non-standard execution model more difficult to understand.
|
|
17 |
\item method bodies separated from calls to handle assumptions in axiomat.
|
|
18 |
semantics
|
|
19 |
NB: Body is intended to be in the environment of the called method.
|
|
20 |
\item class initialization is regarded as (auxiliary) statement
|
|
21 |
(required for AxSem)
|
|
22 |
\item result expression of method return is handled by a special result variable
|
|
23 |
result variable is treated uniformly with local variables
|
|
24 |
\begin{itemize}
|
|
25 |
\item[+] welltypedness and existence of the result/return expression is
|
|
26 |
ensured without extra efford
|
|
27 |
\end{itemize}
|
|
28 |
\end{itemize}
|
|
29 |
|
|
30 |
simplifications:
|
|
31 |
\begin{itemize}
|
|
32 |
\item expression statement allowed for any expression
|
|
33 |
\item no unary, binary, etc, operators
|
|
34 |
\item This is modeled as a special non-assignable local variable
|
|
35 |
\item Super is modeled as a general expression with the same value as This
|
|
36 |
\item access to field x in current class via This.x
|
|
37 |
\item NewA creates only one-dimensional arrays;
|
|
38 |
initialization of further subarrays may be simulated with nested NewAs
|
|
39 |
\item The 'Lit' constructor is allowed to contain a reference value.
|
|
40 |
But this is assumed to be prohibited in the input language, which is enforced
|
|
41 |
by the type-checking rules.
|
|
42 |
\item a call of a static method via a type name may be simulated by a dummy
|
|
43 |
variable
|
|
44 |
\item no nested blocks with inner local variables
|
|
45 |
\item no synchronized statements
|
|
46 |
\item no secondary forms of if, while (e.g. no for) (may be easily simulated)
|
|
47 |
\item no switch (may be simulated with if)
|
|
48 |
\item the @{text try_catch_finally} statement is divided into the
|
|
49 |
@{text try_catch} statement
|
|
50 |
and a finally statement, which may be considered as try..finally with
|
|
51 |
empty catch
|
|
52 |
\item the @{text try_catch} statement has exactly one catch clause;
|
|
53 |
multiple ones can be
|
|
54 |
simulated with instanceof
|
|
55 |
\item the compiler is supposed to add the annotations {@{text _}} during
|
|
56 |
type-checking. This
|
|
57 |
transformation is left out as its result is checked by the type rules anyway
|
|
58 |
\end{itemize}
|
|
59 |
*}
|
|
60 |
|
|
61 |
datatype inv_mode (* invocation mode for method calls *)
|
|
62 |
= Static (* static *)
|
|
63 |
| SuperM (* super *)
|
|
64 |
| IntVir (* interface or virtual *)
|
|
65 |
|
|
66 |
record sig = (* signature of a method, cf. 8.4.2 *)
|
|
67 |
name ::"mname" (* acutally belongs to Decl.thy *)
|
|
68 |
parTs::"ty list"
|
|
69 |
|
|
70 |
translations
|
|
71 |
"sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>"
|
|
72 |
"sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>"
|
|
73 |
|
|
74 |
datatype jump
|
|
75 |
= Break label (* break *)
|
|
76 |
| Cont label (* continue *)
|
|
77 |
| Ret (* return from method *)
|
|
78 |
|
|
79 |
datatype var
|
|
80 |
= LVar lname(* local variable (incl. parameters) *)
|
|
81 |
| FVar qtname bool expr vname(*class field*)("{_,_}_.._"[10,10,85,99]90)
|
|
82 |
| AVar expr expr (* array component *) ("_.[_]"[90,10 ]90)
|
|
83 |
|
|
84 |
and expr
|
|
85 |
= NewC qtname (* class instance creation *)
|
|
86 |
| NewA ty expr (* array creation *) ("New _[_]"[99,10 ]85)
|
|
87 |
| Cast ty expr (* type cast *)
|
|
88 |
| Inst expr ref_ty (* instanceof *) ("_ InstOf _"[85,99] 85)
|
|
89 |
| Lit val (* literal value, references not allowed *)
|
|
90 |
| Super (* special Super keyword *)
|
|
91 |
| Acc var (* variable access *)
|
|
92 |
| Ass var expr (* variable assign *) ("_:=_" [90,85 ]85)
|
|
93 |
| Cond expr expr expr (* conditional *) ("_ ? _ : _" [85,85,80]80)
|
|
94 |
| Call ref_ty inv_mode expr mname "(ty list)" (* method call *)
|
|
95 |
"(expr list)" ("{_,_}_\<cdot>_'( {_}_')"[10,10,85,99,10,10]85)
|
|
96 |
| Methd qtname sig (* (folded) method (see below) *)
|
|
97 |
| Body qtname stmt (* (unfolded) method body *)
|
|
98 |
and stmt
|
|
99 |
= Skip (* empty statement *)
|
|
100 |
| Expr expr (* expression statement *)
|
|
101 |
| Lab label stmt ("_\<bullet> _"(* labeled statement*)[ 99,66]66)
|
|
102 |
(* handles break *)
|
|
103 |
| Comp stmt stmt ("_;; _" [ 66,65]65)
|
|
104 |
| If_ expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70)
|
|
105 |
| Loop label expr stmt ("_\<bullet> While'(_') _" [ 99,80,79]70)
|
|
106 |
| Do jump (* break, continue, return *)
|
|
107 |
| Throw expr
|
|
108 |
| TryC stmt
|
|
109 |
qtname vname stmt ("Try _ Catch'(_ _') _" [79,99,80,79]70)
|
|
110 |
| Fin stmt stmt ("_ Finally _" [ 79,79]70)
|
|
111 |
| Init qtname (* class initialization *)
|
|
112 |
|
|
113 |
|
|
114 |
text {*
|
|
115 |
The expressions Methd and Body are artificial program constructs, in the
|
|
116 |
sense that they are not used to define a concrete Bali program. In the
|
|
117 |
evaluation semantic definition they are "generated on the fly" to decompose
|
|
118 |
the task to define the behaviour of the Call expression. They are crucial
|
|
119 |
for the axiomatic semantics to give a syntactic hook to insert
|
|
120 |
some assertions (cf. AxSem.thy, Eval.thy).
|
|
121 |
Also the Init statement (to initialize a class on its first use) is inserted
|
|
122 |
in various places by the evaluation semantics.
|
|
123 |
*}
|
|
124 |
|
|
125 |
types "term" = "(expr+stmt, var, expr list) sum3"
|
|
126 |
translations
|
|
127 |
"sig" <= (type) "mname \<times> ty list"
|
|
128 |
"var" <= (type) "Term.var"
|
|
129 |
"expr" <= (type) "Term.expr"
|
|
130 |
"stmt" <= (type) "Term.stmt"
|
|
131 |
"term" <= (type) "(expr+stmt, var, expr list) sum3"
|
|
132 |
|
|
133 |
syntax
|
|
134 |
|
|
135 |
this :: expr
|
|
136 |
LAcc :: "vname \<Rightarrow> expr" ("!!")
|
|
137 |
LAss :: "vname \<Rightarrow> expr \<Rightarrow> stmt" ("_:==_" [90,85] 85)
|
|
138 |
Return :: "expr \<Rightarrow> stmt"
|
|
139 |
StatRef :: "ref_ty \<Rightarrow> expr"
|
|
140 |
|
|
141 |
translations
|
|
142 |
|
|
143 |
"this" == "Acc (LVar This)"
|
|
144 |
"!!v" == "Acc (LVar (EName (VNam v)))"
|
|
145 |
"v:==e" == "Expr (Ass (LVar (EName (VNam v))) e)"
|
|
146 |
"Return e" == "Expr (Ass (LVar (EName Res)) e);; Do Ret"
|
|
147 |
(* Res := e;; Do Ret *)
|
|
148 |
"StatRef rt" == "Cast (RefT rt) (Lit Null)"
|
|
149 |
|
|
150 |
constdefs
|
|
151 |
|
|
152 |
is_stmt :: "term \<Rightarrow> bool"
|
|
153 |
"is_stmt t \<equiv> \<exists>c. t=In1r c"
|
|
154 |
|
|
155 |
ML {*
|
|
156 |
bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def"));
|
|
157 |
*}
|
|
158 |
|
|
159 |
declare is_stmt_rews [simp]
|
|
160 |
|
|
161 |
|
|
162 |
(* ############# Just testing syntax *)
|
|
163 |
(** unfortunately cannot simply instantiate tnam **)
|
|
164 |
(*
|
|
165 |
datatype tnam_ = HasFoo_ | Base_ | Ext_
|
|
166 |
datatype vnam_ = arr_ | vee_ | z_ | e_
|
|
167 |
datatype label_ = lab1_
|
|
168 |
|
|
169 |
consts
|
|
170 |
|
|
171 |
tnam_ :: "tnam_ \<Rightarrow> tnam"
|
|
172 |
vnam_ :: "vnam_ \<Rightarrow> vname"
|
|
173 |
label_:: "label_ \<Rightarrow> label"
|
|
174 |
axioms
|
|
175 |
|
|
176 |
inj_tnam_ [simp]: "(tnam_ x = tnam_ y) = (x = y)"
|
|
177 |
inj_vnam_ [simp]: "(vnam_ x = vnam_ y) = (x = y)"
|
|
178 |
inj_label_ [simp]: "(label_ x = label_ y) = (x = y)"
|
|
179 |
|
|
180 |
|
|
181 |
surj_tnam_: "\<exists>m. n = tnam_ m"
|
|
182 |
surj_vnam_: "\<exists>m. n = vnam_ m"
|
|
183 |
surj_label_:" \<exists>m. n = label_ m"
|
|
184 |
|
|
185 |
syntax
|
|
186 |
|
|
187 |
HasFoo :: qtname
|
|
188 |
Base :: qtname
|
|
189 |
Ext :: qtname
|
|
190 |
arr :: ename
|
|
191 |
vee :: ename
|
|
192 |
z :: ename
|
|
193 |
e :: ename
|
|
194 |
lab1:: label
|
|
195 |
|
|
196 |
consts
|
|
197 |
|
|
198 |
foo :: mname
|
|
199 |
translations
|
|
200 |
|
|
201 |
"HasFoo" == "\<lparr>pid=java_lang,tid=TName (tnam_ HasFoo_)\<rparr>"
|
|
202 |
"Base" == "\<lparr>pid=java_lang,tid=TName (tnam_ Base_)\<rparr>"
|
|
203 |
"Ext" == "\<lparr>pid=java_lang,tid=TName (tnam_ Ext_)\<rparr>"
|
|
204 |
"arr" == "(vnam_ arr_)"
|
|
205 |
"vee" == "(vnam_ vee_)"
|
|
206 |
"z" == "(vnam_ z_)"
|
|
207 |
"e" == "(vnam_ e_)"
|
|
208 |
"lab1" == "label_ lab1_"
|
|
209 |
|
|
210 |
constdefs test::stmt
|
|
211 |
"test \<equiv>
|
|
212 |
(lab1@ While(Acc
|
|
213 |
(Acc ({Base,True}StatRef (ClassT Object).arr).[Lit (Intg #2)])) Skip)"
|
|
214 |
|
|
215 |
consts
|
|
216 |
pTs :: "ty list"
|
|
217 |
|
|
218 |
constdefs
|
|
219 |
|
|
220 |
test1::stmt
|
|
221 |
"test1 \<equiv>
|
|
222 |
Expr({ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null]))"
|
|
223 |
|
|
224 |
|
|
225 |
|
|
226 |
constdefs test::stmt
|
|
227 |
"test \<equiv>
|
|
228 |
(lab1\<cdot> While(Acc
|
|
229 |
(Acc ({Base,True}StatRef (ClassT Object)..arr).[Lit (Intg #2)])) Skip)"
|
|
230 |
*)
|
|
231 |
end |