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
|
|
11 |
| Aassign name aexp
|
|
12 |
| Asemi acom acom
|
|
13 |
| Aif bexp acom acom
|
|
14 |
| Awhile bexp assn acom
|
|
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))" |
|
|
25 |
"pre (Awhile b I c) Q = I"
|
|
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)" |
|
|
34 |
"vc (Awhile b I c) Q =
|
|
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)" |
|
|
46 |
"astrip (Awhile b I c) = (WHILE b DO astrip c)"
|
|
47 |
|
|
48 |
|
|
49 |
subsection "Soundness"
|
|
50 |
|
|
51 |
lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} astrip c {Q}"
|
|
52 |
proof(induct c arbitrary: Q)
|
|
53 |
case (Awhile b I c)
|
|
54 |
show ?case
|
|
55 |
proof(simp, rule While')
|
|
56 |
from `\<forall>s. vc (Awhile b I c) Q s`
|
|
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
|
|
59 |
have "\<turnstile> {pre c I} astrip c {I}" by(rule Awhile.hyps[OF vc])
|
|
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"
|
|
75 |
proof (induct c arbitrary: P P' s)
|
|
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"
|
|
81 |
proof(induct c arbitrary: P P')
|
|
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'")
|
|
88 |
proof (induct rule: hoare.induct)
|
|
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)
|
|
98 |
from Semi.hyps obtain ac1 where ih1: "?G P c1 Q ac1" by blast
|
|
99 |
from Semi.hyps obtain ac2 where ih2: "?G Q c2 R ac2" by blast
|
|
100 |
show ?case (is "\<exists>ac. ?C ac")
|
|
101 |
proof
|
|
102 |
show "?C(Asemi ac1 ac2)"
|
|
103 |
using ih1 ih2 by (fastsimp elim!: pre_mono vc_mono)
|
|
104 |
qed
|
|
105 |
next
|
|
106 |
case (If P b c1 Q c2)
|
|
107 |
from If.hyps obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1"
|
|
108 |
by blast
|
|
109 |
from If.hyps obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2"
|
|
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)
|
|
117 |
from While.hyps obtain ac where ih: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast
|
|
118 |
show ?case (is "\<exists>ac. ?C ac")
|
|
119 |
proof show "?C(Awhile b P ac)" using ih by simp qed
|
|
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)))" |
|
|
138 |
"vcpre (Awhile b I c) Q =
|
|
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
|