author | schirmer |
Thu, 11 Jul 2002 09:36:41 +0200 | |
changeset 13345 | bd611943cbc2 |
parent 13337 | f75dfc606ac7 |
child 13358 | c837ba4cfb62 |
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 |
||
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
9 |
theory Term = Value + Table: |
12854 | 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 |
||
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
61 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
62 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
63 |
types locals = "(lname, val) table" (* local variables *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
64 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
65 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
66 |
datatype jump |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
67 |
= Break label (* break *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
68 |
| Cont label (* continue *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
69 |
| Ret (* return from method *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
70 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
71 |
datatype xcpt (* exception *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
72 |
= Loc loc (* location of allocated execption object *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
73 |
| Std xname (* intermediate standard exception, see Eval.thy *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
74 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
75 |
datatype error |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
76 |
= AccessViolation (* Access to a member that isn't permitted *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
77 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
78 |
datatype abrupt (* abrupt completion *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
79 |
= Xcpt xcpt (* exception *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
80 |
| Jump jump (* break, continue, return *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
81 |
| Error error (* runtime errors, we wan't to detect and proof absent |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
82 |
in welltyped programms *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
83 |
types |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
84 |
abopt = "abrupt option" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
85 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
86 |
text {* Local variable store and exception. |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
87 |
Anticipation of State.thy used by smallstep semantics. For a method call, |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
88 |
we save the local variables of the caller in the term Callee to restore them |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
89 |
after method return. Also an exception must be restored after the finally |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
90 |
statement *} |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
91 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
92 |
translations |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
93 |
"locals" <= (type) "(lname, val) table" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
94 |
|
12854 | 95 |
datatype inv_mode (* invocation mode for method calls *) |
96 |
= Static (* static *) |
|
97 |
| SuperM (* super *) |
|
98 |
| IntVir (* interface or virtual *) |
|
99 |
||
100 |
record sig = (* signature of a method, cf. 8.4.2 *) |
|
101 |
name ::"mname" (* acutally belongs to Decl.thy *) |
|
102 |
parTs::"ty list" |
|
103 |
||
104 |
translations |
|
105 |
"sig" <= (type) "\<lparr>name::mname,parTs::ty list\<rparr>" |
|
106 |
"sig" <= (type) "\<lparr>name::mname,parTs::ty list,\<dots>::'a\<rparr>" |
|
107 |
||
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
108 |
-- "function codes for unary operations" |
13345 | 109 |
datatype unop = UPlus -- {*{\tt +} unary plus*} |
110 |
| UMinus -- {*{\tt -} unary minus*} |
|
111 |
| UBitNot -- {*{\tt ~} bitwise NOT*} |
|
112 |
| UNot -- {*{\tt !} logical complement*} |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
113 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
114 |
-- "function codes for binary operations" |
13345 | 115 |
datatype binop = Mul -- {*{\tt * } multiplication*} |
116 |
| Div -- {*{\tt /} division*} |
|
117 |
| Mod -- {*{\tt %} remainder*} |
|
118 |
| Plus -- {*{\tt +} addition*} |
|
119 |
| Minus -- {*{\tt -} subtraction*} |
|
120 |
| LShift -- {*{\tt <<} left shift*} |
|
121 |
| RShift -- {*{\tt >>} signed right shift*} |
|
122 |
| RShiftU -- {*{\tt >>>} unsigned right shift*} |
|
123 |
| Less -- {*{\tt <} less than*} |
|
124 |
| Le -- {*{\tt <=} less than or equal*} |
|
125 |
| Greater -- {*{\tt >} greater than*} |
|
126 |
| Ge -- {*{\tt >=} greater than or equal*} |
|
127 |
| Eq -- {*{\tt ==} equal*} |
|
128 |
| Neq -- {*{\tt !=} not equal*} |
|
129 |
| BitAnd -- {*{\tt &} bitwise AND*} |
|
130 |
| And -- {*{\tt &} boolean AND*} |
|
131 |
| BitXor -- {*{\tt ^} bitwise Xor*} |
|
132 |
| Xor -- {*{\tt ^} boolean Xor*} |
|
133 |
| BitOr -- {*{\tt |} bitwise Or*} |
|
134 |
| Or -- {*{\tt |} boolean Or*} |
|
135 |
text{* The boolean operators {\tt &} and {\tt |} strictly evaluate both |
|
136 |
of their arguments. The lazy operators {\tt &&} and {\tt ||} are modeled |
|
137 |
as instances of the @{text Cond} expression: {\tt a && b = a?b:false} and |
|
138 |
{\tt a || b = a?true:b} |
|
139 |
*} |
|
12854 | 140 |
datatype var |
141 |
= 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
|
142 |
| 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
|
143 |
(*class field*)("{_,_,_}_.._"[10,10,10,85,99]90) |
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
144 |
| AVar expr expr (* array component *) ("_.[_]"[90,10 ]90) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
145 |
| InsInitV stmt var (* insertion of initialization before |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
146 |
evaluation of var (for smallstep sem.) *) |
12854 | 147 |
|
148 |
and expr |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
149 |
= NewC qtname (* class instance creation *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
150 |
| NewA ty expr (* array creation *) ("New _[_]"[99,10 ]85) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
151 |
| Cast ty expr (* type cast *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
152 |
| Inst expr ref_ty (* instanceof *) ("_ InstOf _"[85,99] 85) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
153 |
| Lit val (* literal value, references not allowed *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
154 |
| UnOp unop expr (* unary operation *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
155 |
| BinOp binop expr expr (* binary operation *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
156 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
157 |
| Super (* special Super keyword *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
158 |
| Acc var (* variable access *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
159 |
| Ass var expr (* variable assign *) ("_:=_" [90,85 ]85) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
160 |
| Cond expr expr expr (* conditional *) ("_ ? _ : _" [85,85,80]80) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
161 |
| Call qtname ref_ty inv_mode expr mname "(ty list)" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
162 |
"(expr list)" (* method call *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
163 |
("{_,_,_}_\<cdot>_'( {_}_')"[10,10,10,85,99,10,10]85) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
164 |
| Methd qtname sig (* (folded) method (see below) *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
165 |
| Body qtname stmt (* (unfolded) method body *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
166 |
| InsInitE stmt expr (* insertion of initialization before |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
167 |
evaluation of expr (for smallstep sem.) *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
168 |
| Callee locals expr (* save Callers locals in Callee-Frame |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
169 |
(for smallstep semantics) *) |
12854 | 170 |
and stmt |
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
171 |
= Skip (* empty statement *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
172 |
| Expr expr (* expression statement *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
173 |
| Lab jump stmt ("_\<bullet> _"(* labeled statement*)[ 99,66]66) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
174 |
(* handles break *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
175 |
| Comp stmt stmt ("_;; _" [ 66,65]65) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
176 |
| If_ expr stmt stmt ("If'(_') _ Else _" [ 80,79,79]70) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
177 |
| Loop label expr stmt ("_\<bullet> While'(_') _" [ 99,80,79]70) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
178 |
| Do jump (* break, continue, return *) |
12854 | 179 |
| Throw expr |
180 |
| TryC stmt |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
181 |
qtname vname stmt ("Try _ Catch'(_ _') _" [79,99,80,79]70) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
182 |
| Fin stmt stmt ("_ Finally _" [ 79,79]70) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
183 |
| FinA abopt stmt (* Save abruption of first statement |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
184 |
(for smallstep sem.) *) |
12854 | 185 |
| Init qtname (* class initialization *) |
186 |
||
187 |
||
188 |
text {* |
|
189 |
The expressions Methd and Body are artificial program constructs, in the |
|
190 |
sense that they are not used to define a concrete Bali program. In the |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
191 |
operational semantic's they are "generated on the fly" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
192 |
to decompose the task to define the behaviour of the Call expression. |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
193 |
They are crucial for the axiomatic semantics to give a syntactic hook to insert |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
194 |
some assertions (cf. AxSem.thy, Eval.thy). |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
195 |
The Init statement (to initialize a class on its first use) is |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
196 |
inserted in various places by the semantics. |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
197 |
Callee, InsInitV, InsInitE,FinA are only needed as intermediate steps in the |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
198 |
smallstep (transition) semantics (cf. Trans.thy). Callee is used to save the |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
199 |
local variables of the caller for method return. So ve avoid modelling a |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
200 |
frame stack. |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
201 |
The InsInitV/E terms are only used by the smallstep semantics to model the |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
202 |
intermediate steps of class-initialisation. |
12854 | 203 |
*} |
204 |
||
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
205 |
types "term" = "(expr+stmt,var,expr list) sum3" |
12854 | 206 |
translations |
207 |
"sig" <= (type) "mname \<times> ty list" |
|
208 |
"var" <= (type) "Term.var" |
|
209 |
"expr" <= (type) "Term.expr" |
|
210 |
"stmt" <= (type) "Term.stmt" |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
211 |
"term" <= (type) "(expr+stmt,var,expr list) sum3" |
12854 | 212 |
|
213 |
syntax |
|
214 |
||
215 |
this :: expr |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
216 |
LAcc :: "vname \<Rightarrow> expr" ("!!") |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
217 |
LAss :: "vname \<Rightarrow> expr \<Rightarrow>stmt" ("_:==_" [90,85] 85) |
12854 | 218 |
Return :: "expr \<Rightarrow> stmt" |
219 |
StatRef :: "ref_ty \<Rightarrow> expr" |
|
220 |
||
221 |
translations |
|
222 |
||
223 |
"this" == "Acc (LVar This)" |
|
224 |
"!!v" == "Acc (LVar (EName (VNam v)))" |
|
225 |
"v:==e" == "Expr (Ass (LVar (EName (VNam v))) e)" |
|
226 |
"Return e" == "Expr (Ass (LVar (EName Res)) e);; Do Ret" |
|
227 |
(* Res := e;; Do Ret *) |
|
228 |
"StatRef rt" == "Cast (RefT rt) (Lit Null)" |
|
229 |
||
230 |
constdefs |
|
231 |
||
232 |
is_stmt :: "term \<Rightarrow> bool" |
|
233 |
"is_stmt t \<equiv> \<exists>c. t=In1r c" |
|
234 |
||
235 |
ML {* |
|
236 |
bind_thms ("is_stmt_rews", sum3_instantiate (thm "is_stmt_def")); |
|
237 |
*} |
|
238 |
||
239 |
declare is_stmt_rews [simp] |
|
13345 | 240 |
|
241 |
axclass inj_term < "type" |
|
242 |
consts inj_term:: "'a::inj_term \<Rightarrow> term" ("\<langle>_\<rangle>" 83) |
|
243 |
||
244 |
instance stmt::inj_term .. |
|
245 |
||
246 |
defs (overloaded) |
|
247 |
stmt_inj_term_def: "\<langle>c::stmt\<rangle> \<equiv> In1r c" |
|
248 |
||
249 |
lemma stmt_inj_term_simp: "\<langle>c::stmt\<rangle> = In1r c" |
|
250 |
by (simp add: stmt_inj_term_def) |
|
251 |
||
252 |
instance expr::inj_term .. |
|
253 |
||
254 |
defs (overloaded) |
|
255 |
expr_inj_term_def: "\<langle>e::expr\<rangle> \<equiv> In1l e" |
|
256 |
||
257 |
lemma expr_inj_term_simp: "\<langle>e::expr\<rangle> = In1l e" |
|
258 |
by (simp add: expr_inj_term_def) |
|
259 |
||
260 |
instance var::inj_term .. |
|
261 |
||
262 |
defs (overloaded) |
|
263 |
var_inj_term_def: "\<langle>v::var\<rangle> \<equiv> In2 v" |
|
264 |
||
265 |
lemma var_inj_term_simp: "\<langle>v::var\<rangle> = In2 v" |
|
266 |
by (simp add: var_inj_term_def) |
|
267 |
||
268 |
instance "list":: (type) inj_term .. |
|
269 |
||
270 |
defs (overloaded) |
|
271 |
expr_list_inj_term_def: "\<langle>es::expr list\<rangle> \<equiv> In3 es" |
|
272 |
||
273 |
lemma expr_list_inj_term_simp: "\<langle>es::expr list\<rangle> = In3 es" |
|
274 |
by (simp add: expr_list_inj_term_def) |
|
275 |
||
12854 | 276 |
end |