1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 theory Abs_Int_den0 |
|
4 imports Abs_State_den |
|
5 begin |
|
6 |
|
7 subsection "Computable Abstract Interpretation" |
|
8 |
|
9 text{* Abstract interpretation over type @{text astate} instead of |
|
10 functions. *} |
|
11 |
|
12 locale Abs_Int = Val_abs + |
|
13 fixes pfp :: "('a astate \<Rightarrow> 'a astate) \<Rightarrow> 'a astate \<Rightarrow> 'a astate" |
|
14 assumes pfp: "f(pfp f x0) \<sqsubseteq> pfp f x0" |
|
15 assumes above: "x0 \<sqsubseteq> pfp f x0" |
|
16 begin |
|
17 |
|
18 fun aval' :: "aexp \<Rightarrow> 'a astate \<Rightarrow> 'a" where |
|
19 "aval' (N n) _ = num' n" | |
|
20 "aval' (V x) S = lookup S x" | |
|
21 "aval' (Plus e1 e2) S = plus' (aval' e1 S) (aval' e2 S)" |
|
22 |
|
23 abbreviation astate_in_rep (infix "<:" 50) where |
|
24 "s <: S == ALL x. s x <: lookup S x" |
|
25 |
|
26 lemma astate_in_rep_le: "(s::state) <: S \<Longrightarrow> S \<sqsubseteq> T \<Longrightarrow> s <: T" |
|
27 by (metis in_mono le_astate_def le_rep lookup_def top) |
|
28 |
|
29 lemma aval'_sound: "s <: S \<Longrightarrow> aval a s <: aval' a S" |
|
30 by (induct a) (auto simp: rep_num' rep_plus') |
|
31 |
|
32 |
|
33 fun AI :: "com \<Rightarrow> 'a astate \<Rightarrow> 'a astate" where |
|
34 "AI SKIP S = S" | |
|
35 "AI (x ::= a) S = update S x (aval' a S)" | |
|
36 "AI (c1;;c2) S = AI c2 (AI c1 S)" | |
|
37 "AI (IF b THEN c1 ELSE c2) S = (AI c1 S) \<squnion> (AI c2 S)" | |
|
38 "AI (WHILE b DO c) S = pfp (AI c) S" |
|
39 |
|
40 lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> s <: S0 \<Longrightarrow> t <: AI c S0" |
|
41 proof(induction c arbitrary: s t S0) |
|
42 case SKIP thus ?case by fastforce |
|
43 next |
|
44 case Assign thus ?case |
|
45 by (auto simp: lookup_update aval'_sound) |
|
46 next |
|
47 case Seq thus ?case by auto |
|
48 next |
|
49 case If thus ?case |
|
50 by (metis AI.simps(4) IfE astate_in_rep_le join_ge1 join_ge2) |
|
51 next |
|
52 case (While b c) |
|
53 let ?P = "pfp (AI c) S0" |
|
54 { fix s t have "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> s <: ?P \<Longrightarrow> t <: ?P" |
|
55 proof(induction "WHILE b DO c" s t rule: big_step_induct) |
|
56 case WhileFalse thus ?case by simp |
|
57 next |
|
58 case WhileTrue thus ?case using While.IH pfp astate_in_rep_le by metis |
|
59 qed |
|
60 } |
|
61 with astate_in_rep_le[OF `s <: S0` above] |
|
62 show ?case by (metis While(2) AI.simps(5)) |
|
63 qed |
|
64 |
|
65 end |
|
66 |
|
67 end |
|