author | wenzelm |
Tue, 27 Aug 2002 11:03:05 +0200 | |
changeset 13524 | 604d0f3622d6 |
parent 13462 | 56610e2ba220 |
child 13688 | a0b16d42d489 |
permissions | -rw-r--r-- |
12857 | 1 |
(* Title: HOL/Bali/WellType.thy |
12854 | 2 |
ID: $Id$ |
3 |
Author: David von Oheimb |
|
12858 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
12854 | 5 |
*) |
6 |
header {* Well-typedness of Java programs *} |
|
7 |
||
8 |
theory WellType = DeclConcepts: |
|
9 |
||
10 |
text {* |
|
11 |
improvements over Java Specification 1.0: |
|
12 |
\begin{itemize} |
|
13 |
\item methods of Object can be called upon references of interface or array type |
|
14 |
\end{itemize} |
|
15 |
simplifications: |
|
16 |
\begin{itemize} |
|
17 |
\item the type rules include all static checks on statements and expressions, |
|
18 |
e.g. definedness of names (of parameters, locals, fields, methods) |
|
19 |
\end{itemize} |
|
20 |
design issues: |
|
21 |
\begin{itemize} |
|
22 |
\item unified type judgment for statements, variables, expressions, |
|
23 |
expression lists |
|
24 |
\item statements are typed like expressions with dummy type Void |
|
25 |
\item the typing rules take an extra argument that is capable of determining |
|
26 |
the dynamic type of objects. Therefore, they can be used for both |
|
27 |
checking static types and determining runtime types in transition semantics. |
|
28 |
\end{itemize} |
|
29 |
*} |
|
30 |
||
31 |
types lenv |
|
32 |
= "(lname, ty) table" (* local variables, including This and Result *) |
|
33 |
||
34 |
record env = |
|
35 |
prg:: "prog" (* program *) |
|
36 |
cls:: "qtname" (* current package and class name *) |
|
37 |
lcl:: "lenv" (* local environment *) |
|
38 |
||
39 |
translations |
|
40 |
"lenv" <= (type) "(lname, ty) table" |
|
41 |
"lenv" <= (type) "lname \<Rightarrow> ty option" |
|
42 |
"env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>" |
|
43 |
"env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>" |
|
44 |
||
45 |
||
46 |
||
47 |
syntax |
|
48 |
pkg :: "env \<Rightarrow> pname" (* select the current package from an environment *) |
|
49 |
translations |
|
50 |
"pkg e" == "pid (cls e)" |
|
51 |
||
52 |
section "Static overloading: maximally specific methods " |
|
53 |
||
54 |
types |
|
55 |
emhead = "ref_ty \<times> mhead" |
|
56 |
||
57 |
(* Some mnemotic selectors for emhead *) |
|
58 |
constdefs |
|
59 |
"declrefT" :: "emhead \<Rightarrow> ref_ty" |
|
60 |
"declrefT \<equiv> fst" |
|
61 |
||
62 |
"mhd" :: "emhead \<Rightarrow> mhead" |
|
63 |
"mhd \<equiv> snd" |
|
64 |
||
65 |
lemma declrefT_simp[simp]:"declrefT (r,m) = r" |
|
66 |
by (simp add: declrefT_def) |
|
67 |
||
68 |
lemma mhd_simp[simp]:"mhd (r,m) = m" |
|
69 |
by (simp add: mhd_def) |
|
70 |
||
71 |
lemma static_mhd_simp[simp]: "static (mhd m) = is_static m" |
|
72 |
by (cases m) (simp add: member_is_static_simp mhd_def) |
|
73 |
||
74 |
lemma mhd_resTy_simp [simp]: "resTy (mhd m) = resTy m" |
|
75 |
by (cases m) simp |
|
76 |
||
77 |
lemma mhd_is_static_simp [simp]: "is_static (mhd m) = is_static m" |
|
78 |
by (cases m) simp |
|
79 |
||
80 |
lemma mhd_accmodi_simp [simp]: "accmodi (mhd m) = accmodi m" |
|
81 |
by (cases m) simp |
|
82 |
||
83 |
consts |
|
84 |
cmheads :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" |
|
85 |
Objectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" |
|
86 |
accObjectmheads:: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set" |
|
87 |
mheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set" |
|
88 |
defs |
|
89 |
cmheads_def: |
|
90 |
"cmheads G S C |
|
91 |
\<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` o2s (accmethd G S C sig)" |
|
92 |
Objectmheads_def: |
|
93 |
"Objectmheads G S |
|
94 |
\<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) |
|
95 |
` o2s (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)" |
|
96 |
accObjectmheads_def: |
|
97 |
"accObjectmheads G S T |
|
98 |
\<equiv> if G\<turnstile>RefT T accessible_in (pid S) |
|
99 |
then Objectmheads G S |
|
100 |
else \<lambda>sig. {}" |
|
101 |
primrec |
|
102 |
"mheads G S NullT = (\<lambda>sig. {})" |
|
103 |
"mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) |
|
104 |
` accimethds G (pid S) I sig \<union> |
|
105 |
accObjectmheads G S (IfaceT I) sig)" |
|
106 |
"mheads G S (ClassT C) = cmheads G S C" |
|
107 |
"mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)" |
|
108 |
||
109 |
||
110 |
(* more detailed than necessary for type-safety, see below. *) |
|
111 |
constdefs |
|
112 |
(* applicable methods, cf. 15.11.2.1 *) |
|
113 |
appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" |
|
114 |
"appl_methds G S rt \<equiv> \<lambda> sig. |
|
115 |
{(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> |
|
116 |
G\<turnstile>(parTs sig)[\<preceq>]pTs'}" |
|
117 |
||
118 |
(* more specific methods, cf. 15.11.2.2 *) |
|
119 |
more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" |
|
120 |
"more_spec G \<equiv> \<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs'" |
|
121 |
(*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*) |
|
122 |
||
123 |
(* maximally specific methods, cf. 15.11.2.2 *) |
|
124 |
max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set" |
|
125 |
||
126 |
"max_spec G S rt sig \<equiv>{m. m \<in>appl_methds G S rt sig \<and> |
|
127 |
(\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}" |
|
128 |
(* |
|
129 |
rules (* all properties of more_spec, appl_methods and max_spec we actually need |
|
130 |
these can easily be proven from the above definitions *) |
|
131 |
||
132 |
max_spec2mheads "max_spec G S rt (mn, pTs) = insert (mh, pTs') A \<Longrightarrow> |
|
133 |
mh\<in>mheads G S rt (mn, pTs') \<and> G\<turnstile>pTs[\<preceq>]pTs'" |
|
134 |
*) |
|
135 |
||
136 |
lemma max_spec2appl_meths: |
|
137 |
"x \<in> max_spec G S T sig \<Longrightarrow> x \<in> appl_methds G S T sig" |
|
138 |
by (auto simp: max_spec_def) |
|
139 |
||
140 |
lemma appl_methsD: "(mh,pTs')\<in>appl_methds G S T \<lparr>name=mn,parTs=pTs\<rparr> \<Longrightarrow> |
|
141 |
mh \<in> mheads G S T \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'" |
|
142 |
by (auto simp: appl_methds_def) |
|
143 |
||
144 |
lemma max_spec2mheads: |
|
145 |
"max_spec G S rt \<lparr>name=mn,parTs=pTs\<rparr> = insert (mh, pTs') A |
|
146 |
\<Longrightarrow> mh \<in> mheads G S rt \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'" |
|
147 |
apply (auto dest: equalityD2 subsetD max_spec2appl_meths appl_methsD) |
|
148 |
done |
|
149 |
||
150 |
||
151 |
constdefs |
|
152 |
empty_dt :: "dyn_ty" |
|
153 |
"empty_dt \<equiv> \<lambda>a. None" |
|
154 |
||
155 |
invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
156 |
"invmode m e \<equiv> if is_static m |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
157 |
then Static |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
158 |
else if e=Super then SuperM else IntVir" |
12854 | 159 |
|
160 |
lemma invmode_nonstatic [simp]: |
|
161 |
"invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir" |
|
162 |
apply (unfold invmode_def) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
163 |
apply (simp (no_asm) add: member_is_static_simp) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
164 |
done |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
165 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
166 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
167 |
lemma invmode_Static_eq [simp]: "(invmode m e = Static) = is_static m" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
168 |
apply (unfold invmode_def) |
12854 | 169 |
apply (simp (no_asm)) |
170 |
done |
|
171 |
||
172 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
173 |
lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(is_static m) \<and> e\<noteq>Super)" |
12854 | 174 |
apply (unfold invmode_def) |
175 |
apply (simp (no_asm)) |
|
176 |
done |
|
177 |
||
178 |
lemma Null_staticD: |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
179 |
"a'=Null \<longrightarrow> (is_static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null" |
12854 | 180 |
apply (clarsimp simp add: invmode_IntVir_eq) |
181 |
done |
|
182 |
||
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
183 |
consts unop_type :: "unop \<Rightarrow> prim_ty" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
184 |
primrec |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
185 |
"unop_type UPlus = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
186 |
"unop_type UMinus = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
187 |
"unop_type UBitNot = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
188 |
"unop_type UNot = Boolean" |
12854 | 189 |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
190 |
consts wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
191 |
primrec |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
192 |
"wt_unop UPlus t = (t = PrimT Integer)" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
193 |
"wt_unop UMinus t = (t = PrimT Integer)" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
194 |
"wt_unop UBitNot t = (t = PrimT Integer)" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
195 |
"wt_unop UNot t = (t = PrimT Boolean)" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
196 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
197 |
consts binop_type :: "binop \<Rightarrow> prim_ty" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
198 |
primrec |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
199 |
"binop_type Mul = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
200 |
"binop_type Div = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
201 |
"binop_type Mod = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
202 |
"binop_type Plus = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
203 |
"binop_type Minus = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
204 |
"binop_type LShift = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
205 |
"binop_type RShift = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
206 |
"binop_type RShiftU = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
207 |
"binop_type Less = Boolean" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
208 |
"binop_type Le = Boolean" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
209 |
"binop_type Greater = Boolean" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
210 |
"binop_type Ge = Boolean" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
211 |
"binop_type Eq = Boolean" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
212 |
"binop_type Neq = Boolean" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
213 |
"binop_type BitAnd = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
214 |
"binop_type And = Boolean" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
215 |
"binop_type BitXor = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
216 |
"binop_type Xor = Boolean" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
217 |
"binop_type BitOr = Integer" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
218 |
"binop_type Or = Boolean" |
13384 | 219 |
"binop_type CondAnd = Boolean" |
220 |
"binop_type CondOr = Boolean" |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
221 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
222 |
consts wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
223 |
primrec |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
224 |
"wt_binop G Mul t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
225 |
"wt_binop G Div t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
226 |
"wt_binop G Mod t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
227 |
"wt_binop G Plus t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
228 |
"wt_binop G Minus t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
229 |
"wt_binop G LShift t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
230 |
"wt_binop G RShift t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
231 |
"wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
232 |
"wt_binop G Less t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
233 |
"wt_binop G Le t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
234 |
"wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
235 |
"wt_binop G Ge t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
236 |
"wt_binop G Eq t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
237 |
"wt_binop G Neq t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
238 |
"wt_binop G BitAnd t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
239 |
"wt_binop G And t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
240 |
"wt_binop G BitXor t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
241 |
"wt_binop G Xor t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
242 |
"wt_binop G BitOr t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
243 |
"wt_binop G Or t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" |
13384 | 244 |
"wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" |
245 |
"wt_binop G CondOr t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
246 |
|
13384 | 247 |
|
12854 | 248 |
types tys = "ty + ty list" |
249 |
translations |
|
250 |
"tys" <= (type) "ty + ty list" |
|
251 |
||
252 |
consts |
|
253 |
wt :: "(env\<spacespace> \<times> dyn_ty\<spacespace> \<times> term \<times> tys) set" |
|
254 |
(*wt :: " env \<Rightarrow> dyn_ty \<Rightarrow> (term \<times> tys) set" not feasible because of |
|
255 |
\<spacespace> changing env in Try stmt *) |
|
256 |
||
257 |
syntax |
|
258 |
wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_|=_::_" [51,51,51,51] 50) |
|
259 |
wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_|=_:<>" [51,51,51 ] 50) |
|
260 |
ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_|=_:-_" [51,51,51,51] 50) |
|
261 |
ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_,_|=_:=_" [51,51,51,51] 50) |
|
262 |
ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, |
|
263 |
\<spacespace> \<spacespace> ty list] \<Rightarrow> bool" ("_,_|=_:#_" [51,51,51,51] 50) |
|
264 |
||
265 |
syntax (xsymbols) |
|
266 |
wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_" [51,51,51,51] 50) |
|
267 |
wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>" [51,51,51 ] 50) |
|
268 |
ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50) |
|
269 |
ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50) |
|
270 |
ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, |
|
271 |
\<spacespace> \<spacespace> ty list] \<Rightarrow> bool"("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50) |
|
272 |
||
273 |
translations |
|
274 |
"E,dt\<Turnstile>t\<Colon>T" == "(E,dt,t,T) \<in> wt" |
|
275 |
"E,dt\<Turnstile>s\<Colon>\<surd>" == "E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)" |
|
276 |
"E,dt\<Turnstile>e\<Colon>-T" == "E,dt\<Turnstile>In1l e\<Colon>Inl T" |
|
277 |
"E,dt\<Turnstile>e\<Colon>=T" == "E,dt\<Turnstile>In2 e\<Colon>Inl T" |
|
278 |
"E,dt\<Turnstile>e\<Colon>\<doteq>T" == "E,dt\<Turnstile>In3 e\<Colon>Inr T" |
|
279 |
||
280 |
syntax (* for purely static typing *) |
|
281 |
wt_ :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50) |
|
282 |
wt_stmt_ :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51 ] 50) |
|
283 |
ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50) |
|
284 |
ty_var_ :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50) |
|
285 |
ty_exprs_:: "env \<Rightarrow> [expr list, |
|
286 |
\<spacespace> ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50) |
|
287 |
||
288 |
syntax (xsymbols) |
|
289 |
wt_ :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_" [51,51,51] 50) |
|
290 |
wt_stmt_ :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50) |
|
291 |
ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50) |
|
292 |
ty_var_ :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50) |
|
293 |
ty_exprs_ :: "env \<Rightarrow> [expr list, |
|
294 |
\<spacespace> ty list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50) |
|
295 |
||
296 |
translations |
|
297 |
"E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T" |
|
298 |
"E\<turnstile>s\<Colon>\<surd>" == "E,empty_dt\<Turnstile>s\<Colon>\<surd>" |
|
299 |
"E\<turnstile>e\<Colon>-T" == "E,empty_dt\<Turnstile>e\<Colon>-T" |
|
300 |
"E\<turnstile>e\<Colon>=T" == "E,empty_dt\<Turnstile>e\<Colon>=T" |
|
301 |
"E\<turnstile>e\<Colon>\<doteq>T" == "E,empty_dt\<Turnstile>e\<Colon>\<doteq>T" |
|
302 |
||
303 |
||
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
304 |
|
12854 | 305 |
inductive wt intros |
306 |
||
307 |
||
308 |
(* well-typed statements *) |
|
309 |
||
310 |
Skip: "E,dt\<Turnstile>Skip\<Colon>\<surd>" |
|
311 |
||
312 |
Expr: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow> |
|
313 |
E,dt\<Turnstile>Expr e\<Colon>\<surd>" |
|
314 |
(* cf. 14.6 *) |
|
315 |
Lab: "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow> |
|
316 |
E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" |
|
317 |
||
318 |
Comp: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; |
|
319 |
E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow> |
|
320 |
E,dt\<Turnstile>c1;; c2\<Colon>\<surd>" |
|
321 |
||
322 |
(* cf. 14.8 *) |
|
323 |
If: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean; |
|
324 |
E,dt\<Turnstile>c1\<Colon>\<surd>; |
|
325 |
E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow> |
|
326 |
E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>" |
|
327 |
||
328 |
(* cf. 14.10 *) |
|
329 |
Loop: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean; |
|
330 |
E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow> |
|
331 |
E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>" |
|
332 |
(* cf. 14.13, 14.15, 14.16 *) |
|
333 |
Do: "E,dt\<Turnstile>Do jump\<Colon>\<surd>" |
|
334 |
||
335 |
(* cf. 14.16 *) |
|
336 |
Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn; |
|
337 |
prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow> |
|
338 |
E,dt\<Turnstile>Throw e\<Colon>\<surd>" |
|
339 |
(* cf. 14.18 *) |
|
340 |
Try: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable; |
|
341 |
lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> |
|
342 |
\<Longrightarrow> |
|
343 |
E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>" |
|
344 |
||
345 |
(* cf. 14.18 *) |
|
346 |
Fin: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow> |
|
347 |
E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>" |
|
348 |
||
349 |
Init: "\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow> |
|
350 |
E,dt\<Turnstile>Init C\<Colon>\<surd>" |
|
351 |
(* Init is created on the fly during evaluation (see Eval.thy). The class |
|
352 |
* isn't necessarily accessible from the points Init is called. Therefor |
|
353 |
* we only demand is_class and not is_acc_class here |
|
354 |
*) |
|
355 |
||
356 |
(* well-typed expressions *) |
|
357 |
||
358 |
(* cf. 15.8 *) |
|
359 |
NewC: "\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow> |
|
360 |
E,dt\<Turnstile>NewC C\<Colon>-Class C" |
|
361 |
(* cf. 15.9 *) |
|
362 |
NewA: "\<lbrakk>is_acc_type (prg E) (pkg E) T; |
|
363 |
E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow> |
|
364 |
E,dt\<Turnstile>New T[i]\<Colon>-T.[]" |
|
365 |
||
366 |
(* cf. 15.15 *) |
|
367 |
Cast: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T'; |
|
368 |
prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow> |
|
369 |
E,dt\<Turnstile>Cast T' e\<Colon>-T'" |
|
370 |
||
371 |
(* cf. 15.19.2 *) |
|
372 |
Inst: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T'); |
|
373 |
prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow> |
|
374 |
E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean" |
|
375 |
||
376 |
(* cf. 15.7.1 *) |
|
377 |
Lit: "\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow> |
|
378 |
E,dt\<Turnstile>Lit x\<Colon>-T" |
|
379 |
||
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
380 |
UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
381 |
\<Longrightarrow> |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
382 |
E,dt\<Turnstile>UnOp unop e\<Colon>-T" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
383 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
384 |
BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
385 |
T=PrimT (binop_type binop)\<rbrakk> |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
386 |
\<Longrightarrow> |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
387 |
E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
388 |
|
12854 | 389 |
(* cf. 15.10.2, 15.11.1 *) |
390 |
Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; |
|
391 |
class (prg E) C = Some c\<rbrakk> \<Longrightarrow> |
|
392 |
E,dt\<Turnstile>Super\<Colon>-Class (super c)" |
|
393 |
||
394 |
(* cf. 15.13.1, 15.10.1, 15.12 *) |
|
395 |
Acc: "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow> |
|
396 |
E,dt\<Turnstile>Acc va\<Colon>-T" |
|
397 |
||
398 |
(* cf. 15.25, 15.25.1 *) |
|
399 |
Ass: "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This; |
|
400 |
E,dt\<Turnstile>v \<Colon>-T'; |
|
401 |
prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow> |
|
402 |
E,dt\<Turnstile>va:=v\<Colon>-T'" |
|
403 |
||
404 |
(* cf. 15.24 *) |
|
405 |
Cond: "\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean; |
|
406 |
E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; |
|
407 |
prg E\<turnstile>T1\<preceq>T2 \<and> T = T2 \<or> prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow> |
|
408 |
E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T" |
|
409 |
||
410 |
(* cf. 15.11.1, 15.11.2, 15.11.3 *) |
|
411 |
Call: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; |
|
412 |
E,dt\<Turnstile>ps\<Colon>\<doteq>pTs; |
|
413 |
max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> |
|
414 |
= {((statDeclT,m),pTs')} |
|
415 |
\<rbrakk> \<Longrightarrow> |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
416 |
E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)" |
12854 | 417 |
|
418 |
Methd: "\<lbrakk>is_class (prg E) C; |
|
419 |
methd (prg E) C sig = Some m; |
|
420 |
E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow> |
|
421 |
E,dt\<Turnstile>Methd C sig\<Colon>-T" |
|
422 |
(* The class C is the dynamic class of the method call (cf. Eval.thy). |
|
423 |
* It hasn't got to be directly accessible from the current package (pkg E). |
|
424 |
* Only the static class must be accessible (enshured indirectly by Call). |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
425 |
* Note that l is just a dummy value. It is only used in the smallstep |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
426 |
* semantics. To proof typesafety directly for the smallstep semantics |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
427 |
* we would have to assume conformance of l here! |
12854 | 428 |
*) |
429 |
||
430 |
Body: "\<lbrakk>is_class (prg E) D; |
|
431 |
E,dt\<Turnstile>blk\<Colon>\<surd>; |
|
432 |
(lcl E) Result = Some T; |
|
433 |
is_type (prg E) T\<rbrakk> \<Longrightarrow> |
|
434 |
E,dt\<Turnstile>Body D blk\<Colon>-T" |
|
435 |
(* the class D implementing the method must not directly be accessible |
|
436 |
* from the current package (pkg E), but can also be indirectly accessible |
|
437 |
* due to inheritance (enshured in Call) |
|
438 |
* The result type hasn't got to be accessible in Java! (If it is not |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
439 |
* accessible you can only assign it to Object). |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
440 |
* For dummy value l see rule Methd. |
12854 | 441 |
*) |
442 |
||
443 |
(* well-typed variables *) |
|
444 |
||
445 |
(* cf. 15.13.1 *) |
|
446 |
LVar: "\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow> |
|
447 |
E,dt\<Turnstile>LVar vn\<Colon>=T" |
|
448 |
(* cf. 15.10.1 *) |
|
449 |
FVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
450 |
accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow> |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
451 |
E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)" |
12854 | 452 |
(* cf. 15.12 *) |
453 |
AVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; |
|
454 |
E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow> |
|
455 |
E,dt\<Turnstile>e.[i]\<Colon>=T" |
|
456 |
||
457 |
||
458 |
(* well-typed expression lists *) |
|
459 |
||
460 |
(* cf. 15.11.??? *) |
|
461 |
Nil: "E,dt\<Turnstile>[]\<Colon>\<doteq>[]" |
|
462 |
||
463 |
(* cf. 15.11.??? *) |
|
464 |
Cons: "\<lbrakk>E,dt\<Turnstile>e \<Colon>-T; |
|
465 |
E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow> |
|
466 |
E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts" |
|
467 |
||
468 |
||
469 |
declare not_None_eq [simp del] |
|
470 |
declare split_if [split del] split_if_asm [split del] |
|
471 |
declare split_paired_All [simp del] split_paired_Ex [simp del] |
|
472 |
ML_setup {* |
|
473 |
simpset_ref() := simpset() delloop "split_all_tac" |
|
474 |
*} |
|
475 |
inductive_cases wt_stmt_cases: "E,dt\<Turnstile>c\<Colon>\<surd>" |
|
476 |
inductive_cases wt_elim_cases: |
|
477 |
"E,dt\<Turnstile>In2 (LVar vn) \<Colon>T" |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
478 |
"E,dt\<Turnstile>In2 ({accC,statDeclC,s}e..fn)\<Colon>T" |
12854 | 479 |
"E,dt\<Turnstile>In2 (e.[i]) \<Colon>T" |
480 |
"E,dt\<Turnstile>In1l (NewC C) \<Colon>T" |
|
481 |
"E,dt\<Turnstile>In1l (New T'[i]) \<Colon>T" |
|
482 |
"E,dt\<Turnstile>In1l (Cast T' e) \<Colon>T" |
|
483 |
"E,dt\<Turnstile>In1l (e InstOf T') \<Colon>T" |
|
484 |
"E,dt\<Turnstile>In1l (Lit x) \<Colon>T" |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
485 |
"E,dt\<Turnstile>In1l (UnOp unop e) \<Colon>T" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
486 |
"E,dt\<Turnstile>In1l (BinOp binop e1 e2) \<Colon>T" |
12854 | 487 |
"E,dt\<Turnstile>In1l (Super) \<Colon>T" |
488 |
"E,dt\<Turnstile>In1l (Acc va) \<Colon>T" |
|
489 |
"E,dt\<Turnstile>In1l (Ass va v) \<Colon>T" |
|
490 |
"E,dt\<Turnstile>In1l (e0 ? e1 : e2) \<Colon>T" |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
491 |
"E,dt\<Turnstile>In1l ({accC,statT,mode}e\<cdot>mn({pT'}p))\<Colon>T" |
12854 | 492 |
"E,dt\<Turnstile>In1l (Methd C sig) \<Colon>T" |
493 |
"E,dt\<Turnstile>In1l (Body D blk) \<Colon>T" |
|
494 |
"E,dt\<Turnstile>In3 ([]) \<Colon>Ts" |
|
495 |
"E,dt\<Turnstile>In3 (e#es) \<Colon>Ts" |
|
496 |
"E,dt\<Turnstile>In1r Skip \<Colon>x" |
|
497 |
"E,dt\<Turnstile>In1r (Expr e) \<Colon>x" |
|
498 |
"E,dt\<Turnstile>In1r (c1;; c2) \<Colon>x" |
|
499 |
"E,dt\<Turnstile>In1r (l\<bullet> c) \<Colon>x" |
|
500 |
"E,dt\<Turnstile>In1r (If(e) c1 Else c2) \<Colon>x" |
|
501 |
"E,dt\<Turnstile>In1r (l\<bullet> While(e) c) \<Colon>x" |
|
502 |
"E,dt\<Turnstile>In1r (Do jump) \<Colon>x" |
|
503 |
"E,dt\<Turnstile>In1r (Throw e) \<Colon>x" |
|
504 |
"E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x" |
|
505 |
"E,dt\<Turnstile>In1r (c1 Finally c2) \<Colon>x" |
|
506 |
"E,dt\<Turnstile>In1r (Init C) \<Colon>x" |
|
507 |
declare not_None_eq [simp] |
|
508 |
declare split_if [split] split_if_asm [split] |
|
509 |
declare split_paired_All [simp] split_paired_Ex [simp] |
|
510 |
ML_setup {* |
|
511 |
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac) |
|
512 |
*} |
|
513 |
||
514 |
lemma is_acc_class_is_accessible: |
|
515 |
"is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P" |
|
516 |
by (auto simp add: is_acc_class_def) |
|
517 |
||
518 |
lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I" |
|
519 |
by (auto simp add: is_acc_iface_def) |
|
520 |
||
13524 | 521 |
lemma is_acc_iface_Iface_is_accessible: |
12854 | 522 |
"is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P" |
523 |
by (auto simp add: is_acc_iface_def) |
|
524 |
||
525 |
lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T" |
|
526 |
by (auto simp add: is_acc_type_def) |
|
527 |
||
13524 | 528 |
lemma is_acc_iface_is_accessible: |
529 |
"is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P" |
|
12854 | 530 |
by (auto simp add: is_acc_type_def) |
531 |
||
532 |
lemma wt_Methd_is_methd: |
|
533 |
"E\<turnstile>In1l (Methd C sig)\<Colon>T \<Longrightarrow> is_methd (prg E) C sig" |
|
534 |
apply (erule_tac wt_elim_cases) |
|
535 |
apply clarsimp |
|
536 |
apply (erule is_methdI, assumption) |
|
537 |
done |
|
538 |
||
539 |
(* Special versions of some typing rules, better suited to pattern match the |
|
540 |
* conclusion (no selectors in the conclusion\<dots>) |
|
541 |
*) |
|
542 |
||
543 |
lemma wt_Call: |
|
544 |
"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs; |
|
545 |
max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
546 |
= {((statDeclC,m),pTs')};rT=(resTy m);accC=cls E; |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
547 |
mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT" |
12854 | 548 |
by (auto elim: wt.Call) |
549 |
||
550 |
||
551 |
lemma invocationTypeExpr_noClassD: |
|
552 |
"\<lbrakk> E\<turnstile>e\<Colon>-RefT statT\<rbrakk> |
|
553 |
\<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM" |
|
554 |
proof - |
|
555 |
assume wt: "E\<turnstile>e\<Colon>-RefT statT" |
|
556 |
show ?thesis |
|
557 |
proof (cases "e=Super") |
|
558 |
case True |
|
559 |
with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases) |
|
560 |
then show ?thesis by blast |
|
561 |
next |
|
562 |
case False then show ?thesis |
|
563 |
by (auto simp add: invmode_def split: split_if_asm) |
|
564 |
qed |
|
565 |
qed |
|
566 |
||
567 |
lemma wt_Super: |
|
568 |
"\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk> |
|
569 |
\<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D" |
|
570 |
by (auto elim: wt.Super) |
|
571 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
572 |
lemma wt_FVar: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
573 |
"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC,f); |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
574 |
sf=is_static f; fT=(type f); accC=cls E\<rbrakk> |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
575 |
\<Longrightarrow> E,dt\<Turnstile>{accC,statDeclC,sf}e..fn\<Colon>=fT" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
576 |
by (auto dest: wt.FVar) |
12854 | 577 |
|
578 |
||
579 |
lemma wt_init [iff]: "E,dt\<Turnstile>Init C\<Colon>\<surd> = is_class (prg E) C" |
|
580 |
by (auto elim: wt_elim_cases intro: "wt.Init") |
|
581 |
||
582 |
declare wt.Skip [iff] |
|
583 |
||
584 |
lemma wt_StatRef: |
|
585 |
"is_acc_type (prg E) (pkg E) (RefT rt) \<Longrightarrow> E\<turnstile>StatRef rt\<Colon>-RefT rt" |
|
586 |
apply (rule wt.Cast) |
|
587 |
apply (rule wt.Lit) |
|
588 |
apply (simp (no_asm)) |
|
589 |
apply (simp (no_asm_simp)) |
|
590 |
apply (rule cast.widen) |
|
591 |
apply (simp (no_asm)) |
|
592 |
done |
|
593 |
||
594 |
lemma wt_Inj_elim: |
|
595 |
"\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of |
|
596 |
In1 ec \<Rightarrow> (case ec of |
|
597 |
Inl e \<Rightarrow> \<exists>T. U=Inl T |
|
598 |
| Inr s \<Rightarrow> U=Inl (PrimT Void)) |
|
599 |
| In2 e \<Rightarrow> (\<exists>T. U=Inl T) |
|
600 |
| In3 e \<Rightarrow> (\<exists>T. U=Inr T)" |
|
601 |
apply (erule wt.induct) |
|
602 |
apply auto |
|
603 |
done |
|
604 |
||
605 |
ML {* |
|
606 |
fun wt_fun name inj rhs = |
|
607 |
let |
|
608 |
val lhs = "E,dt\<Turnstile>" ^ inj ^ " t\<Colon>U" |
|
609 |
val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") |
|
610 |
(K [Auto_tac, ALLGOALS (ftac (thm "wt_Inj_elim")) THEN Auto_tac]) |
|
611 |
fun is_Inj (Const (inj,_) $ _) = true |
|
612 |
| is_Inj _ = false |
|
613 |
fun pred (t as (_ $ (Const ("Pair",_) $ |
|
614 |
_ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $ |
|
615 |
x))) $ _ )) = is_Inj x |
|
616 |
in |
|
13462 | 617 |
cond_simproc name lhs pred (thm name) |
12854 | 618 |
end |
619 |
||
620 |
val wt_expr_proc = wt_fun "wt_expr_eq" "In1l" "\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>-T" |
|
621 |
val wt_var_proc = wt_fun "wt_var_eq" "In2" "\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>=T" |
|
622 |
val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3" "\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts" |
|
623 |
val wt_stmt_proc = wt_fun "wt_stmt_eq" "In1r" "U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>" |
|
624 |
*} |
|
625 |
||
626 |
ML {* |
|
627 |
Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc] |
|
628 |
*} |
|
629 |
||
630 |
lemma Inj_eq_lemma [simp]: |
|
631 |
"(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))" |
|
632 |
by auto |
|
633 |
||
634 |
(* unused *) |
|
635 |
lemma single_valued_tys_lemma [rule_format (no_asm)]: |
|
636 |
"\<forall>S T. G\<turnstile>S\<preceq>T \<longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T \<Longrightarrow> E,dt\<Turnstile>t\<Colon>T \<Longrightarrow> |
|
637 |
G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T = T')" |
|
638 |
apply (cases "E", erule wt.induct) |
|
639 |
apply (safe del: disjE) |
|
640 |
apply (simp_all (no_asm_use) split del: split_if_asm) |
|
641 |
apply (safe del: disjE) |
|
642 |
(* 17 subgoals *) |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
643 |
apply (tactic {* ALLGOALS (fn i => if i = 11 then EVERY'[thin_tac "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean", thin_tac "?E,dt\<Turnstile>e1\<Colon>-?T1", thin_tac "?E,dt\<Turnstile>e2\<Colon>-?T2"] i else thin_tac "All ?P" i) *}) |
12854 | 644 |
(*apply (safe del: disjE elim!: wt_elim_cases)*) |
645 |
apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*}) |
|
646 |
apply (simp_all (no_asm_use) split del: split_if_asm) |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
647 |
apply (erule_tac [12] V = "All ?P" in thin_rl) (* Call *) |
12854 | 648 |
apply ((blast del: equalityCE dest: sym [THEN trans])+) |
649 |
done |
|
650 |
||
651 |
(* unused *) |
|
652 |
lemma single_valued_tys: |
|
653 |
"ws_prog (prg E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}" |
|
654 |
apply (unfold single_valued_def) |
|
655 |
apply clarsimp |
|
656 |
apply (rule single_valued_tys_lemma) |
|
657 |
apply (auto intro!: widen_antisym) |
|
658 |
done |
|
659 |
||
660 |
lemma typeof_empty_is_type [rule_format (no_asm)]: |
|
661 |
"typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T" |
|
662 |
apply (rule val.induct) |
|
663 |
apply auto |
|
664 |
done |
|
665 |
||
666 |
(* unused *) |
|
667 |
lemma typeof_is_type [rule_format (no_asm)]: |
|
668 |
"(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)" |
|
669 |
apply (rule val.induct) |
|
670 |
prefer 5 |
|
671 |
apply fast |
|
672 |
apply (simp_all (no_asm)) |
|
673 |
done |
|
674 |
||
675 |
end |