30 our formulation of Hoare Logic. *} |
30 our formulation of Hoare Logic. *} |
31 |
31 |
32 text {* Using the basic @{text assign} rule directly is a bit |
32 text {* Using the basic @{text assign} rule directly is a bit |
33 cumbersome. *} |
33 cumbersome. *} |
34 |
34 |
35 lemma "|- .{\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) : .{\<acute>N = 10}.}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}." |
35 lemma "\<turnstile> \<lbrace>\<acute>(N_update (\<lambda>_. (2 * \<acute>N))) \<in> \<lbrace>\<acute>N = 10\<rbrace>\<rbrace> \<acute>N := 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>" |
36 by (rule assign) |
36 by (rule assign) |
37 |
37 |
38 text {* Certainly we want the state modification already done, e.g.\ |
38 text {* Certainly we want the state modification already done, e.g.\ |
39 by simplification. The \name{hoare} method performs the basic state |
39 by simplification. The \name{hoare} method performs the basic state |
40 update for us; we may apply the Simplifier afterwards to achieve |
40 update for us; we may apply the Simplifier afterwards to achieve |
41 ``obvious'' consequences as well. *} |
41 ``obvious'' consequences as well. *} |
42 |
42 |
43 lemma "|- .{True}. \<acute>N := 10 .{\<acute>N = 10}." |
43 lemma "\<turnstile> \<lbrace>True\<rbrace> \<acute>N := 10 \<lbrace>\<acute>N = 10\<rbrace>" |
44 by hoare |
44 by hoare |
45 |
45 |
46 lemma "|- .{2 * \<acute>N = 10}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}." |
46 lemma "\<turnstile> \<lbrace>2 * \<acute>N = 10\<rbrace> \<acute>N := 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>" |
47 by hoare |
47 by hoare |
48 |
48 |
49 lemma "|- .{\<acute>N = 5}. \<acute>N := 2 * \<acute>N .{\<acute>N = 10}." |
49 lemma "\<turnstile> \<lbrace>\<acute>N = 5\<rbrace> \<acute>N := 2 * \<acute>N \<lbrace>\<acute>N = 10\<rbrace>" |
50 by hoare simp |
50 by hoare simp |
51 |
51 |
52 lemma "|- .{\<acute>N + 1 = a + 1}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}." |
52 lemma "\<turnstile> \<lbrace>\<acute>N + 1 = a + 1\<rbrace> \<acute>N := \<acute>N + 1 \<lbrace>\<acute>N = a + 1\<rbrace>" |
53 by hoare |
53 by hoare |
54 |
54 |
55 lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N + 1 .{\<acute>N = a + 1}." |
55 lemma "\<turnstile> \<lbrace>\<acute>N = a\<rbrace> \<acute>N := \<acute>N + 1 \<lbrace>\<acute>N = a + 1\<rbrace>" |
56 by hoare simp |
56 by hoare simp |
57 |
57 |
58 lemma "|- .{a = a & b = b}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}." |
58 lemma "\<turnstile> \<lbrace>a = a \<and> b = b\<rbrace> \<acute>M := a; \<acute>N := b \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>" |
59 by hoare |
59 by hoare |
60 |
60 |
61 lemma "|- .{True}. \<acute>M := a; \<acute>N := b .{\<acute>M = a & \<acute>N = b}." |
61 lemma "\<turnstile> \<lbrace>True\<rbrace> \<acute>M := a; \<acute>N := b \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace>" |
62 by hoare simp |
62 by hoare simp |
63 |
63 |
64 lemma |
64 lemma |
65 "|- .{\<acute>M = a & \<acute>N = b}. |
65 "\<turnstile> \<lbrace>\<acute>M = a \<and> \<acute>N = b\<rbrace> |
66 \<acute>I := \<acute>M; \<acute>M := \<acute>N; \<acute>N := \<acute>I |
66 \<acute>I := \<acute>M; \<acute>M := \<acute>N; \<acute>N := \<acute>I |
67 .{\<acute>M = b & \<acute>N = a}." |
67 \<lbrace>\<acute>M = b \<and> \<acute>N = a\<rbrace>" |
68 by hoare simp |
68 by hoare simp |
69 |
69 |
70 text {* It is important to note that statements like the following one |
70 text {* It is important to note that statements like the following one |
71 can only be proven for each individual program variable. Due to the |
71 can only be proven for each individual program variable. Due to the |
72 extra-logical nature of record fields, we cannot formulate a theorem |
72 extra-logical nature of record fields, we cannot formulate a theorem |
73 relating record selectors and updates schematically. *} |
73 relating record selectors and updates schematically. *} |
74 |
74 |
75 lemma "|- .{\<acute>N = a}. \<acute>N := \<acute>N .{\<acute>N = a}." |
75 lemma "\<turnstile> \<lbrace>\<acute>N = a\<rbrace> \<acute>N := \<acute>N \<lbrace>\<acute>N = a\<rbrace>" |
76 by hoare |
76 by hoare |
77 |
77 |
78 lemma "|- .{\<acute>x = a}. \<acute>x := \<acute>x .{\<acute>x = a}." |
78 lemma "\<turnstile> \<lbrace>\<acute>x = a\<rbrace> \<acute>x := \<acute>x \<lbrace>\<acute>x = a\<rbrace>" |
79 oops |
79 oops |
80 |
80 |
81 lemma |
81 lemma |
82 "Valid {s. x s = a} (Basic (\<lambda>s. x_update (x s) s)) {s. x s = n}" |
82 "Valid {s. x s = a} (Basic (\<lambda>s. x_update (x s) s)) {s. x s = n}" |
83 -- {* same statement without concrete syntax *} |
83 -- {* same statement without concrete syntax *} |
86 |
86 |
87 text {* In the following assignments we make use of the consequence |
87 text {* In the following assignments we make use of the consequence |
88 rule in order to achieve the intended precondition. Certainly, the |
88 rule in order to achieve the intended precondition. Certainly, the |
89 \name{hoare} method is able to handle this case, too. *} |
89 \name{hoare} method is able to handle this case, too. *} |
90 |
90 |
91 lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." |
91 lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>" |
92 proof - |
92 proof - |
93 have ".{\<acute>M = \<acute>N}. <= .{\<acute>M + 1 ~= \<acute>N}." |
93 have "\<lbrace>\<acute>M = \<acute>N\<rbrace> \<subseteq> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace>" |
94 by auto |
94 by auto |
95 also have "|- ... \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." |
95 also have "\<turnstile> \<dots> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>" |
96 by hoare |
96 by hoare |
97 finally show ?thesis . |
97 finally show ?thesis . |
98 qed |
98 qed |
99 |
99 |
100 lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." |
100 lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>" |
101 proof - |
101 proof - |
102 have "!!m n::nat. m = n --> m + 1 ~= n" |
102 have "\<And>m n::nat. m = n \<longrightarrow> m + 1 \<noteq> n" |
103 -- {* inclusion of assertions expressed in ``pure'' logic, *} |
103 -- {* inclusion of assertions expressed in ``pure'' logic, *} |
104 -- {* without mentioning the state space *} |
104 -- {* without mentioning the state space *} |
105 by simp |
105 by simp |
106 also have "|- .{\<acute>M + 1 ~= \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." |
106 also have "\<turnstile> \<lbrace>\<acute>M + 1 \<noteq> \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>" |
107 by hoare |
107 by hoare |
108 finally show ?thesis . |
108 finally show ?thesis . |
109 qed |
109 qed |
110 |
110 |
111 lemma "|- .{\<acute>M = \<acute>N}. \<acute>M := \<acute>M + 1 .{\<acute>M ~= \<acute>N}." |
111 lemma "\<turnstile> \<lbrace>\<acute>M = \<acute>N\<rbrace> \<acute>M := \<acute>M + 1 \<lbrace>\<acute>M \<noteq> \<acute>N\<rbrace>" |
112 by hoare simp |
112 by hoare simp |
113 |
113 |
114 |
114 |
115 subsection {* Multiplication by addition *} |
115 subsection {* Multiplication by addition *} |
116 |
116 |
118 programs. This one is a loop for calculating the product of two |
118 programs. This one is a loop for calculating the product of two |
119 natural numbers, by iterated addition. We first give detailed |
119 natural numbers, by iterated addition. We first give detailed |
120 structured proof based on single-step Hoare rules. *} |
120 structured proof based on single-step Hoare rules. *} |
121 |
121 |
122 lemma |
122 lemma |
123 "|- .{\<acute>M = 0 & \<acute>S = 0}. |
123 "\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> |
124 WHILE \<acute>M ~= a |
124 WHILE \<acute>M \<noteq> a |
125 DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD |
125 DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD |
126 .{\<acute>S = a * b}." |
126 \<lbrace>\<acute>S = a * b\<rbrace>" |
127 proof - |
127 proof - |
128 let "|- _ ?while _" = ?thesis |
128 let "\<turnstile> _ ?while _" = ?thesis |
129 let ".{\<acute>?inv}." = ".{\<acute>S = \<acute>M * b}." |
129 let "\<lbrace>\<acute>?inv\<rbrace>" = "\<lbrace>\<acute>S = \<acute>M * b\<rbrace>" |
130 |
130 |
131 have ".{\<acute>M = 0 & \<acute>S = 0}. <= .{\<acute>?inv}." by auto |
131 have "\<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> \<subseteq> \<lbrace>\<acute>?inv\<rbrace>" by auto |
132 also have "|- ... ?while .{\<acute>?inv & ~ (\<acute>M ~= a)}." |
132 also have "\<turnstile> \<dots> ?while \<lbrace>\<acute>?inv \<and> \<not> (\<acute>M \<noteq> a)\<rbrace>" |
133 proof |
133 proof |
134 let ?c = "\<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1" |
134 let ?c = "\<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1" |
135 have ".{\<acute>?inv & \<acute>M ~= a}. <= .{\<acute>S + b = (\<acute>M + 1) * b}." |
135 have "\<lbrace>\<acute>?inv \<and> \<acute>M \<noteq> a\<rbrace> \<subseteq> \<lbrace>\<acute>S + b = (\<acute>M + 1) * b\<rbrace>" |
136 by auto |
136 by auto |
137 also have "|- ... ?c .{\<acute>?inv}." by hoare |
137 also have "\<turnstile> \<dots> ?c \<lbrace>\<acute>?inv\<rbrace>" by hoare |
138 finally show "|- .{\<acute>?inv & \<acute>M ~= a}. ?c .{\<acute>?inv}." . |
138 finally show "\<turnstile> \<lbrace>\<acute>?inv \<and> \<acute>M \<noteq> a\<rbrace> ?c \<lbrace>\<acute>?inv\<rbrace>" . |
139 qed |
139 qed |
140 also have "... <= .{\<acute>S = a * b}." by auto |
140 also have "\<dots> \<subseteq> \<lbrace>\<acute>S = a * b\<rbrace>" by auto |
141 finally show ?thesis . |
141 finally show ?thesis . |
142 qed |
142 qed |
143 |
143 |
144 text {* The subsequent version of the proof applies the @{text hoare} |
144 text {* The subsequent version of the proof applies the @{text hoare} |
145 method to reduce the Hoare statement to a purely logical problem |
145 method to reduce the Hoare statement to a purely logical problem |
146 that can be solved fully automatically. Note that we have to |
146 that can be solved fully automatically. Note that we have to |
147 specify the \texttt{WHILE} loop invariant in the original statement. *} |
147 specify the \texttt{WHILE} loop invariant in the original statement. *} |
148 |
148 |
149 lemma |
149 lemma |
150 "|- .{\<acute>M = 0 & \<acute>S = 0}. |
150 "\<turnstile> \<lbrace>\<acute>M = 0 \<and> \<acute>S = 0\<rbrace> |
151 WHILE \<acute>M ~= a |
151 WHILE \<acute>M \<noteq> a |
152 INV .{\<acute>S = \<acute>M * b}. |
152 INV \<lbrace>\<acute>S = \<acute>M * b\<rbrace> |
153 DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD |
153 DO \<acute>S := \<acute>S + b; \<acute>M := \<acute>M + 1 OD |
154 .{\<acute>S = a * b}." |
154 \<lbrace>\<acute>S = a * b\<rbrace>" |
155 by hoare auto |
155 by hoare auto |
156 |
156 |
157 |
157 |
158 subsection {* Summing natural numbers *} |
158 subsection {* Summing natural numbers *} |
159 |
159 |
166 care of assignment and sequential composition. Note that we express |
166 care of assignment and sequential composition. Note that we express |
167 intermediate proof obligation in pure logic, without referring to |
167 intermediate proof obligation in pure logic, without referring to |
168 the state space. *} |
168 the state space. *} |
169 |
169 |
170 theorem |
170 theorem |
171 "|- .{True}. |
171 "\<turnstile> \<lbrace>True\<rbrace> |
172 \<acute>S := 0; \<acute>I := 1; |
172 \<acute>S := 0; \<acute>I := 1; |
173 WHILE \<acute>I ~= n |
173 WHILE \<acute>I \<noteq> n |
174 DO |
174 DO |
175 \<acute>S := \<acute>S + \<acute>I; |
175 \<acute>S := \<acute>S + \<acute>I; |
176 \<acute>I := \<acute>I + 1 |
176 \<acute>I := \<acute>I + 1 |
177 OD |
177 OD |
178 .{\<acute>S = (SUM j<n. j)}." |
178 \<lbrace>\<acute>S = (\<Sum>j<n. j)\<rbrace>" |
179 (is "|- _ (_; ?while) _") |
179 (is "\<turnstile> _ (_; ?while) _") |
180 proof - |
180 proof - |
181 let ?sum = "\<lambda>k::nat. SUM j<k. j" |
181 let ?sum = "\<lambda>k::nat. \<Sum>j<k. j" |
182 let ?inv = "\<lambda>s i::nat. s = ?sum i" |
182 let ?inv = "\<lambda>s i::nat. s = ?sum i" |
183 |
183 |
184 have "|- .{True}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}." |
184 have "\<turnstile> \<lbrace>True\<rbrace> \<acute>S := 0; \<acute>I := 1 \<lbrace>?inv \<acute>S \<acute>I\<rbrace>" |
185 proof - |
185 proof - |
186 have "True --> 0 = ?sum 1" |
186 have "True \<longrightarrow> 0 = ?sum 1" |
187 by simp |
187 by simp |
188 also have "|- .{...}. \<acute>S := 0; \<acute>I := 1 .{?inv \<acute>S \<acute>I}." |
188 also have "\<turnstile> \<lbrace>\<dots>\<rbrace> \<acute>S := 0; \<acute>I := 1 \<lbrace>?inv \<acute>S \<acute>I\<rbrace>" |
189 by hoare |
189 by hoare |
190 finally show ?thesis . |
190 finally show ?thesis . |
191 qed |
191 qed |
192 also have "|- ... ?while .{?inv \<acute>S \<acute>I & ~ \<acute>I ~= n}." |
192 also have "\<turnstile> \<dots> ?while \<lbrace>?inv \<acute>S \<acute>I \<and> \<not> \<acute>I \<noteq> n\<rbrace>" |
193 proof |
193 proof |
194 let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1" |
194 let ?body = "\<acute>S := \<acute>S + \<acute>I; \<acute>I := \<acute>I + 1" |
195 have "!!s i. ?inv s i & i ~= n --> ?inv (s + i) (i + 1)" |
195 have "\<And>s i. ?inv s i \<and> i \<noteq> n \<longrightarrow> ?inv (s + i) (i + 1)" |
196 by simp |
196 by simp |
197 also have "|- .{\<acute>S + \<acute>I = ?sum (\<acute>I + 1)}. ?body .{?inv \<acute>S \<acute>I}." |
197 also have "\<turnstile> \<lbrace>\<acute>S + \<acute>I = ?sum (\<acute>I + 1)\<rbrace> ?body \<lbrace>?inv \<acute>S \<acute>I\<rbrace>" |
198 by hoare |
198 by hoare |
199 finally show "|- .{?inv \<acute>S \<acute>I & \<acute>I ~= n}. ?body .{?inv \<acute>S \<acute>I}." . |
199 finally show "\<turnstile> \<lbrace>?inv \<acute>S \<acute>I \<and> \<acute>I \<noteq> n\<rbrace> ?body \<lbrace>?inv \<acute>S \<acute>I\<rbrace>" . |
200 qed |
200 qed |
201 also have "!!s i. s = ?sum i & ~ i ~= n --> s = ?sum n" |
201 also have "\<And>s i. s = ?sum i \<and> \<not> i \<noteq> n \<longrightarrow> s = ?sum n" |
202 by simp |
202 by simp |
203 finally show ?thesis . |
203 finally show ?thesis . |
204 qed |
204 qed |
205 |
205 |
206 text {* The next version uses the @{text hoare} method, while still |
206 text {* The next version uses the @{text hoare} method, while still |
207 explaining the resulting proof obligations in an abstract, |
207 explaining the resulting proof obligations in an abstract, |
208 structured manner. *} |
208 structured manner. *} |
209 |
209 |
210 theorem |
210 theorem |
211 "|- .{True}. |
211 "\<turnstile> \<lbrace>True\<rbrace> |
212 \<acute>S := 0; \<acute>I := 1; |
212 \<acute>S := 0; \<acute>I := 1; |
213 WHILE \<acute>I ~= n |
213 WHILE \<acute>I \<noteq> n |
214 INV .{\<acute>S = (SUM j<\<acute>I. j)}. |
214 INV \<lbrace>\<acute>S = (\<Sum>j<\<acute>I. j)\<rbrace> |
215 DO |
215 DO |
216 \<acute>S := \<acute>S + \<acute>I; |
216 \<acute>S := \<acute>S + \<acute>I; |
217 \<acute>I := \<acute>I + 1 |
217 \<acute>I := \<acute>I + 1 |
218 OD |
218 OD |
219 .{\<acute>S = (SUM j<n. j)}." |
219 \<lbrace>\<acute>S = (\<Sum>j<n. j)\<rbrace>" |
220 proof - |
220 proof - |
221 let ?sum = "\<lambda>k::nat. SUM j<k. j" |
221 let ?sum = "\<lambda>k::nat. \<Sum>j<k. j" |
222 let ?inv = "\<lambda>s i::nat. s = ?sum i" |
222 let ?inv = "\<lambda>s i::nat. s = ?sum i" |
223 |
223 |
224 show ?thesis |
224 show ?thesis |
225 proof hoare |
225 proof hoare |
226 show "?inv 0 1" by simp |
226 show "?inv 0 1" by simp |
227 next |
227 next |
228 fix s i assume "?inv s i & i ~= n" |
228 fix s i |
|
229 assume "?inv s i \<and> i \<noteq> n" |
229 then show "?inv (s + i) (i + 1)" by simp |
230 then show "?inv (s + i) (i + 1)" by simp |
230 next |
231 next |
231 fix s i assume "?inv s i & ~ i ~= n" |
232 fix s i |
|
233 assume "?inv s i \<and> \<not> i \<noteq> n" |
232 then show "s = ?sum n" by simp |
234 then show "s = ?sum n" by simp |
233 qed |
235 qed |
234 qed |
236 qed |
235 |
237 |
236 text {* Certainly, this proof may be done fully automatic as well, |
238 text {* Certainly, this proof may be done fully automatic as well, |
237 provided that the invariant is given beforehand. *} |
239 provided that the invariant is given beforehand. *} |
238 |
240 |
239 theorem |
241 theorem |
240 "|- .{True}. |
242 "\<turnstile> \<lbrace>True\<rbrace> |
241 \<acute>S := 0; \<acute>I := 1; |
243 \<acute>S := 0; \<acute>I := 1; |
242 WHILE \<acute>I ~= n |
244 WHILE \<acute>I \<noteq> n |
243 INV .{\<acute>S = (SUM j<\<acute>I. j)}. |
245 INV \<lbrace>\<acute>S = (\<Sum>j<\<acute>I. j)\<rbrace> |
244 DO |
246 DO |
245 \<acute>S := \<acute>S + \<acute>I; |
247 \<acute>S := \<acute>S + \<acute>I; |
246 \<acute>I := \<acute>I + 1 |
248 \<acute>I := \<acute>I + 1 |
247 OD |
249 OD |
248 .{\<acute>S = (SUM j<n. j)}." |
250 \<lbrace>\<acute>S = (\<Sum>j<n. j)\<rbrace>" |
249 by hoare auto |
251 by hoare auto |
250 |
252 |
251 |
253 |
252 subsection {* Time *} |
254 subsection {* Time *} |
253 |
255 |
271 |
273 |
272 lemma lem: "(0::nat) < n \<Longrightarrow> n + n \<le> Suc (n * n)" |
274 lemma lem: "(0::nat) < n \<Longrightarrow> n + n \<le> Suc (n * n)" |
273 by (induct n) simp_all |
275 by (induct n) simp_all |
274 |
276 |
275 lemma |
277 lemma |
276 "|- .{i = \<acute>I & \<acute>time = 0}. |
278 "\<turnstile> \<lbrace>i = \<acute>I \<and> \<acute>time = 0\<rbrace> |
277 timeit ( |
279 (timeit |
278 WHILE \<acute>I \<noteq> 0 |
280 (WHILE \<acute>I \<noteq> 0 |
279 INV .{2 *\<acute> time + \<acute>I * \<acute>I + 5 * \<acute>I = i * i + 5 * i}. |
281 INV \<lbrace>2 *\<acute> time + \<acute>I * \<acute>I + 5 * \<acute>I = i * i + 5 * i\<rbrace> |
280 DO |
282 DO |
281 \<acute>J := \<acute>I; |
283 \<acute>J := \<acute>I; |
282 WHILE \<acute>J \<noteq> 0 |
284 WHILE \<acute>J \<noteq> 0 |
283 INV .{0 < \<acute>I & 2 * \<acute>time + \<acute>I * \<acute>I + 3 * \<acute>I + 2 * \<acute>J - 2 = i * i + 5 * i}. |
285 INV \<lbrace>0 < \<acute>I \<and> 2 * \<acute>time + \<acute>I * \<acute>I + 3 * \<acute>I + 2 * \<acute>J - 2 = i * i + 5 * i\<rbrace> |
284 DO \<acute>J := \<acute>J - 1 OD; |
286 DO \<acute>J := \<acute>J - 1 OD; |
285 \<acute>I := \<acute>I - 1 |
287 \<acute>I := \<acute>I - 1 |
286 OD |
288 OD)) |
287 ) .{2*\<acute>time = i*i + 5*i}." |
289 \<lbrace>2 * \<acute>time = i * i + 5 * i\<rbrace>" |
288 apply simp |
290 apply simp |
289 apply hoare |
291 apply hoare |
290 apply simp |
292 apply simp |
291 apply clarsimp |
293 apply clarsimp |
292 apply clarsimp |
294 apply clarsimp |