author | nipkow |
Fri, 31 May 2013 07:55:09 +0200 | |
changeset 52269 | d867812da48b |
parent 52268 | b28695e5a018 |
child 52316 | cc5718f60778 |
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)" | |
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
23 |
"strip (c\<^isub>1;; c\<^isub>2) = (strip c\<^isub>1;; strip c\<^isub>2)" | |
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
24 |
"strip (IF b THEN c\<^isub>1 ELSE c\<^isub>2) = (IF b THEN strip c\<^isub>1 ELSE strip c\<^isub>2)" | |
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
25 |
"strip ({_} WHILE b DO c) = (WHILE b DO strip c)" |
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)))" | |
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
32 |
"pre (c\<^isub>1;; c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)" | |
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
33 |
"pre (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q = |
43158 | 34 |
(\<lambda>s. (bval b s \<longrightarrow> pre c\<^isub>1 Q s) \<and> |
35 |
(\<not> bval b s \<longrightarrow> pre c\<^isub>2 Q s))" | |
|
52267
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
36 |
"pre ({I} WHILE b DO c) Q = I" |
43158 | 37 |
|
38 |
text{* Verification condition: *} |
|
39 |
||
40 |
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
|
41 |
"vc SKIP Q = (\<lambda>s. True)" | |
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
42 |
"vc (x ::= a) Q = (\<lambda>s. True)" | |
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
43 |
"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)" | |
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
44 |
"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)" | |
2a16957cd379
used nice syntax, removed lemma because it makes a nice exercise.
nipkow
parents:
52193
diff
changeset
|
45 |
"vc ({I} WHILE b DO c) Q = |
43158 | 46 |
(\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and> |
47 |
(I s \<and> bval b s \<longrightarrow> pre c I s) \<and> |
|
48 |
vc c I s)" |
|
49 |
||
50 |
||
50421 | 51 |
text {* Soundness: *} |
43158 | 52 |
|
45840 | 53 |
lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} strip c {Q}" |
45015 | 54 |
proof(induction c arbitrary: Q) |
45745 | 55 |
case (Awhile I b c) |
43158 | 56 |
show ?case |
57 |
proof(simp, rule While') |
|
45745 | 58 |
from `\<forall>s. vc (Awhile I b c) Q s` |
43158 | 59 |
have vc: "\<forall>s. vc c I s" and IQ: "\<forall>s. I s \<and> \<not> bval b s \<longrightarrow> Q s" and |
60 |
pre: "\<forall>s. I s \<and> bval b s \<longrightarrow> pre c I s" by simp_all |
|
45840 | 61 |
have "\<turnstile> {pre c I} strip c {I}" by(rule Awhile.IH[OF vc]) |
62 |
with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} strip c {I}" |
|
43158 | 63 |
by(rule strengthen_pre) |
64 |
show "\<forall>s. I s \<and> \<not>bval b s \<longrightarrow> Q s" by(rule IQ) |
|
65 |
qed |
|
66 |
qed (auto intro: hoare.conseq) |
|
67 |
||
68 |
corollary vc_sound': |
|
45840 | 69 |
"(\<forall>s. vc c Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c Q s) \<Longrightarrow> \<turnstile> {P} strip c {Q}" |
43158 | 70 |
by (metis strengthen_pre vc_sound) |
71 |
||
72 |
||
50421 | 73 |
text{* Completeness: *} |
43158 | 74 |
|
75 |
lemma pre_mono: |
|
76 |
"\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> pre c P s \<Longrightarrow> pre c P' s" |
|
45015 | 77 |
proof (induction c arbitrary: P P' s) |
47818 | 78 |
case Aseq thus ?case by simp metis |
43158 | 79 |
qed simp_all |
80 |
||
81 |
lemma vc_mono: |
|
82 |
"\<forall>s. P s \<longrightarrow> P' s \<Longrightarrow> vc c P s \<Longrightarrow> vc c P' s" |
|
45015 | 83 |
proof(induction c arbitrary: P P') |
47818 | 84 |
case Aseq thus ?case by simp (metis pre_mono) |
43158 | 85 |
qed simp_all |
86 |
||
87 |
lemma vc_complete: |
|
45840 | 88 |
"\<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)" |
43158 | 89 |
(is "_ \<Longrightarrow> \<exists>c'. ?G P c Q c'") |
45015 | 90 |
proof (induction rule: hoare.induct) |
43158 | 91 |
case Skip |
92 |
show ?case (is "\<exists>ac. ?C ac") |
|
52193 | 93 |
proof show "?C Askip" by simp qed |
43158 | 94 |
next |
95 |
case (Assign P a x) |
|
96 |
show ?case (is "\<exists>ac. ?C ac") |
|
97 |
proof show "?C(Aassign x a)" by simp qed |
|
98 |
next |
|
47818 | 99 |
case (Seq P c1 Q c2 R) |
100 |
from Seq.IH obtain ac1 where ih1: "?G P c1 Q ac1" by blast |
|
101 |
from Seq.IH obtain ac2 where ih2: "?G Q c2 R ac2" by blast |
|
43158 | 102 |
show ?case (is "\<exists>ac. ?C ac") |
103 |
proof |
|
47818 | 104 |
show "?C(Aseq ac1 ac2)" |
44890
22f665a2e91c
new fastforce replacing fastsimp - less confusing name
nipkow
parents:
43158
diff
changeset
|
105 |
using ih1 ih2 by (fastforce elim!: pre_mono vc_mono) |
43158 | 106 |
qed |
107 |
next |
|
108 |
case (If P b c1 Q c2) |
|
45015 | 109 |
from If.IH obtain ac1 where ih1: "?G (\<lambda>s. P s \<and> bval b s) c1 Q ac1" |
43158 | 110 |
by blast |
45015 | 111 |
from If.IH obtain ac2 where ih2: "?G (\<lambda>s. P s \<and> \<not>bval b s) c2 Q ac2" |
43158 | 112 |
by blast |
113 |
show ?case (is "\<exists>ac. ?C ac") |
|
114 |
proof |
|
115 |
show "?C(Aif b ac1 ac2)" using ih1 ih2 by simp |
|
116 |
qed |
|
117 |
next |
|
118 |
case (While P b c) |
|
45015 | 119 |
from While.IH obtain ac where ih: "?G (\<lambda>s. P s \<and> bval b s) c P ac" by blast |
43158 | 120 |
show ?case (is "\<exists>ac. ?C ac") |
45745 | 121 |
proof show "?C(Awhile P b ac)" using ih by simp qed |
43158 | 122 |
next |
123 |
case conseq thus ?case by(fast elim!: pre_mono vc_mono) |
|
124 |
qed |
|
125 |
||
126 |
end |