|
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 theory Abs_Int0 |
|
4 imports Abs_State |
|
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 st up acom \<Rightarrow> 'a st up acom) \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom" |
|
14 assumes pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> f(pfp f c) \<sqsubseteq> pfp f c" |
|
15 and strip_pfp: "\<forall>c. strip(f c) = strip c \<Longrightarrow> strip(pfp f c) = strip c" |
|
16 begin |
|
17 |
|
18 fun aval' :: "aexp \<Rightarrow> 'a st \<Rightarrow> 'a" where |
|
19 "aval' (N n) _ = num' n" | |
|
20 "aval' (V x) S = lookup S x" | |
|
21 "aval' (Plus a1 a2) S = plus' (aval' a1 S) (aval' a2 S)" |
|
22 |
|
23 fun step :: "'a st up \<Rightarrow> 'a st up acom \<Rightarrow> 'a st up acom" where |
|
24 "step S (SKIP {P}) = (SKIP {S})" | |
|
25 "step S (x ::= e {P}) = |
|
26 x ::= e {case S of Bot \<Rightarrow> Bot | Up S \<Rightarrow> Up(update S x (aval' e S))}" | |
|
27 "step S (c1; c2) = step S c1; step (post c1) c2" | |
|
28 "step S (IF b THEN c1 ELSE c2 {P}) = |
|
29 (let c1' = step S c1; c2' = step S c2 |
|
30 in IF b THEN c1' ELSE c2' {post c1 \<squnion> post c2})" | |
|
31 "step S ({Inv} WHILE b DO c {P}) = |
|
32 {S \<squnion> post c} WHILE b DO step Inv c {Inv}" |
|
33 |
|
34 lemma strip_step[simp]: "strip(step S c) = strip c" |
|
35 by(induct c arbitrary: S) (simp_all add: Let_def) |
|
36 |
|
37 definition AI :: "com \<Rightarrow> 'a st up acom" where |
|
38 "AI c = pfp (step Top) (bot_acom c)" |
|
39 |
|
40 |
|
41 subsubsection "Monotonicity" |
|
42 |
|
43 lemma mono_aval': "S \<sqsubseteq> S' \<Longrightarrow> aval' e S \<sqsubseteq> aval' e S'" |
|
44 by(induction e) (auto simp: le_st_def lookup_def mono_plus') |
|
45 |
|
46 lemma mono_update: "a \<sqsubseteq> a' \<Longrightarrow> S \<sqsubseteq> S' \<Longrightarrow> update S x a \<sqsubseteq> update S' x a'" |
|
47 by(auto simp add: le_st_def lookup_def update_def) |
|
48 |
|
49 lemma step_mono: "S \<sqsubseteq> S' \<Longrightarrow> step S c \<sqsubseteq> step S' c" |
|
50 apply(induction c arbitrary: S S') |
|
51 apply (auto simp: Let_def mono_update mono_aval' le_join_disj split: up.split) |
|
52 done |
|
53 |
|
54 subsubsection "Soundness" |
|
55 |
|
56 lemma aval'_sound: "s <:f S \<Longrightarrow> aval a s <: aval' a S" |
|
57 by (induct a) (auto simp: rep_num' rep_plus' rep_st_def lookup_def) |
|
58 |
|
59 lemma in_rep_update: "\<lbrakk> s <:f S; i <: a \<rbrakk> \<Longrightarrow> s(x := i) <:f update S x a" |
|
60 by(simp add: rep_st_def lookup_update) |
|
61 |
|
62 lemma step_sound: |
|
63 "step S c \<sqsubseteq> c \<Longrightarrow> (strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up S \<Longrightarrow> t <:up post c" |
|
64 proof(induction c arbitrary: S s t) |
|
65 case SKIP thus ?case |
|
66 by simp (metis skipE up_fun_in_rep_le) |
|
67 next |
|
68 case Assign thus ?case |
|
69 apply (auto simp del: fun_upd_apply simp: split: up.splits) |
|
70 by (metis aval'_sound fun_in_rep_le in_rep_update) |
|
71 next |
|
72 case Semi thus ?case by simp blast |
|
73 next |
|
74 case (If b c1 c2 S0) thus ?case |
|
75 apply(auto simp: Let_def) |
|
76 apply (metis up_fun_in_rep_le)+ |
|
77 done |
|
78 next |
|
79 case (While Inv b c P) |
|
80 from While.prems have inv: "step Inv c \<sqsubseteq> c" |
|
81 and "post c \<sqsubseteq> Inv" and "S \<sqsubseteq> Inv" and "Inv \<sqsubseteq> P" by(auto simp: Let_def) |
|
82 { fix s t have "(WHILE b DO strip c,s) \<Rightarrow> t \<Longrightarrow> s <:up Inv \<Longrightarrow> t <:up Inv" |
|
83 proof(induction "WHILE b DO strip c" s t rule: big_step_induct) |
|
84 case WhileFalse thus ?case by simp |
|
85 next |
|
86 case (WhileTrue s1 s2 s3) |
|
87 from WhileTrue.hyps(5)[OF up_fun_in_rep_le[OF While.IH[OF inv `(strip c, s1) \<Rightarrow> s2` `s1 <:up Inv`] `post c \<sqsubseteq> Inv`]] |
|
88 show ?case . |
|
89 qed |
|
90 } |
|
91 thus ?case using While.prems(2) |
|
92 by simp (metis `s <:up S` `S \<sqsubseteq> Inv` `Inv \<sqsubseteq> P` up_fun_in_rep_le) |
|
93 qed |
|
94 |
|
95 lemma AI_sound: "(c,s) \<Rightarrow> t \<Longrightarrow> t <:up post(AI c)" |
|
96 by(fastforce simp: AI_def strip_pfp in_rep_Top_up intro: step_sound pfp) |
|
97 |
|
98 end |
|
99 |
|
100 |
|
101 end |