|
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 theory VCG_Total_EX2 |
|
4 imports Hoare_Total_EX2 |
|
5 begin |
|
6 |
|
7 subsection "Verification Conditions for Total Correctness" |
|
8 |
|
9 text \<open> |
|
10 Theory \<open>VCG_Total_EX\<close> conatins a VCG built on top of a Hoare logic without logical variables. |
|
11 As a result the completeness proof runs into a problem. This theory uses a Hoare logic |
|
12 with logical variables and proves soundness and completeness. |
|
13 \<close> |
|
14 |
|
15 text{* Annotated commands: commands where loops are annotated with |
|
16 invariants. *} |
|
17 |
|
18 datatype acom = |
|
19 Askip ("SKIP") | |
|
20 Aassign vname aexp ("(_ ::= _)" [1000, 61] 61) | |
|
21 Aseq acom acom ("_;;/ _" [60, 61] 60) | |
|
22 Aif bexp acom acom ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) | |
|
23 Awhile assn2 lvname bexp acom |
|
24 ("({_'/_}/ WHILE _/ DO _)" [0, 0, 0, 61] 61) |
|
25 |
|
26 notation com.SKIP ("SKIP") |
|
27 |
|
28 text{* Strip annotations: *} |
|
29 |
|
30 fun strip :: "acom \<Rightarrow> com" where |
|
31 "strip SKIP = SKIP" | |
|
32 "strip (x ::= a) = (x ::= a)" | |
|
33 "strip (C\<^sub>1;; C\<^sub>2) = (strip C\<^sub>1;; strip C\<^sub>2)" | |
|
34 "strip (IF b THEN C\<^sub>1 ELSE C\<^sub>2) = (IF b THEN strip C\<^sub>1 ELSE strip C\<^sub>2)" | |
|
35 "strip ({_/_} WHILE b DO C) = (WHILE b DO strip C)" |
|
36 |
|
37 text{* Weakest precondition from annotated commands: *} |
|
38 |
|
39 fun pre :: "acom \<Rightarrow> assn2 \<Rightarrow> assn2" where |
|
40 "pre SKIP Q = Q" | |
|
41 "pre (x ::= a) Q = (\<lambda>l s. Q l (s(x := aval a s)))" | |
|
42 "pre (C\<^sub>1;; C\<^sub>2) Q = pre C\<^sub>1 (pre C\<^sub>2 Q)" | |
|
43 "pre (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q = |
|
44 (\<lambda>l s. if bval b s then pre C\<^sub>1 Q l s else pre C\<^sub>2 Q l s)" | |
|
45 "pre ({I/x} WHILE b DO C) Q = (\<lambda>l s. EX n. I (l(x:=n)) s)" |
|
46 |
|
47 text{* Verification condition: *} |
|
48 |
|
49 fun vc :: "acom \<Rightarrow> assn2 \<Rightarrow> bool" where |
|
50 "vc SKIP Q = True" | |
|
51 "vc (x ::= a) Q = True" | |
|
52 "vc (C\<^sub>1;; C\<^sub>2) Q = (vc C\<^sub>1 (pre C\<^sub>2 Q) \<and> vc C\<^sub>2 Q)" | |
|
53 "vc (IF b THEN C\<^sub>1 ELSE C\<^sub>2) Q = (vc C\<^sub>1 Q \<and> vc C\<^sub>2 Q)" | |
|
54 "vc ({I/x} WHILE b DO C) Q = |
|
55 (\<forall>l s. (I (l(x:=Suc(l x))) s \<longrightarrow> pre C I l s) \<and> |
|
56 (l x > 0 \<and> I l s \<longrightarrow> bval b s) \<and> |
|
57 (I (l(x := 0)) s \<longrightarrow> \<not> bval b s \<and> Q l s) \<and> |
|
58 vc C I)" |
|
59 |
|
60 lemma vc_sound: "vc C Q \<Longrightarrow> \<turnstile>\<^sub>t {pre C Q} strip C {Q}" |
|
61 proof(induction C arbitrary: Q) |
|
62 case (Awhile I x b C) |
|
63 show ?case |
|
64 proof(simp, rule weaken_post[OF While[of I x]], goal_cases) |
|
65 case 1 show ?case |
|
66 using Awhile.IH[of "I"] Awhile.prems by (auto intro: strengthen_pre) |
|
67 next |
|
68 case 3 show ?case |
|
69 using Awhile.prems by (simp) (metis fun_upd_triv) |
|
70 qed (insert Awhile.prems, auto) |
|
71 qed (auto intro: conseq Seq If simp: Skip Assign) |
|
72 |
|
73 |
|
74 text{* Completeness: *} |
|
75 |
|
76 lemma pre_mono: |
|
77 "\<forall>l s. P l s \<longrightarrow> P' l s \<Longrightarrow> pre C P l s \<Longrightarrow> pre C P' l s" |
|
78 proof (induction C arbitrary: P P' l s) |
|
79 case Aseq thus ?case by simp metis |
|
80 qed simp_all |
|
81 |
|
82 lemma vc_mono: |
|
83 "\<forall>l s. P l s \<longrightarrow> P' l s \<Longrightarrow> vc C P \<Longrightarrow> vc C P'" |
|
84 proof(induction C arbitrary: P P') |
|
85 case Aseq thus ?case by simp (metis pre_mono) |
|
86 qed simp_all |
|
87 |
|
88 lemma vc_complete: |
|
89 "\<turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<exists>C. strip C = c \<and> vc C Q \<and> (\<forall>l s. P l s \<longrightarrow> pre C Q l s)" |
|
90 (is "_ \<Longrightarrow> \<exists>C. ?G P c Q C") |
|
91 proof (induction rule: hoaret.induct) |
|
92 case Skip |
|
93 show ?case (is "\<exists>C. ?C C") |
|
94 proof show "?C Askip" by simp qed |
|
95 next |
|
96 case (Assign P a x) |
|
97 show ?case (is "\<exists>C. ?C C") |
|
98 proof show "?C(Aassign x a)" by simp qed |
|
99 next |
|
100 case (Seq P c1 Q c2 R) |
|
101 from Seq.IH obtain C1 where ih1: "?G P c1 Q C1" by blast |
|
102 from Seq.IH obtain C2 where ih2: "?G Q c2 R C2" by blast |
|
103 show ?case (is "\<exists>C. ?C C") |
|
104 proof |
|
105 show "?C(Aseq C1 C2)" |
|
106 using ih1 ih2 by (fastforce elim!: pre_mono vc_mono) |
|
107 qed |
|
108 next |
|
109 case (If P b c1 Q c2) |
|
110 from If.IH obtain C1 where ih1: "?G (\<lambda>l s. P l s \<and> bval b s) c1 Q C1" |
|
111 by blast |
|
112 from If.IH obtain C2 where ih2: "?G (\<lambda>l s. P l s \<and> \<not>bval b s) c2 Q C2" |
|
113 by blast |
|
114 show ?case (is "\<exists>C. ?C C") |
|
115 proof |
|
116 show "?C(Aif b C1 C2)" using ih1 ih2 by simp |
|
117 qed |
|
118 next |
|
119 case (While P x c b) |
|
120 from While.IH obtain C where |
|
121 ih: "?G (\<lambda>l s. P (l(x:=Suc(l x))) s \<and> bval b s) c P C" |
|
122 by blast |
|
123 show ?case (is "\<exists>C. ?C C") |
|
124 proof |
|
125 have "vc ({P/x} WHILE b DO C) (\<lambda>l. P (l(x := 0)))" |
|
126 using ih While.hyps(2,3) |
|
127 by simp (metis fun_upd_same zero_less_Suc) |
|
128 thus "?C(Awhile P x b C)" using ih by simp |
|
129 qed |
|
130 next |
|
131 case conseq thus ?case by(fast elim!: pre_mono vc_mono) |
|
132 qed |
|
133 |
|
134 end |