author  nipkow 
Mon, 12 Sep 2011 07:55:43 +0200  
changeset 44890  22f665a2e91c 
parent 44177  b4b5cbca2519 
child 45015  fdac1e9880eb 
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 

5 
text{* 

6 
Now that we have termination, we can define 

7 
total validity, @{text"\<Turnstile>\<^sub>t"}, as partial validity and guaranteed termination:*} 

8 

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

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

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

12 

13 
text{* Proveability of Hoare triples in the proof system for total 

14 
correctness is written @{text"\<turnstile>\<^sub>t {P}c{Q}"} and defined 

15 
inductively. The rules for @{text"\<turnstile>\<^sub>t"} differ from those for 

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

17 
@{term While}rule. *} 

18 

19 
inductive 

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

21 
where 

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

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

24 
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}"  

25 
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> 

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

27 
While: 

28 
"\<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> 

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

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

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

32 

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

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

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

36 

37 
lemma strengthen_pre: 

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

39 
by (metis conseq) 

40 

41 
lemma weaken_post: 

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

43 
by (metis conseq) 

44 

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

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

47 

48 
lemma While': 

49 
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}" 

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

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

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

53 

54 
text{* Our standard example: *} 

55 

56 
abbreviation "w n == 

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

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

59 

60 
lemma "\<turnstile>\<^sub>t {\<lambda>s. 0 <= n} ''x'' ::= N 0; ''y'' ::= N 0; w n {\<lambda>s. s ''x'' = \<Sum> {1 .. n}}" 

61 
apply(rule Semi) 

62 
prefer 2 

63 
apply(rule While' 

64 
[where P = "\<lambda>s. s ''x'' = \<Sum> {1..s ''y''} \<and> 0 <= n \<and> 0 <= s ''y'' \<and> s ''y'' \<le> n" 

65 
and f = "\<lambda>s. nat n  nat (s ''y'')"]) 

66 
apply(rule Semi) 

67 
prefer 2 

68 
apply(rule Assign) 

69 
apply(rule Assign') 

70 
apply (simp add: atLeastAtMostPlus1_int_conv algebra_simps) 

71 
apply clarsimp 

72 
apply arith 

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

73 
apply fastforce 
43158  74 
apply(rule Semi) 
75 
prefer 2 

76 
apply(rule Assign) 

77 
apply(rule Assign') 

78 
apply simp 

79 
done 

80 

81 

82 
text{* The soundness theorem: *} 

83 

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

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

86 
case (While P b f c) 

87 
show ?case 

88 
proof 

89 
fix s 

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

91 
proof(induct "f s" arbitrary: s rule: less_induct) 

92 
case (less n) 

93 
thus ?case by (metis While(2) WhileFalse WhileTrue) 

94 
qed 

95 
qed 

96 
next 

97 
case If thus ?case by auto blast 

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

98 
qed fastforce+ 
43158  99 

100 

101 
text{* 

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

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

104 
to take termination into account: *} 

105 

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

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

108 

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

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

111 

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

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

114 

115 
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)" 

116 
unfolding wpt_def 

117 
apply(rule ext) 

118 
apply auto 

119 
done 

120 

121 
lemma [simp]: 

122 
"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)" 

123 
apply(unfold wpt_def) 

124 
apply(rule ext) 

125 
apply auto 

126 
done 

127 

128 

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

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

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

132 

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

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

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

136 

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

138 

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

140 
proof(induct arbitrary: n' rule:Its.induct) 

141 
(* new release: 

142 
case Its_0 thus ?case by(metis Its.cases) 

143 
next 

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

145 
qed 

146 
*) 

147 
case Its_0 

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

149 
next 

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

151 
note C = this 

152 
from this(5) show ?case 

153 
proof cases 

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

155 
next 

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

157 
qed 

158 
qed 

159 

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

161 

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

163 
proof(induct "WHILE b DO c" s t rule: big_step_induct) 

164 
case WhileFalse thus ?case by (metis Its_0) 

165 
next 

166 
case WhileTrue thus ?case by (metis Its_Suc) 

167 
qed 

168 

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

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

171 

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

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

174 

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

176 

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

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

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

180 

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

182 
proof (induct c arbitrary: Q) 

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

184 
next 

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

186 
next 

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

188 
next 

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

190 
next 

191 
case (While b c) 

192 
let ?w = "WHILE b DO c" 

193 
{ fix n 

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

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

196 
unfolding wpt_def by (metis WhileE its_Suc lessI) 

197 
note strengthen_pre[OF this While] 

198 
} note hoaret.While[OF this] 

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

200 
ultimately show ?case by(rule weaken_post) 

201 
qed 

202 

203 

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

205 
termination argument. 

206 

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

208 
as for partial correctness: *} 

209 

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

211 
apply(rule strengthen_pre[OF _ wpt_is_pre]) 

212 
apply(auto simp: hoare_tvalid_def hoare_valid_def wpt_def) 

213 
done 

214 

215 
end 