author | urbanc |
Wed, 11 Jan 2006 12:14:25 +0100 | |
changeset 18651 | 0cb5a8f501aa |
parent 18249 | 4398f0f12579 |
child 21765 | 89275a3ed7be |
permissions | -rw-r--r-- |
12857 | 1 |
(* Title: HOL/Bali/Eval.thy |
12854 | 2 |
ID: $Id$ |
3 |
Author: David von Oheimb |
|
4 |
*) |
|
5 |
header {* Operational evaluation (big-step) semantics of Java expressions and |
|
6 |
statements |
|
7 |
*} |
|
8 |
||
16417 | 9 |
theory Eval imports State DeclConcepts begin |
12854 | 10 |
|
11 |
text {* |
|
12 |
||
13 |
improvements over Java Specification 1.0: |
|
14 |
\begin{itemize} |
|
15 |
\item dynamic method lookup does not need to consider the return type |
|
16 |
(cf.15.11.4.4) |
|
17 |
\item throw raises a NullPointer exception if a null reference is given, and |
|
18 |
each throw of a standard exception yield a fresh exception object |
|
19 |
(was not specified) |
|
20 |
\item if there is not enough memory even to allocate an OutOfMemory exception, |
|
21 |
evaluation/execution fails, i.e. simply stops (was not specified) |
|
22 |
\item array assignment checks lhs (and may throw exceptions) before evaluating |
|
23 |
rhs |
|
24 |
\item fixed exact positions of class initializations |
|
25 |
(immediate at first active use) |
|
26 |
\end{itemize} |
|
27 |
||
28 |
design issues: |
|
29 |
\begin{itemize} |
|
30 |
\item evaluation vs. (single-step) transition semantics |
|
31 |
evaluation semantics chosen, because: |
|
32 |
\begin{itemize} |
|
33 |
\item[++] less verbose and therefore easier to read (and to handle in proofs) |
|
34 |
\item[+] more abstract |
|
35 |
\item[+] intermediate values (appearing in recursive rules) need not be |
|
36 |
stored explicitly, e.g. no call body construct or stack of invocation |
|
37 |
frames containing local variables and return addresses for method calls |
|
38 |
needed |
|
39 |
\item[+] convenient rule induction for subject reduction theorem |
|
40 |
\item[-] no interleaving (for parallelism) can be described |
|
41 |
\item[-] stating a property of infinite executions requires the meta-level |
|
42 |
argument that this property holds for any finite prefixes of it |
|
43 |
(e.g. stopped using a counter that is decremented to zero and then |
|
44 |
throwing an exception) |
|
45 |
\end{itemize} |
|
46 |
\item unified evaluation for variables, expressions, expression lists, |
|
47 |
statements |
|
48 |
\item the value entry in statement rules is redundant |
|
49 |
\item the value entry in rules is irrelevant in case of exceptions, but its full |
|
50 |
inclusion helps to make the rule structure independent of exception occurence. |
|
51 |
\item as irrelevant value entries are ignored, it does not matter if they are |
|
52 |
unique. |
|
53 |
For simplicity, (fixed) arbitrary values are preferred over "free" values. |
|
54 |
\item the rule format is such that the start state may contain an exception. |
|
55 |
\begin{itemize} |
|
56 |
\item[++] faciliates exception handling |
|
57 |
\item[+] symmetry |
|
58 |
\end{itemize} |
|
59 |
\item the rules are defined carefully in order to be applicable even in not |
|
60 |
type-correct situations (yielding undefined values), |
|
61 |
e.g. @{text "the_Addr (Val (Bool b)) = arbitrary"}. |
|
62 |
\begin{itemize} |
|
63 |
\item[++] fewer rules |
|
64 |
\item[-] less readable because of auxiliary functions like @{text the_Addr} |
|
65 |
\end{itemize} |
|
66 |
Alternative: "defensive" evaluation throwing some InternalError exception |
|
67 |
in case of (impossible, for correct programs) type mismatches |
|
68 |
\item there is exactly one rule per syntactic construct |
|
69 |
\begin{itemize} |
|
70 |
\item[+] no redundancy in case distinctions |
|
71 |
\end{itemize} |
|
72 |
\item halloc fails iff there is no free heap address. When there is |
|
73 |
only one free heap address left, it returns an OutOfMemory exception. |
|
74 |
In this way it is guaranteed that when an OutOfMemory exception is thrown for |
|
75 |
the first time, there is a free location on the heap to allocate it. |
|
76 |
\item the allocation of objects that represent standard exceptions is deferred |
|
77 |
until execution of any enclosing catch clause, which is transparent to |
|
78 |
the program. |
|
79 |
\begin{itemize} |
|
80 |
\item[-] requires an auxiliary execution relation |
|
81 |
\item[++] avoids copies of allocation code and awkward case distinctions |
|
82 |
(whether there is enough memory to allocate the exception) in |
|
83 |
evaluation rules |
|
84 |
\end{itemize} |
|
85 |
\item unfortunately @{text new_Addr} is not directly executable because of |
|
86 |
Hilbert operator. |
|
87 |
\end{itemize} |
|
88 |
simplifications: |
|
89 |
\begin{itemize} |
|
90 |
\item local variables are initialized with default values |
|
91 |
(no definite assignment) |
|
92 |
\item garbage collection not considered, therefore also no finalizers |
|
93 |
\item stack overflow and memory overflow during class initialization not |
|
94 |
modelled |
|
95 |
\item exceptions in initializations not replaced by ExceptionInInitializerError |
|
96 |
\end{itemize} |
|
97 |
*} |
|
98 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
99 |
|
12854 | 100 |
types vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)" |
101 |
vals = "(val, vvar, val list) sum3" |
|
102 |
translations |
|
103 |
"vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)" |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
104 |
"vals" <= (type)"(val, vvar, val list) sum3" |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
105 |
|
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
106 |
text {* To avoid redundancy and to reduce the number of rules, there is only |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
107 |
one evaluation rule for each syntactic term. This is also true for variables |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
108 |
(e.g. see the rules below for @{text LVar}, @{text FVar} and @{text AVar}). |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
109 |
So evaluation of a variable must capture both possible further uses: |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
110 |
read (rule @{text Acc}) or write (rule @{text Ass}) to the variable. |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
111 |
Therefor a variable evaluates to a special value @{term vvar}, which is |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
112 |
a pair, consisting of the current value (for later read access) and an update |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
113 |
function (for later write access). Because |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
114 |
during assignment to an array variable an exception may occur if the types |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
115 |
don't match, the update function is very generic: it transforms the |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
116 |
full state. This generic update function causes some technical trouble during |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
117 |
some proofs (e.g. type safety, correctness of definite assignment). There we |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
118 |
need to prove some additional invariant on this update function to prove the |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
119 |
assignment correct, since the update function could potentially alter the whole |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
120 |
state in an arbitrary manner. This invariant must be carried around through |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
121 |
the whole induction. |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
122 |
So for future approaches it may be better not to take |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
123 |
such a generic update function, but only to store the address and the kind |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
124 |
of variable (array (+ element type), local variable or field) for later |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
125 |
assignment. |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
126 |
*} |
12854 | 127 |
|
128 |
syntax (xsymbols) |
|
129 |
dummy_res :: "vals" ("\<diamondsuit>") |
|
130 |
translations |
|
131 |
"\<diamondsuit>" == "In1 Unit" |
|
132 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
133 |
syntax |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
134 |
val_inj_vals:: "expr \<Rightarrow> term" ("\<lfloor>_\<rfloor>\<^sub>e" 1000) |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
135 |
var_inj_vals:: "var \<Rightarrow> term" ("\<lfloor>_\<rfloor>\<^sub>v" 1000) |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
136 |
lst_inj_vals:: "expr list \<Rightarrow> term" ("\<lfloor>_\<rfloor>\<^sub>l" 1000) |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
137 |
|
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
138 |
translations |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
139 |
"\<lfloor>e\<rfloor>\<^sub>e" \<rightharpoonup> "In1 e" |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
140 |
"\<lfloor>v\<rfloor>\<^sub>v" \<rightharpoonup> "In2 v" |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
141 |
"\<lfloor>es\<rfloor>\<^sub>l" \<rightharpoonup> "In3 es" |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
142 |
|
12854 | 143 |
constdefs |
144 |
arbitrary3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals" |
|
145 |
"arbitrary3 \<equiv> sum3_case (In1 \<circ> sum_case (\<lambda>x. arbitrary) (\<lambda>x. Unit)) |
|
146 |
(\<lambda>x. In2 arbitrary) (\<lambda>x. In3 arbitrary)" |
|
147 |
||
148 |
lemma [simp]: "arbitrary3 (In1l x) = In1 arbitrary" |
|
149 |
by (simp add: arbitrary3_def) |
|
150 |
||
151 |
lemma [simp]: "arbitrary3 (In1r x) = \<diamondsuit>" |
|
152 |
by (simp add: arbitrary3_def) |
|
153 |
||
154 |
lemma [simp]: "arbitrary3 (In2 x) = In2 arbitrary" |
|
155 |
by (simp add: arbitrary3_def) |
|
156 |
||
157 |
lemma [simp]: "arbitrary3 (In3 x) = In3 arbitrary" |
|
158 |
by (simp add: arbitrary3_def) |
|
159 |
||
160 |
||
161 |
section "exception throwing and catching" |
|
162 |
||
163 |
constdefs |
|
164 |
throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt" |
|
165 |
"throw a' x \<equiv> abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)" |
|
166 |
||
167 |
lemma throw_def2: |
|
168 |
"throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)" |
|
169 |
apply (unfold throw_def) |
|
170 |
apply (simp (no_asm)) |
|
171 |
done |
|
172 |
||
173 |
constdefs |
|
174 |
fits :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60) |
|
175 |
"G,s\<turnstile>a' fits T \<equiv> (\<exists>rt. T=RefT rt) \<longrightarrow> a'=Null \<or> G\<turnstile>obj_ty(lookup_obj s a')\<preceq>T" |
|
176 |
||
177 |
lemma fits_Null [simp]: "G,s\<turnstile>Null fits T" |
|
178 |
by (simp add: fits_def) |
|
179 |
||
180 |
||
181 |
lemma fits_Addr_RefT [simp]: |
|
182 |
"G,s\<turnstile>Addr a fits RefT t = G\<turnstile>obj_ty (the (heap s a))\<preceq>RefT t" |
|
183 |
by (simp add: fits_def) |
|
184 |
||
185 |
lemma fitsD: "\<And>X. G,s\<turnstile>a' fits T \<Longrightarrow> (\<exists>pt. T = PrimT pt) \<or> |
|
186 |
(\<exists>t. T = RefT t) \<and> a' = Null \<or> |
|
187 |
(\<exists>t. T = RefT t) \<and> a' \<noteq> Null \<and> G\<turnstile>obj_ty (lookup_obj s a')\<preceq>T" |
|
188 |
apply (unfold fits_def) |
|
189 |
apply (case_tac "\<exists>pt. T = PrimT pt") |
|
190 |
apply simp_all |
|
191 |
apply (case_tac "T") |
|
192 |
defer |
|
193 |
apply (case_tac "a' = Null") |
|
194 |
apply simp_all |
|
17589 | 195 |
apply iprover |
12854 | 196 |
done |
197 |
||
198 |
constdefs |
|
199 |
catch ::"prog \<Rightarrow> state \<Rightarrow> qtname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60) |
|
200 |
"G,s\<turnstile>catch C\<equiv>\<exists>xc. abrupt s=Some (Xcpt xc) \<and> |
|
201 |
G,store s\<turnstile>Addr (the_Loc xc) fits Class C" |
|
202 |
||
203 |
lemma catch_Norm [simp]: "\<not>G,Norm s\<turnstile>catch tn" |
|
204 |
apply (unfold catch_def) |
|
205 |
apply (simp (no_asm)) |
|
206 |
done |
|
207 |
||
208 |
lemma catch_XcptLoc [simp]: |
|
209 |
"G,(Some (Xcpt (Loc a)),s)\<turnstile>catch C = G,s\<turnstile>Addr a fits Class C" |
|
210 |
apply (unfold catch_def) |
|
211 |
apply (simp (no_asm)) |
|
212 |
done |
|
213 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
214 |
lemma catch_Jump [simp]: "\<not>G,(Some (Jump j),s)\<turnstile>catch tn" |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
215 |
apply (unfold catch_def) |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
216 |
apply (simp (no_asm)) |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
217 |
done |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
218 |
|
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
219 |
lemma catch_Error [simp]: "\<not>G,(Some (Error e),s)\<turnstile>catch tn" |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
220 |
apply (unfold catch_def) |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
221 |
apply (simp (no_asm)) |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
222 |
done |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
223 |
|
12854 | 224 |
constdefs |
225 |
new_xcpt_var :: "vname \<Rightarrow> state \<Rightarrow> state" |
|
226 |
"new_xcpt_var vn \<equiv> |
|
227 |
\<lambda>(x,s). Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)" |
|
228 |
||
229 |
lemma new_xcpt_var_def2 [simp]: |
|
230 |
"new_xcpt_var vn (x,s) = |
|
231 |
Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)" |
|
232 |
apply (unfold new_xcpt_var_def) |
|
233 |
apply (simp (no_asm)) |
|
234 |
done |
|
235 |
||
236 |
||
237 |
||
238 |
section "misc" |
|
239 |
||
240 |
constdefs |
|
241 |
||
242 |
assign :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state" |
|
243 |
"assign f v \<equiv> \<lambda>(x,s). let (x',s') = (if x = None then f v else id) (x,s) |
|
244 |
in (x',if x' = None then s' else s)" |
|
245 |
||
246 |
(* |
|
247 |
lemma assign_Norm_Norm [simp]: |
|
248 |
"f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=None,store=s'\<rparr> |
|
249 |
\<Longrightarrow> assign f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=None,store=s'\<rparr>" |
|
250 |
by (simp add: assign_def Let_def) |
|
251 |
*) |
|
252 |
||
253 |
lemma assign_Norm_Norm [simp]: |
|
254 |
"f v (Norm s) = Norm s' \<Longrightarrow> assign f v (Norm s) = Norm s'" |
|
255 |
by (simp add: assign_def Let_def) |
|
256 |
||
257 |
(* |
|
258 |
lemma assign_Norm_Some [simp]: |
|
259 |
"\<lbrakk>abrupt (f v \<lparr>abrupt=None,store=s\<rparr>) = Some y\<rbrakk> |
|
260 |
\<Longrightarrow> assign f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=Some y,store =s\<rparr>" |
|
261 |
by (simp add: assign_def Let_def split_beta) |
|
262 |
*) |
|
263 |
||
264 |
lemma assign_Norm_Some [simp]: |
|
265 |
"\<lbrakk>abrupt (f v (Norm s)) = Some y\<rbrakk> |
|
266 |
\<Longrightarrow> assign f v (Norm s) = (Some y,s)" |
|
267 |
by (simp add: assign_def Let_def split_beta) |
|
268 |
||
269 |
||
270 |
lemma assign_Some [simp]: |
|
271 |
"assign f v (Some x,s) = (Some x,s)" |
|
272 |
by (simp add: assign_def Let_def split_beta) |
|
273 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
274 |
lemma assign_Some1 [simp]: "\<not> normal s \<Longrightarrow> assign f v s = s" |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
275 |
by (auto simp add: assign_def Let_def split_beta) |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
276 |
|
12854 | 277 |
lemma assign_supd [simp]: |
278 |
"assign (\<lambda>v. supd (f v)) v (x,s) |
|
279 |
= (x, if x = None then f v s else s)" |
|
280 |
apply auto |
|
281 |
done |
|
282 |
||
283 |
lemma assign_raise_if [simp]: |
|
284 |
"assign (\<lambda>v (x,s). ((raise_if (b s v) xcpt) x, f v s)) v (x, s) = |
|
285 |
(raise_if (b s v) xcpt x, if x=None \<and> \<not>b s v then f v s else s)" |
|
286 |
apply (case_tac "x = None") |
|
287 |
apply auto |
|
288 |
done |
|
289 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
290 |
|
12854 | 291 |
(* |
292 |
lemma assign_raise_if [simp]: |
|
293 |
"assign (\<lambda>v s. \<lparr>abrupt=(raise_if (b (store s) v) xcpt) (abrupt s), |
|
294 |
store = f v (store s)\<rparr>) v s = |
|
295 |
\<lparr>abrupt=raise_if (b (store s) v) xcpt (abrupt s), |
|
296 |
store= if (abrupt s)=None \<and> \<not>b (store s) v |
|
297 |
then f v (store s) else (store s)\<rparr>" |
|
298 |
apply (case_tac "abrupt s = None") |
|
299 |
apply auto |
|
300 |
done |
|
301 |
*) |
|
302 |
||
303 |
constdefs |
|
304 |
||
305 |
init_comp_ty :: "ty \<Rightarrow> stmt" |
|
306 |
"init_comp_ty T \<equiv> if (\<exists>C. T = Class C) then Init (the_Class T) else Skip" |
|
307 |
||
308 |
lemma init_comp_ty_PrimT [simp]: "init_comp_ty (PrimT pt) = Skip" |
|
309 |
apply (unfold init_comp_ty_def) |
|
310 |
apply (simp (no_asm)) |
|
311 |
done |
|
312 |
||
313 |
constdefs |
|
314 |
||
315 |
invocation_class :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname" |
|
316 |
"invocation_class m s a' statT |
|
317 |
\<equiv> (case m of |
|
318 |
Static \<Rightarrow> if (\<exists> statC. statT = ClassT statC) |
|
319 |
then the_Class (RefT statT) |
|
320 |
else Object |
|
321 |
| SuperM \<Rightarrow> the_Class (RefT statT) |
|
322 |
| IntVir \<Rightarrow> obj_class (lookup_obj s a'))" |
|
323 |
||
324 |
invocation_declclass::"prog \<Rightarrow> inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> qtname" |
|
325 |
"invocation_declclass G m s a' statT sig |
|
326 |
\<equiv> declclass (the (dynlookup G statT |
|
327 |
(invocation_class m s a' statT) |
|
328 |
sig))" |
|
329 |
||
330 |
lemma invocation_class_IntVir [simp]: |
|
331 |
"invocation_class IntVir s a' statT = obj_class (lookup_obj s a')" |
|
332 |
by (simp add: invocation_class_def) |
|
333 |
||
334 |
lemma dynclass_SuperM [simp]: |
|
335 |
"invocation_class SuperM s a' statT = the_Class (RefT statT)" |
|
336 |
by (simp add: invocation_class_def) |
|
337 |
||
338 |
lemma invocation_class_Static [simp]: |
|
339 |
"invocation_class Static s a' statT = (if (\<exists> statC. statT = ClassT statC) |
|
340 |
then the_Class (RefT statT) |
|
341 |
else Object)" |
|
342 |
by (simp add: invocation_class_def) |
|
343 |
||
344 |
constdefs |
|
345 |
init_lvars :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> inv_mode \<Rightarrow> val \<Rightarrow> val list \<Rightarrow> |
|
346 |
state \<Rightarrow> state" |
|
347 |
"init_lvars G C sig mode a' pvs |
|
348 |
\<equiv> \<lambda> (x,s). |
|
349 |
let m = mthd (the (methd G C sig)); |
|
350 |
l = \<lambda> k. |
|
351 |
(case k of |
|
352 |
EName e |
|
353 |
\<Rightarrow> (case e of |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
354 |
VNam v \<Rightarrow> (empty ((pars m)[\<mapsto>]pvs)) v |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
355 |
| Res \<Rightarrow> None) |
12854 | 356 |
| This |
357 |
\<Rightarrow> (if mode=Static then None else Some a')) |
|
358 |
in set_lvars l (if mode = Static then x else np a' x,s)" |
|
359 |
||
360 |
||
361 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
362 |
lemma init_lvars_def2: --{* better suited for simplification *} |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
363 |
"init_lvars G C sig mode a' pvs (x,s) = |
12854 | 364 |
set_lvars |
365 |
(\<lambda> k. |
|
366 |
(case k of |
|
367 |
EName e |
|
368 |
\<Rightarrow> (case e of |
|
369 |
VNam v |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
370 |
\<Rightarrow> (empty ((pars (mthd (the (methd G C sig))))[\<mapsto>]pvs)) v |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
371 |
| Res \<Rightarrow> None) |
12854 | 372 |
| This |
373 |
\<Rightarrow> (if mode=Static then None else Some a'))) |
|
374 |
(if mode = Static then x else np a' x,s)" |
|
375 |
apply (unfold init_lvars_def) |
|
376 |
apply (simp (no_asm) add: Let_def) |
|
377 |
done |
|
378 |
||
379 |
constdefs |
|
380 |
body :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> expr" |
|
381 |
"body G C sig \<equiv> let m = the (methd G C sig) |
|
382 |
in Body (declclass m) (stmt (mbody (mthd m)))" |
|
383 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
384 |
lemma body_def2: --{* better suited for simplification *} |
12854 | 385 |
"body G C sig = Body (declclass (the (methd G C sig))) |
386 |
(stmt (mbody (mthd (the (methd G C sig)))))" |
|
387 |
apply (unfold body_def Let_def) |
|
388 |
apply auto |
|
389 |
done |
|
390 |
||
391 |
section "variables" |
|
392 |
||
393 |
constdefs |
|
394 |
||
395 |
lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar" |
|
396 |
"lvar vn s \<equiv> (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))" |
|
397 |
||
398 |
fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" |
|
399 |
"fvar C stat fn a' s |
|
400 |
\<equiv> let (oref,xf) = if stat then (Stat C,id) |
|
401 |
else (Heap (the_Addr a'),np a'); |
|
402 |
n = Inl (fn,C); |
|
403 |
f = (\<lambda>v. supd (upd_gobj oref n v)) |
|
404 |
in ((the (values (the (globs (store s) oref)) n),f),abupd xf s)" |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
405 |
|
12854 | 406 |
avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" |
407 |
"avar G i' a' s |
|
408 |
\<equiv> let oref = Heap (the_Addr a'); |
|
409 |
i = the_Intg i'; |
|
410 |
n = Inr i; |
|
411 |
(T,k,cs) = the_Arr (globs (store s) oref); |
|
412 |
f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T) |
|
413 |
ArrStore x |
|
414 |
,upd_gobj oref n v s)) |
|
415 |
in ((the (cs n),f) |
|
416 |
,abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s)" |
|
417 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
418 |
lemma fvar_def2: --{* better suited for simplification *} |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
419 |
"fvar C stat fn a' s = |
12854 | 420 |
((the |
421 |
(values |
|
422 |
(the (globs (store s) (if stat then Stat C else Heap (the_Addr a')))) |
|
423 |
(Inl (fn,C))) |
|
424 |
,(\<lambda>v. supd (upd_gobj (if stat then Stat C else Heap (the_Addr a')) |
|
425 |
(Inl (fn,C)) |
|
426 |
v))) |
|
427 |
,abupd (if stat then id else np a') s) |
|
428 |
" |
|
429 |
apply (unfold fvar_def) |
|
430 |
apply (simp (no_asm) add: Let_def split_beta) |
|
431 |
done |
|
432 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
433 |
lemma avar_def2: --{* better suited for simplification *} |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
434 |
"avar G i' a' s = |
12854 | 435 |
((the ((snd(snd(the_Arr (globs (store s) (Heap (the_Addr a')))))) |
436 |
(Inr (the_Intg i'))) |
|
437 |
,(\<lambda>v (x,s'). (raise_if (\<not>G,s'\<turnstile>v fits (fst(the_Arr (globs (store s) |
|
438 |
(Heap (the_Addr a')))))) |
|
439 |
ArrStore x |
|
440 |
,upd_gobj (Heap (the_Addr a')) |
|
441 |
(Inr (the_Intg i')) v s'))) |
|
442 |
,abupd (raise_if (\<not>(the_Intg i') in_bounds (fst(snd(the_Arr (globs (store s) |
|
443 |
(Heap (the_Addr a'))))))) IndOutBound \<circ> np a') |
|
444 |
s)" |
|
445 |
apply (unfold avar_def) |
|
446 |
apply (simp (no_asm) add: Let_def split_beta) |
|
447 |
done |
|
448 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
449 |
constdefs |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
450 |
check_field_access:: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
451 |
"prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> vname \<Rightarrow> bool \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
452 |
"check_field_access G accC statDeclC fn stat a' s |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
453 |
\<equiv> let oref = if stat then Stat statDeclC |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
454 |
else Heap (the_Addr a'); |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
455 |
dynC = case oref of |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
456 |
Heap a \<Rightarrow> obj_class (the (globs (store s) oref)) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
457 |
| Stat C \<Rightarrow> C; |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
458 |
f = (the (table_of (DeclConcepts.fields G dynC) (fn,statDeclC))) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
459 |
in abupd |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
460 |
(error_if (\<not> G\<turnstile>Field fn (statDeclC,f) in dynC dyn_accessible_from accC) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
461 |
AccessViolation) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
462 |
s" |
12854 | 463 |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
464 |
constdefs |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
465 |
check_method_access:: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
466 |
"prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> inv_mode \<Rightarrow> sig \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
467 |
"check_method_access G accC statT mode sig a' s |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
468 |
\<equiv> let invC = invocation_class mode (store s) a' statT; |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
469 |
dynM = the (dynlookup G statT invC sig) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
470 |
in abupd |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
471 |
(error_if (\<not> G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
472 |
AccessViolation) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
473 |
s" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
474 |
|
12854 | 475 |
section "evaluation judgments" |
476 |
||
477 |
consts |
|
478 |
eval :: "prog \<Rightarrow> (state \<times> term \<times> vals \<times> state) set" |
|
479 |
halloc:: "prog \<Rightarrow> (state \<times> obj_tag \<times> loc \<times> state) set" |
|
480 |
sxalloc:: "prog \<Rightarrow> (state \<times> state) set" |
|
481 |
||
482 |
||
483 |
syntax |
|
484 |
eval ::"[prog,state,term,vals*state]=>bool"("_|-_ -_>-> _" [61,61,80, 61]60) |
|
485 |
exec ::"[prog,state,stmt ,state]=>bool"("_|-_ -_-> _" [61,61,65, 61]60) |
|
486 |
evar ::"[prog,state,var ,vvar,state]=>bool"("_|-_ -_=>_-> _"[61,61,90,61,61]60) |
|
487 |
eval_::"[prog,state,expr ,val, state]=>bool"("_|-_ -_->_-> _"[61,61,80,61,61]60) |
|
488 |
evals::"[prog,state,expr list , |
|
489 |
val list ,state]=>bool"("_|-_ -_#>_-> _"[61,61,61,61,61]60) |
|
490 |
hallo::"[prog,state,obj_tag, |
|
491 |
loc,state]=>bool"("_|-_ -halloc _>_-> _"[61,61,61,61,61]60) |
|
492 |
sallo::"[prog,state ,state]=>bool"("_|-_ -sxalloc-> _"[61,61, 61]60) |
|
493 |
||
494 |
syntax (xsymbols) |
|
495 |
eval ::"[prog,state,term,vals\<times>state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> _" [61,61,80, 61]60) |
|
496 |
exec ::"[prog,state,stmt ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _" [61,61,65, 61]60) |
|
497 |
evar ::"[prog,state,var ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60) |
|
498 |
eval_::"[prog,state,expr ,val ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_-\<succ>_\<rightarrow> _"[61,61,80,61,61]60) |
|
499 |
evals::"[prog,state,expr list , |
|
500 |
val list ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<rightarrow> _"[61,61,61,61,61]60) |
|
501 |
hallo::"[prog,state,obj_tag, |
|
502 |
loc,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60) |
|
503 |
sallo::"[prog,state, state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61, 61]60) |
|
504 |
||
505 |
translations |
|
506 |
"G\<turnstile>s \<midarrow>t \<succ>\<rightarrow> w___s' " == "(s,t,w___s') \<in> eval G" |
|
507 |
"G\<turnstile>s \<midarrow>t \<succ>\<rightarrow> (w, s')" <= "(s,t,w, s') \<in> eval G" |
|
508 |
"G\<turnstile>s \<midarrow>t \<succ>\<rightarrow> (w,x,s')" <= "(s,t,w,x,s') \<in> eval G" |
|
509 |
"G\<turnstile>s \<midarrow>c \<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>,x,s')" |
|
510 |
"G\<turnstile>s \<midarrow>c \<rightarrow> s' " == "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit> , s')" |
|
511 |
"G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,x,s')" |
|
512 |
"G\<turnstile>s \<midarrow>e-\<succ>v \<rightarrow> s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v , s')" |
|
513 |
"G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In2 e\<succ>\<rightarrow> (In2 vf,x,s')" |
|
514 |
"G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow> s' " == "G\<turnstile>s \<midarrow>In2 e\<succ>\<rightarrow> (In2 vf, s')" |
|
515 |
"G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In3 e\<succ>\<rightarrow> (In3 v ,x,s')" |
|
516 |
"G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow> s' " == "G\<turnstile>s \<midarrow>In3 e\<succ>\<rightarrow> (In3 v , s')" |
|
517 |
"G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s')" <= "(s,oi,a,x,s') \<in> halloc G" |
|
518 |
"G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow> s' " == "(s,oi,a, s') \<in> halloc G" |
|
519 |
"G\<turnstile>s \<midarrow>sxalloc\<rightarrow> (x,s')" <= "(s ,x,s') \<in> sxalloc G" |
|
520 |
"G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' " == "(s , s') \<in> sxalloc G" |
|
521 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
522 |
inductive "halloc G" intros --{* allocating objects on the heap, cf. 12.5 *} |
12854 | 523 |
|
524 |
Abrupt: |
|
525 |
"G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>arbitrary\<rightarrow> (Some x,s)" |
|
526 |
||
527 |
New: "\<lbrakk>new_Addr (heap s) = Some a; |
|
528 |
(x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi) |
|
529 |
else (Some (Xcpt (Loc a)),CInst (SXcpt OutOfMemory)))\<rbrakk> |
|
530 |
\<Longrightarrow> |
|
531 |
G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)" |
|
532 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
533 |
inductive "sxalloc G" intros --{* allocating exception objects for |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
534 |
standard exceptions (other than OutOfMemory) *} |
12854 | 535 |
|
536 |
Norm: "G\<turnstile> Norm s \<midarrow>sxalloc\<rightarrow> Norm s" |
|
537 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
538 |
Jmp: "G\<turnstile>(Some (Jump j), s) \<midarrow>sxalloc\<rightarrow> (Some (Jump j), s)" |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
539 |
|
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
540 |
Error: "G\<turnstile>(Some (Error e), s) \<midarrow>sxalloc\<rightarrow> (Some (Error e), s)" |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
541 |
|
12854 | 542 |
XcptL: "G\<turnstile>(Some (Xcpt (Loc a) ),s) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s)" |
543 |
||
544 |
SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow> |
|
545 |
G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)" |
|
546 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
547 |
|
12854 | 548 |
inductive "eval G" intros |
549 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
550 |
--{* propagation of abrupt completion *} |
12854 | 551 |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
552 |
--{* cf. 14.1, 15.5 *} |
12854 | 553 |
Abrupt: |
554 |
"G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s))" |
|
555 |
||
556 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
557 |
--{* execution of statements *} |
12854 | 558 |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
559 |
--{* cf. 14.5 *} |
12854 | 560 |
Skip: "G\<turnstile>Norm s \<midarrow>Skip\<rightarrow> Norm s" |
561 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
562 |
--{* cf. 14.7 *} |
12854 | 563 |
Expr: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow> |
564 |
G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1" |
|
565 |
||
566 |
Lab: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow> |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
567 |
G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb l) s1" |
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
568 |
--{* cf. 14.2 *} |
12854 | 569 |
Comp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1; |
570 |
G\<turnstile> s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow> |
|
571 |
G\<turnstile>Norm s0 \<midarrow>c1;; c2\<rightarrow> s2" |
|
572 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
573 |
--{* cf. 14.8.2 *} |
12854 | 574 |
If: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1; |
575 |
G\<turnstile> s1\<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<rbrakk> \<Longrightarrow> |
|
576 |
G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<rightarrow> s2" |
|
577 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
578 |
--{* cf. 14.10, 14.10.1 *} |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
579 |
|
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
580 |
--{* A continue jump from the while body @{term c} is handled by |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
581 |
this rule. If a continue jump with the proper label was invoked inside |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
582 |
@{term c} this label (Cont l) is deleted out of the abrupt component of |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
583 |
the state before the iterative evaluation of the while statement. |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
584 |
A break jump is handled by the Lab Statement @{text "Lab l (while\<dots>)"}. |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
585 |
*} |
12854 | 586 |
Loop: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<rightarrow> s1; |
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
587 |
if the_Bool b |
12854 | 588 |
then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> |
589 |
G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3) |
|
590 |
else s3 = s1\<rbrakk> \<Longrightarrow> |
|
591 |
G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3" |
|
592 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
593 |
Jmp: "G\<turnstile>Norm s \<midarrow>Jmp j\<rightarrow> (Some (Jump j), s)" |
12854 | 594 |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
595 |
--{* cf. 14.16 *} |
12854 | 596 |
Throw: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1\<rbrakk> \<Longrightarrow> |
597 |
G\<turnstile>Norm s0 \<midarrow>Throw e\<rightarrow> abupd (throw a') s1" |
|
598 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
599 |
--{* cf. 14.18.1 *} |
12854 | 600 |
Try: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; |
601 |
if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2\<rbrakk> \<Longrightarrow> |
|
602 |
G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(C vn) c2\<rightarrow> s3" |
|
603 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
604 |
--{* cf. 14.18.2 *} |
12854 | 605 |
Fin: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1); |
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
606 |
G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2; |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
607 |
s3=(if (\<exists> err. x1=Some (Error err)) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
608 |
then (x1,s1) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
609 |
else abupd (abrupt_if (x1\<noteq>None) x1) s2) \<rbrakk> |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
610 |
\<Longrightarrow> |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
611 |
G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> s3" |
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
612 |
--{* cf. 12.4.2, 8.5 *} |
12854 | 613 |
Init: "\<lbrakk>the (class G C) = c; |
614 |
if inited C (globs s0) then s3 = Norm s0 |
|
615 |
else (G\<turnstile>Norm (init_class_obj G C s0) |
|
616 |
\<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and> |
|
617 |
G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk> |
|
618 |
\<Longrightarrow> |
|
619 |
G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3" |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
620 |
--{* This class initialisation rule is a little bit inaccurate. Look at the |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
621 |
exact sequence: |
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
622 |
(1) The current class object (the static fields) are initialised |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
623 |
(@{text init_class_obj}), |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
624 |
(2) the superclasses are initialised, |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
625 |
(3) the static initialiser of the current class is invoked. |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
626 |
More precisely we should expect another ordering, namely 2 1 3. |
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
627 |
But we can't just naively toggle 1 and 2. By calling |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
628 |
@{text init_class_obj} |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
629 |
before initialising the superclasses, we also implicitly record that |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
630 |
we have started to initialise the current class (by setting an |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
631 |
value for the class object). This becomes |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
632 |
crucial for the completeness proof of the axiomatic semantics |
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
633 |
@{text "AxCompl.thy"}. Static initialisation requires an induction on |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
634 |
the number of classes not yet initialised (or to be more precise, |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
635 |
classes were the initialisation has not yet begun). |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
636 |
So we could first assign a dummy value to the class before |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
637 |
superclass initialisation and afterwards set the correct values. |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
638 |
But as long as we don't take memory overflow into account |
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
639 |
when allocating class objects, we can leave things as they are for |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
640 |
convenience. |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
641 |
*} |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
642 |
--{* evaluation of expressions *} |
12854 | 643 |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
644 |
--{* cf. 15.8.1, 12.4.1 *} |
12854 | 645 |
NewC: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1; |
646 |
G\<turnstile> s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow> |
|
647 |
G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<rightarrow> s2" |
|
648 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
649 |
--{* cf. 15.9.1, 12.4.1 *} |
12854 | 650 |
NewA: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<rightarrow> s2; |
651 |
G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow> |
|
652 |
G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<rightarrow> s3" |
|
653 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
654 |
--{* cf. 15.15 *} |
12854 | 655 |
Cast: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1; |
656 |
s2 = abupd (raise_if (\<not>G,store s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow> |
|
657 |
G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<rightarrow> s2" |
|
658 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
659 |
--{* cf. 15.19.2 *} |
12854 | 660 |
Inst: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1; |
661 |
b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow> |
|
662 |
G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<rightarrow> s1" |
|
663 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
664 |
--{* cf. 15.7.1 *} |
12854 | 665 |
Lit: "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<rightarrow> Norm s" |
666 |
||
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
667 |
UnOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<rightarrow> s1\<rbrakk> |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
668 |
\<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>UnOp unop e-\<succ>(eval_unop unop v)\<rightarrow> s1" |
13384 | 669 |
|
670 |
BinOp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1; |
|
671 |
G\<turnstile>s1 \<midarrow>(if need_second_arg binop v1 then (In1l e2) else (In1r Skip)) |
|
672 |
\<succ>\<rightarrow> (In1 v2,s2) |
|
673 |
\<rbrakk> |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
674 |
\<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s2" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
675 |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
676 |
--{* cf. 15.10.2 *} |
12854 | 677 |
Super: "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<rightarrow> Norm s" |
678 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
679 |
--{* cf. 15.2 *} |
12854 | 680 |
Acc: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<rightarrow> s1\<rbrakk> \<Longrightarrow> |
681 |
G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<rightarrow> s1" |
|
682 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
683 |
--{* cf. 15.25.1 *} |
12854 | 684 |
Ass: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<rightarrow> s1; |
685 |
G\<turnstile> s1 \<midarrow>e-\<succ>v \<rightarrow> s2\<rbrakk> \<Longrightarrow> |
|
686 |
G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<rightarrow> assign f v s2" |
|
687 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
688 |
--{* cf. 15.24 *} |
12854 | 689 |
Cond: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<rightarrow> s1; |
690 |
G\<turnstile> s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow> |
|
691 |
G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<rightarrow> s2" |
|
692 |
||
693 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
694 |
-- {* The interplay of @{term Call}, @{term Methd} and @{term Body}: |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
695 |
Method invocation is split up into these three rules: |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
696 |
\begin{itemize} |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
697 |
\item [@{term Call}] Calculates the target address and evaluates the |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
698 |
arguments of the method, and then performs dynamic |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
699 |
or static lookup of the method, corresponding to the |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
700 |
call mode. Then the @{term Methd} rule is evaluated |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
701 |
on the calculated declaration class of the method |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
702 |
invocation. |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
703 |
\item [@{term Methd}] A syntactic bridge for the folded method body. |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
704 |
It is used by the axiomatic semantics to add the |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
705 |
proper hypothesis for recursive calls of the method. |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
706 |
\item [@{term Body}] An extra syntactic entity for the unfolded method |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
707 |
body was introduced to properly trigger class |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
708 |
initialisation. Without class initialisation we |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
709 |
could just evaluate the body statement. |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
710 |
\end{itemize} |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
711 |
*} |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
712 |
--{* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5 *} |
12854 | 713 |
Call: |
714 |
"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2; |
|
715 |
D = invocation_declclass G mode (store s2) a' 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:
12919
diff
changeset
|
716 |
s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2; |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
717 |
s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3; |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
718 |
G\<turnstile>s3' \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ>v\<rightarrow> s4\<rbrakk> |
12854 | 719 |
\<Longrightarrow> |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
720 |
G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)-\<succ>v\<rightarrow> (restore_lvars s2 s4)" |
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
721 |
--{* The accessibility check is after @{term init_lvars}, to keep it simple. |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
722 |
@{term init_lvars} already tests for the absence of a null-pointer |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
723 |
reference in case of an instance method invocation. |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
724 |
*} |
12854 | 725 |
|
726 |
Methd: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig-\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow> |
|
727 |
G\<turnstile>Norm s0 \<midarrow>Methd D sig-\<succ>v\<rightarrow> s1" |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
728 |
|
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
729 |
Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2; |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
730 |
s3 = (if (\<exists> l. abrupt s2 = Some (Jump (Break l)) \<or> |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
731 |
abrupt s2 = Some (Jump (Cont l))) |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
732 |
then abupd (\<lambda> x. Some (Error CrossMethodJump)) s2 |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
733 |
else s2)\<rbrakk> \<Longrightarrow> |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
734 |
G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>the (locals (store s2) Result) |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
735 |
\<rightarrow>abupd (absorb Ret) s3" |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
736 |
--{* cf. 14.15, 12.4.1 *} |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
737 |
--{* We filter out a break/continue in @{term s2}, so that we can proof |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
738 |
definite assignment |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
739 |
correct, without the need of conformance of the state. By this the |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
740 |
different parts of the typesafety proof can be disentangled a little. *} |
12854 | 741 |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
742 |
--{* evaluation of variables *} |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
743 |
|
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
744 |
--{* cf. 15.13.1, 15.7.2 *} |
12854 | 745 |
LVar: "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<rightarrow> Norm s" |
746 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
747 |
--{* cf. 15.10.1, 12.4.1 *} |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
748 |
FVar: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a\<rightarrow> s2; |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
749 |
(v,s2') = fvar statDeclC stat fn a s2; |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
750 |
s3 = check_field_access G accC statDeclC fn stat a s2' \<rbrakk> \<Longrightarrow> |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
751 |
G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<rightarrow> s3" |
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
752 |
--{* The accessibility check is after @{term fvar}, to keep it simple. |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
753 |
@{term fvar} already tests for the absence of a null-pointer reference |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
754 |
in case of an instance field |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
755 |
*} |
12854 | 756 |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
757 |
--{* cf. 15.12.1, 15.25.1 *} |
12854 | 758 |
AVar: "\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<rightarrow> s2; |
759 |
(v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow> |
|
760 |
G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<rightarrow> s2'" |
|
761 |
||
762 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
763 |
--{* evaluation of expression lists *} |
12854 | 764 |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
765 |
--{* cf. 15.11.4.2 *} |
12854 | 766 |
Nil: |
767 |
"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<rightarrow> Norm s0" |
|
768 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
769 |
--{* cf. 15.6.4 *} |
12854 | 770 |
Cons: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<rightarrow> s1; |
771 |
G\<turnstile> s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2\<rbrakk> \<Longrightarrow> |
|
772 |
G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2" |
|
773 |
||
774 |
(* Rearrangement of premisses: |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
775 |
[0,1(Abrupt),2(Skip),8(Jmp),4(Lab),30(Nil),31(Cons),27(LVar),17(Cast),18(Inst), |
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
776 |
17(Lit),18(UnOp),19(BinOp),20(Super),21(Acc),3(Expr),5(Comp),25(Methd),26(Body),23(Cond),6(If), |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
777 |
7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),22(Ass),10(Try),28(FVar), |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
778 |
29(AVar),24(Call)] |
12854 | 779 |
*) |
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
780 |
|
12854 | 781 |
ML {* |
782 |
bind_thm ("eval_induct_", rearrange_prems |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
783 |
[0,1,2,8,4,30,31,27,15,16, |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
784 |
17,18,19,20,21,3,5,25,26,23,6, |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
785 |
7,11,9,13,14,12,22,10,28, |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
786 |
29,24] (thm "eval.induct")) |
12854 | 787 |
*} |
788 |
||
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
789 |
|
12854 | 790 |
lemmas eval_induct = eval_induct_ [split_format and and and and and and and and |
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
791 |
and and and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
792 |
and and |
12854 | 793 |
s2 (* Fin *) and and s2 (* NewC *)] |
794 |
||
795 |
declare split_if [split del] split_if_asm [split del] |
|
796 |
option.split [split del] option.split_asm [split del] |
|
797 |
inductive_cases halloc_elim_cases: |
|
798 |
"G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'" |
|
799 |
"G\<turnstile>(Norm s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'" |
|
800 |
||
801 |
inductive_cases sxalloc_elim_cases: |
|
802 |
"G\<turnstile> Norm s \<midarrow>sxalloc\<rightarrow> s'" |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
803 |
"G\<turnstile>(Some (Jump j),s) \<midarrow>sxalloc\<rightarrow> s'" |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
804 |
"G\<turnstile>(Some (Error e),s) \<midarrow>sxalloc\<rightarrow> s'" |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
805 |
"G\<turnstile>(Some (Xcpt (Loc a )),s) \<midarrow>sxalloc\<rightarrow> s'" |
12854 | 806 |
"G\<turnstile>(Some (Xcpt (Std xn)),s) \<midarrow>sxalloc\<rightarrow> s'" |
807 |
inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'" |
|
808 |
||
809 |
lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'; |
|
810 |
\<And>s. \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P; |
|
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
811 |
\<And>j s. \<lbrakk>s' = (Some (Jump j),s)\<rbrakk> \<Longrightarrow> P; |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
812 |
\<And>e s. \<lbrakk>s' = (Some (Error e),s)\<rbrakk> \<Longrightarrow> P; |
12854 | 813 |
\<And>a s. \<lbrakk>s' = (Some (Xcpt (Loc a)),s)\<rbrakk> \<Longrightarrow> P |
814 |
\<rbrakk> \<Longrightarrow> P" |
|
815 |
apply cut_tac |
|
816 |
apply (erule sxalloc_cases) |
|
817 |
apply blast+ |
|
818 |
done |
|
819 |
||
820 |
declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *) |
|
821 |
declare split_paired_All [simp del] split_paired_Ex [simp del] |
|
822 |
ML_setup {* |
|
17876 | 823 |
change_simpset (fn ss => ss delloop "split_all_tac"); |
12854 | 824 |
*} |
825 |
inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'" |
|
826 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
827 |
inductive_cases eval_elim_cases [cases set]: |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
828 |
"G\<turnstile>(Some xc,s) \<midarrow>t \<succ>\<rightarrow> vs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
829 |
"G\<turnstile>Norm s \<midarrow>In1r Skip \<succ>\<rightarrow> xs'" |
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
830 |
"G\<turnstile>Norm s \<midarrow>In1r (Jmp j) \<succ>\<rightarrow> xs'" |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
831 |
"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c) \<succ>\<rightarrow> xs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
832 |
"G\<turnstile>Norm s \<midarrow>In3 ([]) \<succ>\<rightarrow> vs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
833 |
"G\<turnstile>Norm s \<midarrow>In3 (e#es) \<succ>\<rightarrow> vs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
834 |
"G\<turnstile>Norm s \<midarrow>In1l (Lit w) \<succ>\<rightarrow> vs'" |
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
835 |
"G\<turnstile>Norm s \<midarrow>In1l (UnOp unop e) \<succ>\<rightarrow> vs'" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
836 |
"G\<turnstile>Norm s \<midarrow>In1l (BinOp binop e1 e2) \<succ>\<rightarrow> vs'" |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
837 |
"G\<turnstile>Norm s \<midarrow>In2 (LVar vn) \<succ>\<rightarrow> vs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
838 |
"G\<turnstile>Norm s \<midarrow>In1l (Cast T e) \<succ>\<rightarrow> vs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
839 |
"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T) \<succ>\<rightarrow> vs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
840 |
"G\<turnstile>Norm s \<midarrow>In1l (Super) \<succ>\<rightarrow> vs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
841 |
"G\<turnstile>Norm s \<midarrow>In1l (Acc va) \<succ>\<rightarrow> vs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
842 |
"G\<turnstile>Norm s \<midarrow>In1r (Expr e) \<succ>\<rightarrow> xs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
843 |
"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2) \<succ>\<rightarrow> xs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
844 |
"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig) \<succ>\<rightarrow> xs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
845 |
"G\<turnstile>Norm s \<midarrow>In1l (Body D c) \<succ>\<rightarrow> xs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
846 |
"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2) \<succ>\<rightarrow> vs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
847 |
"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2) \<succ>\<rightarrow> xs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
848 |
"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c) \<succ>\<rightarrow> xs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
849 |
"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2) \<succ>\<rightarrow> xs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
850 |
"G\<turnstile>Norm s \<midarrow>In1r (Throw e) \<succ>\<rightarrow> xs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
851 |
"G\<turnstile>Norm s \<midarrow>In1l (NewC C) \<succ>\<rightarrow> vs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
852 |
"G\<turnstile>Norm s \<midarrow>In1l (New T[e]) \<succ>\<rightarrow> vs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
853 |
"G\<turnstile>Norm s \<midarrow>In1l (Ass va e) \<succ>\<rightarrow> vs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
854 |
"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2) \<succ>\<rightarrow> xs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
855 |
"G\<turnstile>Norm s \<midarrow>In2 ({accC,statDeclC,stat}e..fn) \<succ>\<rightarrow> vs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
856 |
"G\<turnstile>Norm s \<midarrow>In2 (e1.[e2]) \<succ>\<rightarrow> vs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
857 |
"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<rightarrow> vs'" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
858 |
"G\<turnstile>Norm s \<midarrow>In1r (Init C) \<succ>\<rightarrow> xs'" |
12854 | 859 |
declare not_None_eq [simp] (* IntDef.Zero_def [simp] *) |
860 |
declare split_paired_All [simp] split_paired_Ex [simp] |
|
861 |
ML_setup {* |
|
17876 | 862 |
change_simpset (fn ss => ss addloop ("split_all_tac", split_all_tac)); |
12854 | 863 |
*} |
864 |
declare split_if [split] split_if_asm [split] |
|
865 |
option.split [split] option.split_asm [split] |
|
866 |
||
867 |
lemma eval_Inj_elim: |
|
868 |
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') |
|
869 |
\<Longrightarrow> case t of |
|
870 |
In1 ec \<Rightarrow> (case ec of |
|
871 |
Inl e \<Rightarrow> (\<exists>v. w = In1 v) |
|
872 |
| Inr c \<Rightarrow> w = \<diamondsuit>) |
|
873 |
| In2 e \<Rightarrow> (\<exists>v. w = In2 v) |
|
874 |
| In3 e \<Rightarrow> (\<exists>v. w = In3 v)" |
|
875 |
apply (erule eval_cases) |
|
876 |
apply auto |
|
877 |
apply (induct_tac "t") |
|
878 |
apply (induct_tac "a") |
|
879 |
apply auto |
|
880 |
done |
|
881 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
882 |
text {* The following simplification procedures set up the proper injections of |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
883 |
terms and their corresponding values in the evaluation relation: |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
884 |
E.g. an expression |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
885 |
(injection @{term In1l} into terms) always evaluates to ordinary values |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
886 |
(injection @{term In1} into generalised values @{term vals}). |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
887 |
*} |
12854 | 888 |
ML_setup {* |
889 |
fun eval_fun nam inj rhs = |
|
890 |
let |
|
891 |
val name = "eval_" ^ nam ^ "_eq" |
|
892 |
val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<rightarrow> (w, s')" |
|
893 |
val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") |
|
894 |
(K [Auto_tac, ALLGOALS (ftac (thm "eval_Inj_elim")) THEN Auto_tac]) |
|
895 |
fun is_Inj (Const (inj,_) $ _) = true |
|
896 |
| is_Inj _ = false |
|
897 |
fun pred (_ $ (Const ("Pair",_) $ _ $ |
|
898 |
(Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ ))) $ _ ) = is_Inj x |
|
899 |
in |
|
13462 | 900 |
cond_simproc name lhs pred (thm name) |
12854 | 901 |
end |
902 |
||
903 |
val eval_expr_proc =eval_fun "expr" "In1l" "\<exists>v. w=In1 v \<and> G\<turnstile>s \<midarrow>t-\<succ>v \<rightarrow> s'" |
|
904 |
val eval_var_proc =eval_fun "var" "In2" "\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<rightarrow> s'" |
|
905 |
val eval_exprs_proc=eval_fun "exprs""In3" "\<exists>vs. w=In3 vs \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<rightarrow> s'" |
|
906 |
val eval_stmt_proc =eval_fun "stmt" "In1r" " w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<rightarrow> s'"; |
|
907 |
Addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc]; |
|
908 |
bind_thms ("AbruptIs", sum3_instantiate (thm "eval.Abrupt")) |
|
909 |
*} |
|
910 |
||
911 |
declare halloc.Abrupt [intro!] eval.Abrupt [intro!] AbruptIs [intro!] |
|
912 |
||
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
913 |
text{* @{text Callee},@{text InsInitE}, @{text InsInitV}, @{text FinA} are only |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
914 |
used in smallstep semantics, not in the bigstep semantics. So their is no |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
915 |
valid evaluation of these terms |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
916 |
*} |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
917 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
918 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
919 |
lemma eval_Callee: "G\<turnstile>Norm s\<midarrow>Callee l e-\<succ>v\<rightarrow> s' = False" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
920 |
proof - |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
921 |
{ fix s t v s' |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
922 |
assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
923 |
normal: "normal s" and |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
924 |
callee: "t=In1l (Callee l e)" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
925 |
then have "False" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
926 |
proof (induct) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
927 |
qed (auto) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
928 |
} |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
929 |
then show ?thesis |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
930 |
by (cases s') fastsimp |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
931 |
qed |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
932 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
933 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
934 |
lemma eval_InsInitE: "G\<turnstile>Norm s\<midarrow>InsInitE c e-\<succ>v\<rightarrow> s' = False" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
935 |
proof - |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
936 |
{ fix s t v s' |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
937 |
assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
938 |
normal: "normal s" and |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
939 |
callee: "t=In1l (InsInitE c e)" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
940 |
then have "False" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
941 |
proof (induct) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
942 |
qed (auto) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
943 |
} |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
944 |
then show ?thesis |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
945 |
by (cases s') fastsimp |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
946 |
qed |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
947 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
948 |
lemma eval_InsInitV: "G\<turnstile>Norm s\<midarrow>InsInitV c w=\<succ>v\<rightarrow> s' = False" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
949 |
proof - |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
950 |
{ fix s t v s' |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
951 |
assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
952 |
normal: "normal s" and |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
953 |
callee: "t=In2 (InsInitV c w)" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
954 |
then have "False" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
955 |
proof (induct) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
956 |
qed (auto) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
957 |
} |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
958 |
then show ?thesis |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
959 |
by (cases s') fastsimp |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
960 |
qed |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
961 |
|
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
962 |
lemma eval_FinA: "G\<turnstile>Norm s\<midarrow>FinA a c\<rightarrow> s' = False" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
963 |
proof - |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
964 |
{ fix s t v s' |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
965 |
assume eval: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s')" and |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
966 |
normal: "normal s" and |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
967 |
callee: "t=In1r (FinA a c)" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
968 |
then have "False" |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
969 |
proof (induct) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
970 |
qed (auto) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
971 |
} |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
972 |
then show ?thesis |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
973 |
by (cases s') fastsimp |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
974 |
qed |
12854 | 975 |
|
976 |
lemma eval_no_abrupt_lemma: |
|
977 |
"\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s" |
|
978 |
by (erule eval_cases, auto) |
|
979 |
||
980 |
lemma eval_no_abrupt: |
|
981 |
"G\<turnstile>(x,s) \<midarrow>t\<succ>\<rightarrow> (w,Norm s') = |
|
982 |
(x = None \<and> G\<turnstile>Norm s \<midarrow>t\<succ>\<rightarrow> (w,Norm s'))" |
|
983 |
apply auto |
|
984 |
apply (frule eval_no_abrupt_lemma, auto)+ |
|
985 |
done |
|
986 |
||
987 |
ML {* |
|
988 |
local |
|
12919 | 989 |
fun is_None (Const ("Datatype.option.None",_)) = true |
12854 | 990 |
| is_None _ = false |
991 |
fun pred (t as (_ $ (Const ("Pair",_) $ |
|
992 |
(Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x |
|
993 |
in |
|
994 |
val eval_no_abrupt_proc = |
|
13462 | 995 |
cond_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred |
12854 | 996 |
(thm "eval_no_abrupt") |
997 |
end; |
|
998 |
Addsimprocs [eval_no_abrupt_proc] |
|
999 |
*} |
|
1000 |
||
1001 |
||
1002 |
lemma eval_abrupt_lemma: |
|
1003 |
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = arbitrary3 t" |
|
1004 |
by (erule eval_cases, auto) |
|
1005 |
||
1006 |
lemma eval_abrupt: |
|
1007 |
" G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (w,s') = |
|
1008 |
(s'=(Some xc,s) \<and> w=arbitrary3 t \<and> |
|
1009 |
G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s)))" |
|
1010 |
apply auto |
|
1011 |
apply (frule eval_abrupt_lemma, auto)+ |
|
1012 |
done |
|
1013 |
||
1014 |
ML {* |
|
1015 |
local |
|
12919 | 1016 |
fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true |
12854 | 1017 |
| is_Some _ = false |
1018 |
fun pred (_ $ (Const ("Pair",_) $ |
|
1019 |
_ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $ |
|
1020 |
x))) $ _ ) = is_Some x |
|
1021 |
in |
|
1022 |
val eval_abrupt_proc = |
|
13462 | 1023 |
cond_simproc "eval_abrupt" |
12854 | 1024 |
"G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred (thm "eval_abrupt") |
1025 |
end; |
|
1026 |
Addsimprocs [eval_abrupt_proc] |
|
1027 |
*} |
|
1028 |
||
1029 |
||
1030 |
lemma LitI: "G\<turnstile>s \<midarrow>Lit v-\<succ>(if normal s then v else arbitrary)\<rightarrow> s" |
|
1031 |
apply (case_tac "s", case_tac "a = None") |
|
1032 |
by (auto intro!: eval.Lit) |
|
1033 |
||
1034 |
lemma SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s" |
|
1035 |
apply (case_tac "s", case_tac "a = None") |
|
1036 |
by (auto intro!: eval.Skip) |
|
1037 |
||
1038 |
lemma ExprI: "G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<rightarrow> s'" |
|
1039 |
apply (case_tac "s", case_tac "a = None") |
|
1040 |
by (auto intro!: eval.Expr) |
|
1041 |
||
1042 |
lemma CompI: "\<lbrakk>G\<turnstile>s \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>c1;; c2\<rightarrow> s2" |
|
1043 |
apply (case_tac "s", case_tac "a = None") |
|
1044 |
by (auto intro!: eval.Comp) |
|
1045 |
||
1046 |
lemma CondI: |
|
1047 |
"\<And>s1. \<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>b\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow> |
|
1048 |
G\<turnstile>s \<midarrow>e ? e1 : e2-\<succ>(if normal s1 then v else arbitrary)\<rightarrow> s2" |
|
1049 |
apply (case_tac "s", case_tac "a = None") |
|
1050 |
by (auto intro!: eval.Cond) |
|
1051 |
||
1052 |
lemma IfI: "\<lbrakk>G\<turnstile>s \<midarrow>e-\<succ>v\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool v then c1 else c2)\<rightarrow> s2\<rbrakk> |
|
1053 |
\<Longrightarrow> G\<turnstile>s \<midarrow>If(e) c1 Else c2\<rightarrow> s2" |
|
1054 |
apply (case_tac "s", case_tac "a = None") |
|
1055 |
by (auto intro!: eval.If) |
|
1056 |
||
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
1057 |
lemma MethdI: "G\<turnstile>s \<midarrow>body G C sig-\<succ>v\<rightarrow> s' |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
1058 |
\<Longrightarrow> G\<turnstile>s \<midarrow>Methd C sig-\<succ>v\<rightarrow> s'" |
12854 | 1059 |
apply (case_tac "s", case_tac "a = None") |
1060 |
by (auto intro!: eval.Methd) |
|
1061 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
1062 |
lemma eval_Call: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
1063 |
"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2; |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
1064 |
D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
1065 |
s3 = init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' pvs s2; |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
1066 |
s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3; |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
1067 |
G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>-\<succ> v\<rightarrow> s4; |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
1068 |
s4' = restore_lvars s2 s4\<rbrakk> \<Longrightarrow> |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset
|
1069 |
G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}ps)-\<succ>v\<rightarrow> s4'" |
12854 | 1070 |
apply (drule eval.Call, assumption) |
1071 |
apply (rule HOL.refl) |
|
1072 |
apply simp+ |
|
1073 |
done |
|
1074 |
||
1075 |
lemma eval_Init: |
|
1076 |
"\<lbrakk>if inited C (globs s0) then s3 = Norm s0 |
|
1077 |
else G\<turnstile>Norm (init_class_obj G C s0) |
|
1078 |
\<midarrow>(if C = Object then Skip else Init (super (the (class G C))))\<rightarrow> s1 \<and> |
|
1079 |
G\<turnstile>set_lvars empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and> |
|
1080 |
s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow> |
|
1081 |
G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3" |
|
1082 |
apply (rule eval.Init) |
|
1083 |
apply auto |
|
1084 |
done |
|
1085 |
||
1086 |
lemma init_done: "initd C s \<Longrightarrow> G\<turnstile>s \<midarrow>Init C\<rightarrow> s" |
|
1087 |
apply (case_tac "s", simp) |
|
1088 |
apply (case_tac "a") |
|
1089 |
apply safe |
|
1090 |
apply (rule eval_Init) |
|
1091 |
apply auto |
|
1092 |
done |
|
1093 |
||
1094 |
lemma eval_StatRef: |
|
1095 |
"G\<turnstile>s \<midarrow>StatRef rt-\<succ>(if abrupt s=None then Null else arbitrary)\<rightarrow> s" |
|
1096 |
apply (case_tac "s", simp) |
|
1097 |
apply (case_tac "a = None") |
|
1098 |
apply (auto del: eval.Abrupt intro!: eval.intros) |
|
1099 |
done |
|
1100 |
||
1101 |
||
1102 |
lemma SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' \<Longrightarrow> s' = s" |
|
1103 |
apply (erule eval_cases) |
|
1104 |
by auto |
|
1105 |
||
1106 |
lemma Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' = (s = s')" |
|
1107 |
by auto |
|
1108 |
||
1109 |
(*unused*) |
|
1110 |
lemma init_retains_locals [rule_format (no_asm)]: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> |
|
1111 |
(\<forall>C. t=In1r (Init C) \<longrightarrow> locals (store s) = locals (store s'))" |
|
1112 |
apply (erule eval.induct) |
|
1113 |
apply (simp (no_asm_use) split del: split_if_asm option.split_asm)+ |
|
1114 |
apply auto |
|
1115 |
done |
|
1116 |
||
1117 |
lemma halloc_xcpt [dest!]: |
|
1118 |
"\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s' \<Longrightarrow> s'=(Some xc,s)" |
|
1119 |
apply (erule_tac halloc_elim_cases) |
|
1120 |
by auto |
|
1121 |
||
1122 |
(* |
|
1123 |
G\<turnstile>(x,(h,l)) \<midarrow>e\<succ>v\<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This" |
|
1124 |
G\<turnstile>(x,(h,l)) \<midarrow>s \<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This" |
|
1125 |
*) |
|
1126 |
||
1127 |
lemma eval_Methd: |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
1128 |
"G\<turnstile>s \<midarrow>In1l(body G C sig)\<succ>\<rightarrow> (w,s') |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
1129 |
\<Longrightarrow> G\<turnstile>s \<midarrow>In1l(Methd C sig)\<succ>\<rightarrow> (w,s')" |
12854 | 1130 |
apply (case_tac "s") |
1131 |
apply (case_tac "a") |
|
1132 |
apply clarsimp+ |
|
1133 |
apply (erule eval.Methd) |
|
1134 |
apply (drule eval_abrupt_lemma) |
|
1135 |
apply force |
|
1136 |
done |
|
1137 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
1138 |
lemma eval_Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2; |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
1139 |
res=the (locals (store s2) Result); |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
1140 |
s3 = (if (\<exists> l. abrupt s2 = Some (Jump (Break l)) \<or> |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
1141 |
abrupt s2 = Some (Jump (Cont l))) |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
1142 |
then abupd (\<lambda> x. Some (Error CrossMethodJump)) s2 |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
1143 |
else s2); |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
1144 |
s4=abupd (absorb Ret) s3\<rbrakk> \<Longrightarrow> |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
1145 |
G\<turnstile>Norm s0 \<midarrow>Body D c-\<succ>res\<rightarrow>s4" |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
1146 |
by (auto elim: eval.Body) |
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
1147 |
|
13384 | 1148 |
lemma eval_binop_arg2_indep: |
1149 |
"\<not> need_second_arg binop v1 \<Longrightarrow> eval_binop binop v1 x = eval_binop binop v1 y" |
|
1150 |
by (cases binop) |
|
1151 |
(simp_all add: need_second_arg_def) |
|
1152 |
||
1153 |
||
1154 |
lemma eval_BinOp_arg2_indepI: |
|
1155 |
assumes eval_e1: "G\<turnstile>Norm s0 \<midarrow>e1-\<succ>v1\<rightarrow> s1" and |
|
1156 |
no_need: "\<not> need_second_arg binop v1" |
|
1157 |
shows "G\<turnstile>Norm s0 \<midarrow>BinOp binop e1 e2-\<succ>(eval_binop binop v1 v2)\<rightarrow> s1" |
|
1158 |
(is "?EvalBinOp v2") |
|
1159 |
proof - |
|
1160 |
from eval_e1 |
|
1161 |
have "?EvalBinOp Unit" |
|
1162 |
by (rule eval.BinOp) |
|
1163 |
(simp add: no_need) |
|
1164 |
moreover |
|
1165 |
from no_need |
|
1166 |
have "eval_binop binop v1 Unit = eval_binop binop v1 v2" |
|
1167 |
by (simp add: eval_binop_arg2_indep) |
|
1168 |
ultimately |
|
1169 |
show ?thesis |
|
1170 |
by simp |
|
1171 |
qed |
|
1172 |
||
12854 | 1173 |
|
1174 |
section "single valued" |
|
1175 |
||
1176 |
lemma unique_halloc [rule_format (no_asm)]: |
|
1177 |
"\<And>s as as'. (s,oi,as)\<in>halloc G \<Longrightarrow> (s,oi,as')\<in>halloc G \<longrightarrow> as'=as" |
|
1178 |
apply (simp (no_asm_simp) only: split_tupled_all) |
|
1179 |
apply (erule halloc.induct) |
|
1180 |
apply (auto elim!: halloc_elim_cases split del: split_if split_if_asm) |
|
1181 |
apply (drule trans [THEN sym], erule sym) |
|
1182 |
defer |
|
1183 |
apply (drule trans [THEN sym], erule sym) |
|
1184 |
apply auto |
|
1185 |
done |
|
1186 |
||
1187 |
||
1188 |
lemma single_valued_halloc: |
|
1189 |
"single_valued {((s,oi),(a,s')). G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s'}" |
|
1190 |
apply (unfold single_valued_def) |
|
1191 |
by (clarsimp, drule (1) unique_halloc, auto) |
|
1192 |
||
1193 |
||
1194 |
lemma unique_sxalloc [rule_format (no_asm)]: |
|
1195 |
"\<And>s s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'' \<longrightarrow> s'' = s'" |
|
1196 |
apply (simp (no_asm_simp) only: split_tupled_all) |
|
1197 |
apply (erule sxalloc.induct) |
|
1198 |
apply (auto dest: unique_halloc elim!: sxalloc_elim_cases |
|
1199 |
split del: split_if split_if_asm) |
|
1200 |
done |
|
1201 |
||
1202 |
lemma single_valued_sxalloc: "single_valued {(s,s'). G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'}" |
|
1203 |
apply (unfold single_valued_def) |
|
1204 |
apply (blast dest: unique_sxalloc) |
|
1205 |
done |
|
1206 |
||
1207 |
lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p" |
|
1208 |
by auto |
|
1209 |
||
13688
a0b16d42d489
"Definite Assignment Analysis" included, with proof of correctness. Large adjustments of type safety proof and soundness proof of the axiomatic semantics were necessary. Completeness proof of the loop rule of the axiomatic semantic was altered. So the additional polymorphic variants of some rules could be removed.
schirmer
parents:
13601
diff
changeset
|
1210 |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
1211 |
|
12854 | 1212 |
lemma unique_eval [rule_format (no_asm)]: |
1213 |
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)" |
|
1214 |
apply (case_tac "ws") |
|
13601 | 1215 |
apply hypsubst |
12854 | 1216 |
apply (erule eval_induct) |
1217 |
apply (tactic {* ALLGOALS (EVERY' |
|
1218 |
[strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *}) |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
1219 |
(* 31 subgoals *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
1220 |
prefer 28 (* Try *) |
12854 | 1221 |
apply (simp (no_asm_use) only: split add: split_if_asm) |
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
1222 |
(* 34 subgoals *) |
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
1223 |
prefer 30 (* Init *) |
12854 | 1224 |
apply (case_tac "inited C (globs s0)", (simp only: if_True if_False)+) |
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
1225 |
prefer 26 (* While *) |
12854 | 1226 |
apply (simp (no_asm_use) only: split add: split_if_asm, blast) |
1227 |
apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp) |
|
1228 |
apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp) |
|
1229 |
apply blast |
|
13337
f75dfc606ac7
Added unary and binary operations like (+,-,<, ...); Added smallstep semantics (no proofs about it yet).
schirmer
parents:
12925
diff
changeset
|
1230 |
(* 33 subgoals *) |
12854 | 1231 |
apply (blast dest: unique_sxalloc unique_halloc split_pairD)+ |
1232 |
done |
|
1233 |
||
1234 |
(* unused *) |
|
1235 |
lemma single_valued_eval: |
|
1236 |
"single_valued {((s,t),vs'). G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'}" |
|
1237 |
apply (unfold single_valued_def) |
|
1238 |
by (clarify, drule (1) unique_eval, auto) |
|
1239 |
||
1240 |
end |