| author | blanchet |
| Tue, 03 Aug 2010 14:28:44 +0200 | |
| changeset 38178 | 0cea0125339a |
| parent 35416 | d8d7d1b785af |
| child 42150 | b0c0638c4aad |
| permissions | -rw-r--r-- |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
1 |
(* Title: HOL/MicroJava/BV/Typing_Framework.thy |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
2 |
Author: Tobias Nipkow |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
3 |
Copyright 2000 TUM |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
4 |
*) |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
5 |
|
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
6 |
header {* \isaheader{Typing and Dataflow Analysis Framework} *}
|
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
7 |
|
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
8 |
theory Typing_Framework |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
9 |
imports Listn |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
10 |
begin |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
11 |
|
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
12 |
text {*
|
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
13 |
The relationship between dataflow analysis and a welltyped-instruction predicate. |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
14 |
*} |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
15 |
types |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
16 |
's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list" |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
17 |
|
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
18 |
definition stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool" where |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
19 |
"stable r step ss p == !(q,s'):set(step p (ss!p)). s' <=_r ss!q" |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
20 |
|
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
21 |
definition stables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool" where |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
22 |
"stables r step ss == !p<size ss. stable r step ss p" |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
23 |
|
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
24 |
definition wt_step :: |
|
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
25 |
"'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool" where |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
26 |
"wt_step r T step ts == |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
27 |
!p<size(ts). ts!p ~= T & stable r step ts p" |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
28 |
|
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
29 |
definition is_bcv :: "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type |
|
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
30 |
\<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> ('s list \<Rightarrow> 's list) \<Rightarrow> bool" where
|
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
31 |
"is_bcv r T step n A bcv == !ss : list n A. |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
32 |
(!p<n. (bcv ss)!p ~= T) = |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
33 |
(? ts: list n A. ss <=[r] ts & wt_step r T step ts)" |
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
34 |
|
|
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
diff
changeset
|
35 |
end |