43158
|
1 |
header{* Hoare Logic for Total Correctness *}
|
|
2 |
|
|
3 |
theory HoareT imports Hoare_Sound_Complete Util begin
|
|
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
|
|
73 |
apply fastsimp
|
|
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
|
|
98 |
qed fastsimp+
|
|
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
|