author  nipkow 
Fri, 31 May 2013 07:55:09 +0200  
changeset 52269  d867812da48b 
parent 52268  b28695e5a018 
child 52316  cc5718f60778 
permissions  rwrr 
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 