author | nipkow |
Sat, 03 Dec 2011 21:25:34 +0100 | |
changeset 45745 | 3a8bc5623410 |
parent 45212 | e87feee00a4c |
child 45840 | dadd139192d1 |
permissions | -rw-r--r-- |
43158 | 1 |
header "Verification Conditions" |
2 |
||
3 |
theory VC imports Hoare begin |
|
4 |
||
5 |
subsection "VCG via Weakest Preconditions" |
|
6 |
||
7 |
text{* Annotated commands: commands where loops are annotated with |
|
8 |
invariants. *} |
|
9 |
||
10 |
datatype acom = Askip |
|
45212 | 11 |
| Aassign vname aexp |
43158 | 12 |
| Asemi acom acom |
13 |
| Aif bexp acom acom |
|
45745 | 14 |
| Awhile assn bexp acom |
43158 | 15 |
|
16 |
text{* Weakest precondition from annotated commands: *} |
|
17 |
||
18 |
fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where |
|
19 |
"pre Askip Q = Q" | |
|
20 |
"pre (Aassign x a) Q = (\<lambda>s. Q(s(x := aval a s)))" | |
|
21 |
"pre (Asemi c\<^isub>1 c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)" | |
|
22 |
"pre (Aif b c\<^isub>1 c\<^isub>2) Q = |
|
23 |
(\<lambda>s. (bval b s \<longrightarrow> pre c\<^isub>1 Q s) \<and> |
|
24 |
(\<not> bval b s \<longrightarrow> pre c\<^isub>2 Q s))" | |
|
45745 | 25 |
"pre (Awhile I b c) Q = I" |
43158 | 26 |
|
27 |
text{* Verification condition: *} |
|
28 |
||
29 |
fun vc :: "acom \<Rightarrow> assn \<Rightarrow> assn" where |
|
30 |
"vc Askip Q = (\<lambda>s. True)" | |
|
31 |
"vc (Aassign x a) Q = (\<lambda>s. True)" | |
|
32 |
"vc (Asemi c\<^isub>1 c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 (pre c\<^isub>2 Q) s \<and> vc c\<^isub>2 Q s)" | |
|
33 |
"vc (Aif b c\<^isub>1 c\<^isub>2) Q = (\<lambda>s. vc c\<^isub>1 Q s \<and> vc c\<^isub>2 Q s)" | |
|
45745 | 34 |
"vc (Awhile I b c) Q = |
43158 | 35 |
(\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and> |
36 |
(I s \<and> bval b s \<longrightarrow> pre c I s) \<and> |
|
37 |
vc c I s)" |
|
38 |
||
39 |
text{* Strip annotations: *} |
|
40 |
||
41 |
fun astrip :: "acom \<Rightarrow> com" where |
|
42 |
"astrip Askip = SKIP" | |
|
43 |
"astrip (Aassign x a) = (x::=a)" | |
|
44 |
"astrip (Asemi c\<^isub>1 c\<^isub>2) = (astrip c\<^isub>1; astrip c\<^isub>2)" | |
|
45 |
"astrip (Aif b c\<^isub>1 c\<^isub>2) = (IF b THEN astrip c\<^isub>1 ELSE astrip c\<^isub>2)" | |
|
45745 | 46 |
"astrip (Awhile I b c) = (WHILE b DO astrip c)" |
43158 | 47 |
|
48 |
||
49 |
subsection "Soundness" |
|
50 |
||
51 |
lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} astrip c {Q}" |
|
45015 | 52 |
proof(induction c arbitrary: Q) |
45745 | 53 |
case (Awhile I b c) |
43158 | 54 |
show ?case |
55 |
proof(simp, rule While') |
|
45745 | 56 |
from `\<forall>s. vc (Awhile I b c) Q s` |
43158 | 57 |
have vc: "\<forall>s. vc c I s" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and |
58 |
pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre c I s" by simp_all |
|
45015 | 59 |
have "\<turnstile> {pre c I} astrip c {I}" by(rule Awhile.IH[OF vc]) |
43158 | 60 |
with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} astrip c {I}" |
61 |
by(rule strengthen_pre) |
|
62 |
show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ) |
|
63 |
qed |
|
64 |
qed (auto intro: hoare.conseq) |
|
65 |
||
66 |
corollary vc_sound': |
|
67 |
"(\<forall>s. vc c Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c Q s) \<Longrightarrow> \<turnstile> {P} astrip c {Q}" |
|
68 |
by (metis strengthen_pre vc_sound) |
|
69 |
||
70 |
||
71 |
subsection "Completeness" |
|
72 |
||
73 |
lemma pre_mono: |
|
74 |
"\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre c P s \<Longrightarrow> pre c P' s" |
|
45015 | 75 |
proof (induction c arbitrary: P P' s) |
43158 | 76 |
case Asemi thus ?case by simp metis |
77 |
qed simp_all |
|
78 |
||
79 |
lemma vc_mono: |
|
80 |
"\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc c P s \<Longrightarrow> vc c P' s" |
|
45015 | 81 |
proof(induction c arbitrary: P P') |
43158 | 82 |
case Asemi thus ?case by simp (metis pre_mono) |
83 |
qed simp_all |
|
84 |
||
85 |
lemma vc_complete: |
|
86 |
"\<turnstile> {P}c{Q} \<Longrightarrow> \<exists>c'. astrip c' = c \<and> (\<forall>s. vc c' Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c' Q s)" |
|
87 |
(is "_ \<Longrightarrow> \<exists>c'. ?G P c Q c'") |
|
45015 | 88 |
proof (induction rule: hoare.induct) |
43158 | 89 |
case Skip |
90 |
show ?case (is "\<exists>ac. ?C ac") |
|
91 |
proof show "?C Askip" by simp qed |
|
92 |
next |
|
93 |
case (Assign P a x) |
|
94 |
show ?case (is "\<exists>ac. ?C ac") |
|
95 |
proof show "?C(Aassign x a)" by simp qed |
|
96 |
next |
|
97 |
case (Semi P c1 Q c2 R) |
|
45015 | 98 |
from Semi.IH obtain ac1 where ih1: "?G P c1 Q ac1" by blast |
99 |
from Semi.IH obtain ac2 where ih2: "?G Q c2 R ac2" by blast |
|
43158 | 100 |
show ?case (is "\<exists>ac. ?C ac") |
101 |
proof |
|
102 |
show "?C(Asemi ac1 ac2)" |
|
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
43158
diff
changeset
|
103 |
using ih1 ih2 by (fastforce elim!: pre_mono vc_mono) |
43158 | 104 |
qed |
105 |
next |
|
106 |
case (If P b c1 Q c2) |
|
45015 | 107 |
from If.IH obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1" |
43158 | 108 |
by blast |
45015 | 109 |
from If.IH obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2" |
43158 | 110 |
by blast |
111 |
show ?case (is "\<exists>ac. ?C ac") |
|
112 |
proof |
|
113 |
show "?C(Aif b ac1 ac2)" using ih1 ih2 by simp |
|
114 |
qed |
|
115 |
next |
|
116 |
case (While P b c) |
|
45015 | 117 |
from While.IH obtain ac where ih: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast |
43158 | 118 |
show ?case (is "\<exists>ac. ?C ac") |
45745 | 119 |
proof show "?C(Awhile P b ac)" using ih by simp qed |
43158 | 120 |
next |
121 |
case conseq thus ?case by(fast elim!: pre_mono vc_mono) |
|
122 |
qed |
|
123 |
||
124 |
||
125 |
subsection "An Optimization" |
|
126 |
||
127 |
fun vcpre :: "acom \<Rightarrow> assn \<Rightarrow> assn \<times> assn" where |
|
128 |
"vcpre Askip Q = (\<lambda>s. True, Q)" | |
|
129 |
"vcpre (Aassign x a) Q = (\<lambda>s. True, \<lambda>s. Q(s[a/x]))" | |
|
130 |
"vcpre (Asemi c\<^isub>1 c\<^isub>2) Q = |
|
131 |
(let (vc\<^isub>2,wp\<^isub>2) = vcpre c\<^isub>2 Q; |
|
132 |
(vc\<^isub>1,wp\<^isub>1) = vcpre c\<^isub>1 wp\<^isub>2 |
|
133 |
in (\<lambda>s. vc\<^isub>1 s \<and> vc\<^isub>2 s, wp\<^isub>1))" | |
|
134 |
"vcpre (Aif b c\<^isub>1 c\<^isub>2) Q = |
|
135 |
(let (vc\<^isub>2,wp\<^isub>2) = vcpre c\<^isub>2 Q; |
|
136 |
(vc\<^isub>1,wp\<^isub>1) = vcpre c\<^isub>1 Q |
|
137 |
in (\<lambda>s. vc\<^isub>1 s \<and> vc\<^isub>2 s, \<lambda>s. (bval b s \<longrightarrow> wp\<^isub>1 s) \<and> (\<not>bval b s \<longrightarrow> wp\<^isub>2 s)))" | |
|
45745 | 138 |
"vcpre (Awhile I b c) Q = |
43158 | 139 |
(let (vcc,wpc) = vcpre c I |
140 |
in (\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and> |
|
141 |
(I s \<and> bval b s \<longrightarrow> wpc s) \<and> vcc s, I))" |
|
142 |
||
143 |
lemma vcpre_vc_pre: "vcpre c Q = (vc c Q, pre c Q)" |
|
144 |
by (induct c arbitrary: Q) (simp_all add: Let_def) |
|
145 |
||
146 |
end |