author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 45840  dadd139192d1 
child 47818  151d137f1095 
permissions  rwrr 
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 

45840  10 
datatype acom = 
11 
ASKIP  

12 
Aassign vname aexp ("(_ ::= _)" [1000, 61] 61)  

13 
Asemi acom acom ("_;/ _" [60, 61] 60)  

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 

17 
text{* Weakest precondition from annotated commands: *} 

18 

19 
fun pre :: "acom \<Rightarrow> assn \<Rightarrow> assn" where 

45840  20 
"pre ASKIP Q = Q"  
43158  21 
"pre (Aassign x a) Q = (\<lambda>s. Q(s(x := aval a s)))"  
22 
"pre (Asemi c\<^isub>1 c\<^isub>2) Q = pre c\<^isub>1 (pre c\<^isub>2 Q)"  

23 
"pre (Aif b c\<^isub>1 c\<^isub>2) Q = 

24 
(\<lambda>s. (bval b s \<longrightarrow> pre c\<^isub>1 Q s) \<and> 

25 
(\<not> bval b s \<longrightarrow> pre c\<^isub>2 Q s))"  

45745  26 
"pre (Awhile I b c) Q = I" 
43158  27 

28 
text{* Verification condition: *} 

29 

30 
fun vc :: "acom \<Rightarrow> assn \<Rightarrow> assn" where 

45840  31 
"vc ASKIP Q = (\<lambda>s. True)"  
43158  32 
"vc (Aassign x a) Q = (\<lambda>s. True)"  
33 
"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)"  

34 
"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  35 
"vc (Awhile I b c) Q = 
43158  36 
(\<lambda>s. (I s \<and> \<not> bval b s \<longrightarrow> Q s) \<and> 
37 
(I s \<and> bval b s \<longrightarrow> pre c I s) \<and> 

38 
vc c I s)" 

39 

40 
text{* Strip annotations: *} 

41 

45840  42 
fun strip :: "acom \<Rightarrow> com" where 
43 
"strip ASKIP = SKIP"  

44 
"strip (Aassign x a) = (x::=a)"  

45 
"strip (Asemi c\<^isub>1 c\<^isub>2) = (strip c\<^isub>1; strip c\<^isub>2)"  

46 
"strip (Aif b c\<^isub>1 c\<^isub>2) = (IF b THEN strip c\<^isub>1 ELSE strip c\<^isub>2)"  

47 
"strip (Awhile I b c) = (WHILE b DO strip c)" 

43158  48 

49 
subsection "Soundness" 

50 

45840  51 
lemma vc_sound: "\<forall>s. vc c Q s \<Longrightarrow> \<turnstile> {pre c Q} strip 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 

45840  59 
have "\<turnstile> {pre c I} strip c {I}" by(rule Awhile.IH[OF vc]) 
60 
with pre show "\<turnstile> {\<lambda>s. I s \<and> bval b s} strip c {I}" 

43158  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': 

45840  67 
"(\<forall>s. vc c Q s) \<and> (\<forall>s. P s \<longrightarrow> pre c Q s) \<Longrightarrow> \<turnstile> {P} strip c {Q}" 
43158  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: 

45840  86 
"\<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  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") 

45840  91 
proof show "?C ASKIP" by simp qed 
43158  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 

45840  128 
"vcpre ASKIP Q = (\<lambda>s. True, Q)"  
43158  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 