|
11229
|
1 |
(* Title: HOL/MicroJava/BV/Typing_Framework.thy
|
|
|
2 |
ID: $Id$
|
|
|
3 |
Author: Tobias Nipkow
|
|
|
4 |
Copyright 2000 TUM
|
|
|
5 |
*)
|
|
|
6 |
|
|
12911
|
7 |
header {* \isaheader{Typing and Dataflow Analysis Framework} *}
|
|
11229
|
8 |
|
|
27680
|
9 |
theory Typing_Framework
|
|
|
10 |
imports Listn
|
|
|
11 |
begin
|
|
11229
|
12 |
|
|
|
13 |
text {*
|
|
13224
|
14 |
The relationship between dataflow analysis and a welltyped-instruction predicate.
|
|
11229
|
15 |
*}
|
|
12516
|
16 |
types
|
|
|
17 |
's step_type = "nat \<Rightarrow> 's \<Rightarrow> (nat \<times> 's) list"
|
|
11229
|
18 |
|
|
|
19 |
constdefs
|
|
13006
|
20 |
stable :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> nat \<Rightarrow> bool"
|
|
12516
|
21 |
"stable r step ss p == !(q,s'):set(step p (ss!p)). s' <=_r ss!q"
|
|
11229
|
22 |
|
|
13006
|
23 |
stables :: "'s ord \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
|
|
12516
|
24 |
"stables r step ss == !p<size ss. stable r step ss p"
|
|
11229
|
25 |
|
|
14653
|
26 |
wt_step ::
|
|
|
27 |
"'s ord \<Rightarrow> 's \<Rightarrow> 's step_type \<Rightarrow> 's list \<Rightarrow> bool"
|
|
|
28 |
"wt_step r T step ts ==
|
|
|
29 |
!p<size(ts). ts!p ~= T & stable r step ts p"
|
|
|
30 |
|
|
13006
|
31 |
is_bcv :: "'s ord \<Rightarrow> 's \<Rightarrow> 's step_type
|
|
|
32 |
\<Rightarrow> nat \<Rightarrow> 's set \<Rightarrow> ('s list \<Rightarrow> 's list) \<Rightarrow> bool"
|
|
12516
|
33 |
"is_bcv r T step n A bcv == !ss : list n A.
|
|
11229
|
34 |
(!p<n. (bcv ss)!p ~= T) =
|
|
12516
|
35 |
(? ts: list n A. ss <=[r] ts & wt_step r T step ts)"
|
|
11229
|
36 |
|
|
|
37 |
end
|