author | schirmer |
Fri, 22 Feb 2002 11:26:44 +0100 | |
changeset 12925 | 99131847fb93 |
parent 12858 | 6214f03d6d27 |
child 13337 | f75dfc606ac7 |
permissions | -rw-r--r-- |
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) *) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
81 |
| FVar qtname qtname bool expr vname |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
82 |
(*class field*)("{_,_,_}_.._"[10,10,10,85,99]90) |
12854 | 83 |
| AVar expr expr (* array component *) ("_.[_]"[90,10 ]90) |
84 |
||
85 |
and expr |
|
86 |
= NewC qtname (* class instance creation *) |
|
87 |
| NewA ty expr (* array creation *) ("New _[_]"[99,10 ]85) |
|
88 |
| Cast ty expr (* type cast *) |
|
89 |
| Inst expr ref_ty (* instanceof *) ("_ InstOf _"[85,99] 85) |
|
90 |
| Lit val (* literal value, references not allowed *) |
|
91 |
| Super (* special Super keyword *) |
|
92 |
| Acc var (* variable access *) |
|
93 |
| Ass var expr (* variable assign *) ("_:=_" [90,85 ]85) |
|
94 |
| Cond expr expr expr (* conditional *) ("_ ? _ : _" [85,85,80]80) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
95 |
| Call qtname ref_ty inv_mode expr mname "(ty list)" (* method call *) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
96 |
"(expr list)" ("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85) |
12854 | 97 |
| Methd qtname sig (* (folded) method (see below) *) |
98 |
| Body qtname stmt (* (unfolded) method body *) |
|
99 |
and stmt |
|
100 |
= Skip (* empty statement *) |
|
101 |
| Expr expr (* expression statement *) |
|
102 |
| Lab label stmt ("_\<bullet> _"(* labeled statement*)[ 99,66]66) |
|
103 |
(* handles break *) |
|
104 |
| Comp stmt stmt ("_;; _" [ 66,65]65) |
|
105 |
| If_ expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70) |
|
106 |
| Loop label expr stmt ("_\<bullet> While'(_') _" [ 99,80,79]70) |
|
107 |
| Do jump (* break, continue, return *) |
|
108 |
| Throw expr |
|
109 |
| TryC stmt |
|
110 |
qtname vname stmt ("Try _ Catch'(_ _') _" [79,99,80,79]70) |
|
111 |
| Fin stmt stmt ("_ Finally _" [ 79,79]70) |
|
112 |
| Init qtname (* class initialization *) |
|
113 |
||
114 |
||
115 |
text {* |
|
116 |
The expressions Methd and Body are artificial program constructs, in the |
|
117 |
sense that they are not used to define a concrete Bali program. In the |
|
118 |
evaluation semantic definition they are "generated on the fly" to decompose |
|
119 |
the task to define the behaviour of the Call expression. They are crucial |
|
120 |
for the axiomatic semantics to give a syntactic hook to insert |
|
121 |
some assertions (cf. AxSem.thy, Eval.thy). |
|
122 |
Also the Init statement (to initialize a class on its first use) is inserted |
|
123 |
in various places by the evaluation semantics. |
|
124 |
*} |
|
125 |
||
126 |
types "term" = "(expr+stmt, var, expr list) sum3" |
|
127 |
translations |
|
128 |
"sig" <= (type) "mname \<times> ty list" |
|
129 |
"var" <= (type) "Term.var" |
|
130 |
"expr" <= (type) "Term.expr" |
|
131 |
"stmt" <= (type) "Term.stmt" |
|
132 |
"term" <= (type) "(expr+stmt, var, expr list) sum3" |
|
133 |
||
134 |
syntax |
|
135 |
||
136 |
this :: expr |
|
137 |
LAcc :: "vname \<Rightarrow> expr" ("!!") |
|
138 |
LAss :: "vname \<Rightarrow> expr \<Rightarrow> stmt" ("_:==_" [90,85] 85) |
|
139 |
Return :: "expr \<Rightarrow> stmt" |
|
140 |
StatRef :: "ref_ty \<Rightarrow> expr" |
|
141 |
||
142 |
translations |
|
143 |
||
144 |
"this" == "Acc (LVar This)" |
|
145 |
"!!v" == "Acc (LVar (EName (VNam v)))" |
|
146 |
"v:==e" == "Expr (Ass (LVar (EName (VNam v))) e)" |
|
147 |
"Return e" == "Expr (Ass (LVar (EName Res)) e);; Do Ret" |
|
148 |
(* Res := e;; Do Ret *) |
|
149 |
"StatRef rt" == "Cast (RefT rt) (Lit Null)" |
|
150 |
||
151 |
constdefs |
|
152 |
||
153 |
is_stmt :: "term \<Rightarrow> bool" |
|
154 |
"is_stmt t \<equiv> \<exists>c. t=In1r c" |
|
155 |
||
156 |
ML {* |
|
157 |
bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def")); |
|
158 |
*} |
|
159 |
||
160 |
declare is_stmt_rews [simp] |
|
161 |
end |