author  wenzelm 
Sat, 07 Apr 2012 16:41:59 +0200  
changeset 47389  e8552cba702d 
parent 46304  ef5d8e94f66f 
child 47818  151d137f1095 
permissions  rwrr 
43158  1 
header{* Hoare Logic for Total Correctness *} 
2 

44177
b4b5cbca2519
IMP/Util distinguishes between sets and functions again; imported only where used.
kleing
parents:
43158
diff
changeset

3 
theory HoareT imports Hoare_Sound_Complete begin 
43158  4 

46203  5 
text{* Note that this definition of total validity @{text"\<Turnstile>\<^sub>t"} only 
6 
works if execution is deterministic (which it is in our case). *} 

43158  7 

8 
definition hoare_tvalid :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" 

9 
("\<Turnstile>\<^sub>t {(1_)}/ (_)/ {(1_)}" 50) where 

10 
"\<Turnstile>\<^sub>t {P}c{Q} \<equiv> \<forall>s. P s \<longrightarrow> (\<exists>t. (c,s) \<Rightarrow> t \<and> Q t)" 

11 

45114  12 
text{* Provability of Hoare triples in the proof system for total 
43158  13 
correctness is written @{text"\<turnstile>\<^sub>t {P}c{Q}"} and defined 
14 
inductively. The rules for @{text"\<turnstile>\<^sub>t"} differ from those for 

15 
@{text"\<turnstile>"} only in the one place where nontermination can arise: the 

16 
@{term While}rule. *} 

17 

18 
inductive 

19 
hoaret :: "assn \<Rightarrow> com \<Rightarrow> assn \<Rightarrow> bool" ("\<turnstile>\<^sub>t ({(1_)}/ (_)/ {(1_)})" 50) 

20 
where 

21 
Skip: "\<turnstile>\<^sub>t {P} SKIP {P}"  

22 
Assign: "\<turnstile>\<^sub>t {\<lambda>s. P(s[a/x])} x::=a {P}"  

23 
Semi: "\<lbrakk> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1 {P\<^isub>2}; \<turnstile>\<^sub>t {P\<^isub>2} c\<^isub>2 {P\<^isub>3} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P\<^isub>1} c\<^isub>1;c\<^isub>2 {P\<^isub>3}"  

24 
If: "\<lbrakk> \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s} c\<^isub>1 {Q}; \<turnstile>\<^sub>t {\<lambda>s. P s \<and> \<not> bval b s} c\<^isub>2 {Q} \<rbrakk> 

25 
\<Longrightarrow> \<turnstile>\<^sub>t {P} IF b THEN c\<^isub>1 ELSE c\<^isub>2 {Q}"  

26 
While: 

27 
"\<lbrakk> \<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> f s = n} c {\<lambda>s. P s \<and> f s < n}\<rbrakk> 

28 
\<Longrightarrow> \<turnstile>\<^sub>t {P} WHILE b DO c {\<lambda>s. P s \<and> \<not>bval b s}"  

29 
conseq: "\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P}c{Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> 

30 
\<turnstile>\<^sub>t {P'}c{Q'}" 

31 

32 
text{* The @{term While}rule is like the one for partial correctness but it 

33 
requires additionally that with every execution of the loop body some measure 

34 
function @{term[source]"f :: state \<Rightarrow> nat"} decreases. *} 

35 

36 
lemma strengthen_pre: 

37 
"\<lbrakk> \<forall>s. P' s \<longrightarrow> P s; \<turnstile>\<^sub>t {P} c {Q} \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P'} c {Q}" 

38 
by (metis conseq) 

39 

40 
lemma weaken_post: 

41 
"\<lbrakk> \<turnstile>\<^sub>t {P} c {Q}; \<forall>s. Q s \<longrightarrow> Q' s \<rbrakk> \<Longrightarrow> \<turnstile>\<^sub>t {P} c {Q'}" 

42 
by (metis conseq) 

43 

44 
lemma Assign': "\<forall>s. P s \<longrightarrow> Q(s[a/x]) \<Longrightarrow> \<turnstile>\<^sub>t {P} x ::= a {Q}" 

45 
by (simp add: strengthen_pre[OF _ Assign]) 

46 

47 
lemma While': 

48 
assumes "\<And>n::nat. \<turnstile>\<^sub>t {\<lambda>s. P s \<and> bval b s \<and> f s = n} c {\<lambda>s. P s \<and> f s < n}" 

49 
and "\<forall>s. P s \<and> \<not> bval b s \<longrightarrow> Q s" 

50 
shows "\<turnstile>\<^sub>t {P} WHILE b DO c {Q}" 

51 
by(blast intro: assms(1) weaken_post[OF While assms(2)]) 

52 

53 
text{* Our standard example: *} 

54 

55 
abbreviation "w n == 

56 
WHILE Less (V ''y'') (N n) 

57 
DO ( ''y'' ::= Plus (V ''y'') (N 1); ''x'' ::= Plus (V ''x'') (V ''y'') )" 

58 

46304  59 
lemma "\<turnstile>\<^sub>t {\<lambda>s. 0 \<le> n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum>{1..n}}" 
43158  60 
apply(rule Semi) 
61 
prefer 2 

62 
apply(rule While' 

46203  63 
[where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 \<le> s ''y'' \<and> s ''y'' \<le> n" 
64 
and f = "\<lambda>s. nat (n  s ''y'')"]) 

43158  65 
apply(rule Semi) 
66 
prefer 2 

67 
apply(rule Assign) 

68 
apply(rule Assign') 

69 
apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps) 

70 
apply clarsimp 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44177
diff
changeset

71 
apply fastforce 
43158  72 
apply(rule Semi) 
73 
prefer 2 

74 
apply(rule Assign) 

75 
apply(rule Assign') 

76 
apply simp 

77 
done 

78 

79 

80 
text{* The soundness theorem: *} 

81 

82 
theorem hoaret_sound: "\<turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<Turnstile>\<^sub>t {P}c{Q}" 

83 
proof(unfold hoare_tvalid_def, induct rule: hoaret.induct) 

84 
case (While P b f c) 

85 
show ?case 

86 
proof 

87 
fix s 

88 
show "P s \<longrightarrow> (\<exists>t. (WHILE b DO c, s) \<Rightarrow> t \<and> P t \<and> \<not> bval b t)" 

45015  89 
proof(induction "f s" arbitrary: s rule: less_induct) 
43158  90 
case (less n) 
91 
thus ?case by (metis While(2) WhileFalse WhileTrue) 

92 
qed 

93 
qed 

94 
next 

95 
case If thus ?case by auto blast 

44890
22f665a2e91c
new fastforce replacing fastsimp  less confusing name
nipkow
parents:
44177
diff
changeset

96 
qed fastforce+ 
43158  97 

98 

99 
text{* 

100 
The completeness proof proceeds along the same lines as the one for partial 

101 
correctness. First we have to strengthen our notion of weakest precondition 

102 
to take termination into account: *} 

103 

104 
definition wpt :: "com \<Rightarrow> assn \<Rightarrow> assn" ("wp\<^sub>t") where 

105 
"wp\<^sub>t c Q \<equiv> \<lambda>s. \<exists>t. (c,s) \<Rightarrow> t \<and> Q t" 

106 

107 
lemma [simp]: "wp\<^sub>t SKIP Q = Q" 

108 
by(auto intro!: ext simp: wpt_def) 

109 

110 
lemma [simp]: "wp\<^sub>t (x ::= e) Q = (\<lambda>s. Q(s(x := aval e s)))" 

111 
by(auto intro!: ext simp: wpt_def) 

112 

113 
lemma [simp]: "wp\<^sub>t (c\<^isub>1;c\<^isub>2) Q = wp\<^sub>t c\<^isub>1 (wp\<^sub>t c\<^isub>2 Q)" 

114 
unfolding wpt_def 

115 
apply(rule ext) 

116 
apply auto 

117 
done 

118 

119 
lemma [simp]: 

120 
"wp\<^sub>t (IF b THEN c\<^isub>1 ELSE c\<^isub>2) Q = (\<lambda>s. wp\<^sub>t (if bval b s then c\<^isub>1 else c\<^isub>2) Q s)" 

121 
apply(unfold wpt_def) 

122 
apply(rule ext) 

123 
apply auto 

124 
done 

125 

126 

127 
text{* Now we define the number of iterations @{term "WHILE b DO c"} needs to 

128 
terminate when started in state @{text s}. Because this is a truly partial 

129 
function, we define it as an (inductive) relation first: *} 

130 

131 
inductive Its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat \<Rightarrow> bool" where 

132 
Its_0: "\<not> bval b s \<Longrightarrow> Its b c s 0"  

133 
Its_Suc: "\<lbrakk> bval b s; (c,s) \<Rightarrow> s'; Its b c s' n \<rbrakk> \<Longrightarrow> Its b c s (Suc n)" 

134 

135 
text{* The relation is in fact a function: *} 

136 

137 
lemma Its_fun: "Its b c s n \<Longrightarrow> Its b c s n' \<Longrightarrow> n=n'" 

45015  138 
proof(induction arbitrary: n' rule:Its.induct) 
43158  139 
(* new release: 
140 
case Its_0 thus ?case by(metis Its.cases) 

141 
next 

142 
case Its_Suc thus ?case by(metis Its.cases big_step_determ) 

143 
qed 

144 
*) 

145 
case Its_0 

146 
from this(1) Its.cases[OF this(2)] show ?case by metis 

147 
next 

148 
case (Its_Suc b s c s' n n') 

149 
note C = this 

150 
from this(5) show ?case 

151 
proof cases 

152 
case Its_0 with Its_Suc(1) show ?thesis by blast 

153 
next 

154 
case Its_Suc with C show ?thesis by(metis big_step_determ) 

155 
qed 

156 
qed 

157 

158 
text{* For all terminating loops, @{const Its} yields a result: *} 

159 

160 
lemma WHILE_Its: "(WHILE b DO c,s) \<Rightarrow> t \<Longrightarrow> \<exists>n. Its b c s n" 

45015  161 
proof(induction "WHILE b DO c" s t rule: big_step_induct) 
43158  162 
case WhileFalse thus ?case by (metis Its_0) 
163 
next 

164 
case WhileTrue thus ?case by (metis Its_Suc) 

165 
qed 

166 

167 
text{* Now the relation is turned into a function with the help of 

168 
the description operator @{text THE}: *} 

169 

170 
definition its :: "bexp \<Rightarrow> com \<Rightarrow> state \<Rightarrow> nat" where 

171 
"its b c s = (THE n. Its b c s n)" 

172 

173 
text{* The key property: every loop iteration increases @{const its} by 1. *} 

174 

175 
lemma its_Suc: "\<lbrakk> bval b s; (c, s) \<Rightarrow> s'; (WHILE b DO c, s') \<Rightarrow> t\<rbrakk> 

176 
\<Longrightarrow> its b c s = Suc(its b c s')" 

177 
by (metis its_def WHILE_Its Its.intros(2) Its_fun the_equality) 

178 

179 
lemma wpt_is_pre: "\<turnstile>\<^sub>t {wp\<^sub>t c Q} c {Q}" 

45015  180 
proof (induction c arbitrary: Q) 
43158  181 
case SKIP show ?case by simp (blast intro:hoaret.Skip) 
182 
next 

183 
case Assign show ?case by simp (blast intro:hoaret.Assign) 

184 
next 

185 
case Semi thus ?case by simp (blast intro:hoaret.Semi) 

186 
next 

187 
case If thus ?case by simp (blast intro:hoaret.If hoaret.conseq) 

188 
next 

189 
case (While b c) 

190 
let ?w = "WHILE b DO c" 

191 
{ fix n 

192 
have "\<forall>s. wp\<^sub>t ?w Q s \<and> bval b s \<and> its b c s = n \<longrightarrow> 

193 
wp\<^sub>t c (\<lambda>s'. wp\<^sub>t ?w Q s' \<and> its b c s' < n) s" 

194 
unfolding wpt_def by (metis WhileE its_Suc lessI) 

195 
note strengthen_pre[OF this While] 

196 
} note hoaret.While[OF this] 

197 
moreover have "\<forall>s. wp\<^sub>t ?w Q s \<and> \<not> bval b s \<longrightarrow> Q s" by (auto simp add:wpt_def) 

198 
ultimately show ?case by(rule weaken_post) 

199 
qed 

200 

201 

202 
text{*\noindent In the @{term While}case, @{const its} provides the obvious 

203 
termination argument. 

204 

205 
The actual completeness theorem follows directly, in the same manner 

206 
as for partial correctness: *} 

207 

208 
theorem hoaret_complete: "\<Turnstile>\<^sub>t {P}c{Q} \<Longrightarrow> \<turnstile>\<^sub>t {P}c{Q}" 

209 
apply(rule strengthen_pre[OF _ wpt_is_pre]) 

210 
apply(auto simp: hoare_tvalid_def hoare_valid_def wpt_def) 

211 
done 

212 

213 
end 