author | nipkow |
Fri, 07 Jun 2013 12:55:09 +0200 | |
changeset 52332 | 8cc665635f83 |
parent 52331 | 427fa76ea727 |
child 52371 | 55908a74065f |
permissions | -rw-r--r-- |
50421 | 1 |
(* Author: Tobias Nipkow *) |
43158 | 2 |
|
52269 | 3 |
theory VCG imports Hoare begin |
43158 | 4 |
|
50421 | 5 |
subsection "Verification Conditions" |
43158 | 6 |
|
7 |
text{* Annotated commands: commands where loops are annotated with |
|
8 |
invariants. *} |
|
9 |
||
45840 | 10 |
datatype acom = |
52193 | 11 |
Askip ("SKIP") | |
45840 | 12 |
Aassign vname aexp ("(_ ::= _)" [1000, 61] 61) | |
52046
bc01725d7918
replaced `;' by `;;' to disambiguate syntax; unexpected slight increase in build time
nipkow
parents:
50421
diff
changeset
|
13 |
Aseq acom acom ("_;;/ _" [60, 61] 60) | |
45840 | 14 |
Aif bexp acom acom ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) | |
15 |
Awhile assn bexp acom ("({_}/ WHILE _/ DO _)" [0, 0, 61] 61) |
|
43158 | 16 |
|
52267
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
17 |
|
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
18 |
text{* Strip annotations: *} |
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
19 |
|
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
20 |
fun strip :: "acom \<Rightarrow> com" where |
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
21 |
"strip SKIP = com.SKIP" | |
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
22 |
"strip (x ::= a) = (x ::= a)" | |
52332 | 23 |
"strip (C\<^isub>1;; C\<^isub>2) = (strip C\<^isub>1;; strip C\<^isub>2)" | |
24 |
"strip (IF b THEN C\<^isub>1 ELSE C\<^isub>2) = (IF b THEN strip C\<^isub>1 ELSE strip C\<^isub>2)" | |
|
25 |
"strip ({_} WHILE b DO C) = (WHILE b DO strip C)" |
|
52267
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
26 |
|
43158 | 27 |
text{* Weakest precondition from annotated commands: *} |
28 |
||
29 |
fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where |
|
52267
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
30 |
"pre SKIP Q = Q" | |
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
31 |
"pre (x ::= a) Q = (\<lambda>s. Q(s(x := aval a s)))" | |
52332 | 32 |
"pre (C\<^isub>1;; C\<^isub>2) Q = pre C\<^isub>1 (pre C\<^isub>2 Q)" | |
33 |
"pre (IF b THEN C\<^isub>1 ELSE C\<^isub>2) Q = |
|
34 |
(\<lambda>s. if bval b s then pre C\<^isub>1 Q s else pre C\<^isub>2 Q s)" | |
|
35 |
"pre ({I} WHILE b DO C) Q = I" |
|
43158 | 36 |
|
37 |
text{* Verification condition: *} |
|
38 |
||
39 |
fun vc :: "acom \<Rightarrow> assn \<Rightarrow> assn" where |
|
52267
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
40 |
"vc SKIP Q = (\<lambda>s. True)" | |
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
41 |
"vc (x ::= a) Q = (\<lambda>s. True)" | |
52332 | 42 |
"vc (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)" | |
43 |
"vc (IF b THEN C\<^isub>1 ELSE C\<^isub>2) Q = (\<lambda>s. vc C\<^isub>1 Q s \<and> vc C\<^isub>2 Q s)" | |
|
44 |
"vc ({I} WHILE b DO C) Q = |
|
43158 | 45 |
(\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and> |
52332 | 46 |
(I s \<and> bval b s \<longrightarrow> pre C I s) \<and> |
47 |
vc C I s)" |
|
43158 | 48 |
|
49 |
||
50421 | 50 |
text {* Soundness: *} |
43158 | 51 |
|
52332 | 52 |
lemma vc_sound: "\<forall>s. vc C Q s \<Longrightarrow> \<turnstile> {pre C Q} strip C {Q}" |
53 |
proof(induction C arbitrary: Q) |
|
54 |
case (Awhile I b C) |
|
43158 | 55 |
show ?case |
56 |
proof(simp, rule While') |
|
52332 | 57 |
from `\<forall>s. vc (Awhile I b C) Q s` |
58 |
have vc: "\<forall>s. vc C I s" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and |
|
59 |
pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre C I s" by simp_all |
|
60 |
have "\<turnstile> {pre C I} strip C {I}" by(rule Awhile.IH[OF vc]) |
|
61 |
with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} strip C {I}" |
|
43158 | 62 |
by(rule strengthen_pre) |
63 |
show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ) |
|
64 |
qed |
|
65 |
qed (auto intro: hoare.conseq) |
|
66 |
||
67 |
corollary vc_sound': |
|
52332 | 68 |
"\<lbrakk> \<forall>s. vc C Q s; \<forall>s. P s \<longrightarrow> pre C Q s \<rbrakk> \<Longrightarrow> \<turnstile> {P} strip C {Q}" |
43158 | 69 |
by (metis strengthen_pre vc_sound) |
70 |
||
71 |
||
50421 | 72 |
text{* Completeness: *} |
43158 | 73 |
|
74 |
lemma pre_mono: |
|
52332 | 75 |
"\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre C P s \<Longrightarrow> pre C P' s" |
76 |
proof (induction C arbitrary: P P' s) |
|
47818 | 77 |
case Aseq thus ?case by simp metis |
43158 | 78 |
qed simp_all |
79 |
||
80 |
lemma vc_mono: |
|
52332 | 81 |
"\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc C P s \<Longrightarrow> vc C P' s" |
82 |
proof(induction C arbitrary: P P') |
|
47818 | 83 |
case Aseq thus ?case by simp (metis pre_mono) |
43158 | 84 |
qed simp_all |
85 |
||
86 |
lemma vc_complete: |
|
52332 | 87 |
"\<turnstile> {P}c{Q} \<Longrightarrow> \<exists>C. strip C = c \<and> (\<forall>s. vc C Q s) \<and> (\<forall>s. P s \<longrightarrow> pre C Q s)" |
88 |
(is "_ \<Longrightarrow> \<exists>C. ?G P c Q C") |
|
45015 | 89 |
proof (induction rule: hoare.induct) |
43158 | 90 |
case Skip |
52332 | 91 |
show ?case (is "\<exists>C. ?C C") |
52193 | 92 |
proof show "?C Askip" by simp qed |
43158 | 93 |
next |
94 |
case (Assign P a x) |
|
52332 | 95 |
show ?case (is "\<exists>C. ?C C") |
43158 | 96 |
proof show "?C(Aassign x a)" by simp qed |
97 |
next |
|
47818 | 98 |
case (Seq P c1 Q c2 R) |
52332 | 99 |
from Seq.IH obtain C1 where ih1: "?G P c1 Q C1" by blast |
100 |
from Seq.IH obtain C2 where ih2: "?G Q c2 R C2" by blast |
|
101 |
show ?case (is "\<exists>C. ?C C") |
|
43158 | 102 |
proof |
52332 | 103 |
show "?C(Aseq C1 C2)" |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
43158
diff
changeset
|
104 |
using ih1 ih2 by (fastforce elim!: pre_mono vc_mono) |
43158 | 105 |
qed |
106 |
next |
|
107 |
case (If P b c1 Q c2) |
|
52332 | 108 |
from If.IH obtain C1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q C1" |
43158 | 109 |
by blast |
52332 | 110 |
from If.IH obtain C2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q C2" |
43158 | 111 |
by blast |
52332 | 112 |
show ?case (is "\<exists>C. ?C C") |
43158 | 113 |
proof |
52332 | 114 |
show "?C(Aif b C1 C2)" using ih1 ih2 by simp |
43158 | 115 |
qed |
116 |
next |
|
117 |
case (While P b c) |
|
52332 | 118 |
from While.IH obtain C where ih: "?G (\<lambda>s. P s \<and> bval b s) c P C" by blast |
119 |
show ?case (is "\<exists>C. ?C C") |
|
120 |
proof show "?C(Awhile P b C)" using ih by simp qed |
|
43158 | 121 |
next |
122 |
case conseq thus ?case by(fast elim!: pre_mono vc_mono) |
|
123 |
qed |
|
124 |
||
125 |
end |