1 (* ========================================================================= *)
2 (* Simple WHILE-language with relational semantics. *)
3 (* ========================================================================= *)
7 parse_as_infix("refined",(12,"right"));;
9 (* ------------------------------------------------------------------------- *)
10 (* Logical operations "lifted" to predicates, for readability. *)
11 (* ------------------------------------------------------------------------- *)
13 parse_as_infix("AND",(20,"right"));;
14 parse_as_infix("OR",(16,"right"));;
15 parse_as_infix("IMP",(13,"right"));;
16 parse_as_infix("IMPLIES",(12,"right"));;
18 let FALSE = new_definition
21 let TRUE = new_definition
24 let NOT = new_definition
25 `NOT p = \x:S. ~(p x)`;;
27 let AND = new_definition
28 `p AND q = \x:S. p x /\ q x`;;
30 let OR = new_definition
31 `p OR q = \x:S. p x \/ q x`;;
33 let ANDS = new_definition
34 `ANDS P = \x:S. !p. P p ==> p x`;;
36 let ORS = new_definition
37 `ORS P = \x:S. ?p. P p /\ p x`;;
39 let IMP = new_definition
40 `p IMP q = \x:S. p x ==> q x`;;
42 (* ------------------------------------------------------------------------- *)
43 (* This one is different, corresponding to "subset". *)
44 (* ------------------------------------------------------------------------- *)
46 let IMPLIES = new_definition
47 `p IMPLIES q <=> !x:S. p x ==> q x`;;
49 (* ------------------------------------------------------------------------- *)
50 (* Simple procedure to prove tautologies at the predicate level. *)
51 (* ------------------------------------------------------------------------- *)
55 REWRITE_TAC[FALSE; TRUE; NOT; AND; OR; ANDS; ORS; IMP;
56 IMPLIES; FUN_EQ_THM] THEN MESON_TAC[] in
57 fun tm -> prove(tm,tac);;
59 (* ------------------------------------------------------------------------- *)
60 (* Some applications. *)
61 (* ------------------------------------------------------------------------- *)
63 let IMPLIES_TRANS = PRED_TAUT
64 `!p q r. p IMPLIES q /\ q IMPLIES r ==> p IMPLIES r`;;
66 (* ------------------------------------------------------------------------- *)
67 (* Enumerated type of basic commands, and other derived commands. *)
68 (* ------------------------------------------------------------------------- *)
70 parse_as_infix("Seq",(26,"right"));;
72 let command_INDUCTION,command_RECURSION = define_type
73 "command = Assign (S->S)
75 | Ite (S->bool) command command
76 | While (S->bool) command";;
78 let SKIP = new_definition
81 let ABORT = new_definition
82 `ABORT = While TRUE SKIP`;;
84 let IF = new_definition
85 `IF e c = Ite e c SKIP`;;
87 let DO = new_definition
88 `DO c e = c Seq (While e c)`;;
90 let ASSERT = new_definition
91 `ASSERT g = Ite g SKIP ABORT`;;
93 (* ------------------------------------------------------------------------- *)
94 (* Annotation commands, to allow insertion of loop (in)variants. *)
95 (* ------------------------------------------------------------------------- *)
97 let AWHILE = new_definition
98 `AWHILE (i:S->bool) (v:S->S->bool) (e:S->bool) c = While e c`;;
100 let ADO = new_definition
101 `ADO (i:S->bool) (v:S->S->bool) c (e:S->bool) = DO c e`;;
103 (* ------------------------------------------------------------------------- *)
104 (* Useful properties of type constructors for commands. *)
105 (* ------------------------------------------------------------------------- *)
107 let command_DISTINCT =
108 distinctness "command";;
110 let command_INJECTIVE =
111 injectivity "command";;
113 (* ------------------------------------------------------------------------- *)
114 (* Relational semantics of commands. *)
115 (* ------------------------------------------------------------------------- *)
117 let sem_RULES,sem_INDUCT,sem_CASES = new_inductive_definition
118 `(!f s. sem(Assign f) s (f s)) /\
119 (!c1 c2 s s' s''. sem(c1) s s' /\ sem(c2) s' s''
120 ==> sem(c1 Seq c2) s s'') /\
121 (!e c1 c2 s s'. e s /\ sem(c1) s s' ==> sem(Ite e c1 c2) s s') /\
122 (!e c1 c2 s s'. ~(e s) /\ sem(c2) s s' ==> sem(Ite e c1 c2) s s') /\
123 (!e c s. ~(e s) ==> sem(While e c) s s) /\
124 (!e c s s' s''. e s /\ sem(c) s s' /\ sem(While e c) s' s''
125 ==> sem(While e c) s s'')`;;
127 (* ------------------------------------------------------------------------- *)
128 (* A more "denotational" view of the semantics. *)
129 (* ------------------------------------------------------------------------- *)
131 let SEM_ASSIGN = prove
132 (`sem(Assign f) s s' <=> (s' = f s)`,
133 GEN_REWRITE_TAC LAND_CONV [sem_CASES] THEN
134 REWRITE_TAC[command_DISTINCT; command_INJECTIVE] THEN MESON_TAC[]);;
137 (`sem(c1 Seq c2) s s' <=> ?s''. sem c1 s s'' /\ sem c2 s'' s'`,
138 GEN_REWRITE_TAC LAND_CONV [sem_CASES] THEN
139 REWRITE_TAC[command_DISTINCT; command_INJECTIVE] THEN MESON_TAC[]);;
142 (`sem(Ite e c1 c2) s s' <=> e s /\ sem c1 s s' \/
143 ~(e s) /\ sem c2 s s'`,
144 GEN_REWRITE_TAC LAND_CONV [sem_CASES] THEN
145 REWRITE_TAC[command_DISTINCT; command_INJECTIVE] THEN MESON_TAC[]);;
148 (`sem(SKIP) s s' <=> (s' = s)`,
149 REWRITE_TAC[SKIP; SEM_ASSIGN; I_THM]);;
152 (`sem(IF e c) s s' <=> e s /\ sem c s s' \/ ~(e s) /\ (s = s')`,
153 REWRITE_TAC[IF; SEM_ITE; SEM_SKIP; EQ_SYM_EQ]);;
155 let SEM_WHILE = prove
156 (`sem(While e c) s s' <=> sem(IF e (c Seq While e c)) s s'`,
157 GEN_REWRITE_TAC LAND_CONV [sem_CASES] THEN
158 REWRITE_TAC[FUN_EQ_THM; SEM_IF; SEM_SEQ] THEN REPEAT GEN_TAC THEN
159 REWRITE_TAC[command_DISTINCT; command_INJECTIVE] THEN MESON_TAC[]);;
161 let SEM_ABORT = prove
162 (`sem(ABORT) s s' <=> F`,
164 (`!c s s'. sem c s s' ==> ~(c = ABORT)`,
165 MATCH_MP_TAC sem_INDUCT THEN
166 REWRITE_TAC[command_DISTINCT; command_INJECTIVE; ABORT] THEN
167 REWRITE_TAC[FUN_EQ_THM; TRUE] THEN MESON_TAC[]) in
171 (`sem(DO c e) s s' <=> sem(c Seq IF e (DO c e)) s s'`,
172 REWRITE_TAC[DO; SEM_SEQ; GSYM SEM_WHILE]);;
174 let SEM_ASSERT = prove
175 (`sem(ASSERT g) s s' <=> g s /\ (s' = s)`,
176 REWRITE_TAC[ASSERT; SEM_ITE; SEM_SKIP; SEM_ABORT]);;
178 (* ------------------------------------------------------------------------- *)
179 (* Proofs that all commands are deterministic. *)
180 (* ------------------------------------------------------------------------- *)
182 let deterministic = new_definition
183 `deterministic r <=> !s s1 s2. r s s1 /\ r s s2 ==> (s1 = s2)`;;
185 let DETERMINISM = prove
186 (`!c:(S)command. deterministic(sem c)`,
187 REWRITE_TAC[deterministic] THEN SUBGOAL_THEN
188 `!c s s1. sem c s s1 ==> !s2:S. sem c s s2 ==> (s1 = s2)`
189 (fun th -> MESON_TAC[th]) THEN
190 MATCH_MP_TAC sem_INDUCT THEN CONJ_TAC THENL
191 [ALL_TAC; REPEAT CONJ_TAC THEN REPEAT GEN_TAC THEN DISCH_TAC] THEN
192 REPEAT GEN_TAC THEN ONCE_REWRITE_TAC[sem_CASES] THEN
193 REWRITE_TAC[command_DISTINCT; command_INJECTIVE] THEN
196 (* ------------------------------------------------------------------------- *)
197 (* Termination, weakest liberal precondition and weakest precondition. *)
198 (* ------------------------------------------------------------------------- *)
200 let terminates = new_definition
201 `terminates c s <=> ?s'. sem c s s'`;;
203 let wlp = new_definition
204 `wlp c q s <=> !s'. sem c s s' ==> q s'`;;
206 let wp = new_definition
207 `wp c q s <=> terminates c s /\ wlp c q s`;;
209 (* ------------------------------------------------------------------------- *)
210 (* Dijkstra's healthiness conditions (the last because of determinism). *)
211 (* ------------------------------------------------------------------------- *)
214 (`!c. (wp c FALSE = FALSE)`,
215 REWRITE_TAC[FUN_EQ_THM; wp; wlp; terminates; FALSE] THEN MESON_TAC[]);;
217 let WP_MONOTONIC = prove
218 (`q IMPLIES r ==> wp c q IMPLIES wp c r`,
219 REWRITE_TAC[IMPLIES; wp; wlp; terminates] THEN MESON_TAC[]);;
221 let WP_CONJUNCTIVE = prove
222 (`(wp c q) AND (wp c r) = wp c (q AND r)`,
223 REWRITE_TAC[FUN_EQ_THM; wp; wlp; terminates; AND] THEN MESON_TAC[]);;
225 let WP_DISJUNCTIVE = prove
226 (`(wp c p) OR (wp c q) = wp c (p OR q)`,
227 REWRITE_TAC[FUN_EQ_THM; wp; wlp; OR; terminates] THEN
228 MESON_TAC[REWRITE_RULE[deterministic] DETERMINISM]);;
230 (* ------------------------------------------------------------------------- *)
231 (* Weakest preconditions for the primitive and derived commands. *)
232 (* ------------------------------------------------------------------------- *)
234 let WP_ASSIGN = prove
235 (`!f q. wp (Assign f) q = q o f`,
236 REWRITE_TAC[wp; wlp; terminates; o_THM; FUN_EQ_THM; SEM_ASSIGN] THEN
240 (`!c1 c2 q. wp (c1 Seq c2) q = wp c1 (wp c2 q)`,
241 REWRITE_TAC[wp; wlp; terminates; SEM_SEQ; FUN_EQ_THM] THEN
242 MESON_TAC[REWRITE_RULE[deterministic] DETERMINISM]);;
245 (`!e c1 c2 q. wp (Ite e c1 c2) q = (e AND wp c1 q) OR (NOT e AND wp c2 q)`,
246 REWRITE_TAC[wp; wlp; terminates; SEM_ITE; FUN_EQ_THM; AND; OR; NOT] THEN
250 (`!e c. wp (IF e (c Seq While e c)) q = wp (While e c) q`,
251 REWRITE_TAC[FUN_EQ_THM; wp; wlp; terminates; GSYM SEM_WHILE]);;
254 (`!q. wp SKIP q = q`,
255 REWRITE_TAC[FUN_EQ_THM; SKIP; WP_ASSIGN; I_THM; o_THM]);;
258 (`!q. wp ABORT q = FALSE`,
259 REWRITE_TAC[FUN_EQ_THM; wp; wlp; terminates; SEM_ABORT; FALSE]);;
262 (`!e c q. wp (IF e c) q = (e AND wp c q) OR (NOT e AND q)`,
263 REWRITE_TAC[IF; WP_ITE; WP_SKIP]);;
266 (`!e c. wp (c Seq IF e (DO c e)) q = wp (DO c e) q`,
267 REWRITE_TAC[FUN_EQ_THM; wp; wlp; terminates; GSYM SEM_DO]);;
269 let WP_ASSERT = prove
270 (`!g q. wp (ASSERT g) q = g AND q`,
271 REWRITE_TAC[wp; wlp; terminates; SEM_ASSERT; FUN_EQ_THM; AND] THEN
274 (* ------------------------------------------------------------------------- *)
275 (* Rules for total correctness. *)
276 (* ------------------------------------------------------------------------- *)
278 let correct = new_definition
279 `correct p c q <=> p IMPLIES (wp c q)`;;
281 let CORRECT_PRESTRENGTH = prove
282 (`!p p' c q. p IMPLIES p' /\ correct p' c q ==> correct p c q`,
283 REWRITE_TAC[correct; IMPLIES_TRANS]);;
285 let CORRECT_POSTWEAK = prove
286 (`!p c q q'. correct p c q' /\ q' IMPLIES q ==> correct p c q`,
287 REWRITE_TAC[correct] THEN MESON_TAC[WP_MONOTONIC; IMPLIES_TRANS]);;
289 let CORRECT_ASSIGN = prove
290 (`!p f q. (p IMPLIES (\s. q(f s))) ==> correct p (Assign f) q`,
291 REWRITE_TAC[correct; WP_ASSIGN; IMPLIES; o_THM]);;
293 let CORRECT_SEQ = prove
295 correct p c1 r /\ correct r c2 q ==> correct p (c1 Seq c2) q`,
296 REWRITE_TAC[correct; WP_SEQ; o_THM] THEN
297 MESON_TAC[WP_MONOTONIC; IMPLIES_TRANS]);;
299 let CORRECT_ITE = prove
301 correct (p AND e) c1 q /\ correct (p AND (NOT e)) c2 q
302 ==> correct p (Ite e c1 c2) q`,
303 REWRITE_TAC[correct; WP_ITE; AND; NOT; IMPLIES; OR] THEN MESON_TAC[]);;
305 let CORRECT_WHILE = prove
306 (`! (<<) p c q e invariant.
308 p IMPLIES invariant /\
309 (NOT e) AND invariant IMPLIES q /\
311 (invariant AND e AND (\s. X = s)) c (invariant AND (\s. s << X)))
312 ==> correct p (While e c) q`,
313 REWRITE_TAC[correct; IMPLIES; IN; AND; NOT] THEN REPEAT STRIP_TAC THEN
314 SUBGOAL_THEN `!s:S. invariant s ==> wp (While e c) q s` MP_TAC THENL
315 [ALL_TAC; ASM_MESON_TAC[]] THEN
316 FIRST_ASSUM(MATCH_MP_TAC o REWRITE_RULE[WF_IND]) THEN
317 X_GEN_TAC `s:S` THEN REPEAT DISCH_TAC THEN
318 ONCE_REWRITE_TAC[GSYM WP_WHILE] THEN
319 REWRITE_TAC[WP_IF; WP_SEQ; AND; OR; NOT; o_THM] THEN
320 ASM_CASES_TAC `(e:S->bool) s` THEN ASM_REWRITE_TAC[] THENL
321 [ALL_TAC; ASM_MESON_TAC[]] THEN
322 SUBGOAL_THEN `wp c (\x:S. invariant x /\ x << s) (s:S) :bool` MP_TAC THENL
323 [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]; ALL_TAC] THEN
324 SUBGOAL_THEN `(\x:S. invariant x /\ x << (s:S)) IMPLIES wp (While e c) q`
325 MP_TAC THENL [REWRITE_TAC[IMPLIES] THEN ASM_MESON_TAC[]; ALL_TAC] THEN
326 MESON_TAC[WP_MONOTONIC; IMPLIES]);;
328 let CORRECT_SKIP = prove
329 (`!p q. (p IMPLIES q) ==> correct p SKIP q`,
330 REWRITE_TAC[correct; WP_SKIP]);;
332 let CORRECT_ABORT = prove
333 (`!p q. F ==> correct p ABORT q`,
336 let CORRECT_IF = prove
338 correct (p AND e) c q /\ (p AND (NOT e)) IMPLIES q
339 ==> correct p (IF e c) q`,
340 REWRITE_TAC[correct; WP_IF; AND; NOT; IMPLIES; OR] THEN MESON_TAC[]);;
342 let CORRECT_DO = prove
343 (`! (<<) p q c invariant.
345 (e AND invariant) IMPLIES p /\
346 ((NOT e) AND invariant) IMPLIES q /\
348 (p AND (\s. X = s)) c (invariant AND (\s. s << X)))
349 ==> correct p (DO c e) q`,
350 REPEAT STRIP_TAC THEN REWRITE_TAC[DO] THEN
351 MATCH_MP_TAC CORRECT_SEQ THEN EXISTS_TAC `invariant:S->bool` THEN
352 ASM_REWRITE_TAC[] THEN CONJ_TAC THENL
353 [POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
354 REWRITE_TAC[correct; GSYM WP_CONJUNCTIVE] THEN
355 REWRITE_TAC[AND; IMPLIES] THEN MESON_TAC[];
356 MATCH_MP_TAC CORRECT_WHILE THEN
357 MAP_EVERY EXISTS_TAC [`(<<) :S->S->bool`; `invariant:S->bool`] THEN
358 ASM_REWRITE_TAC[IMPLIES] THEN X_GEN_TAC `X:S` THEN
359 MATCH_MP_TAC CORRECT_PRESTRENGTH THEN
360 EXISTS_TAC `p AND (\s:S. X = s)` THEN ASM_REWRITE_TAC[] THEN
361 UNDISCH_TAC `(e:S->bool) AND invariant IMPLIES p` THEN
362 REWRITE_TAC[AND; IMPLIES] THEN MESON_TAC[]]);;
364 let CORRECT_ASSERT = prove
365 (`!p g q. p IMPLIES (g AND q) ==> correct p (ASSERT g) q`,
366 REWRITE_TAC[correct; WP_ASSERT]);;
368 (* ------------------------------------------------------------------------- *)
369 (* VCs for the basic commands (in fact only assign should be needed). *)
370 (* ------------------------------------------------------------------------- *)
372 let VC_ASSIGN = prove
373 (`p IMPLIES (q o f) ==> correct p (Assign f) q`,
374 REWRITE_TAC[o_DEF; CORRECT_ASSIGN]);;
377 (`p IMPLIES q ==> correct p SKIP q`,
378 REWRITE_TAC[CORRECT_SKIP]);;
381 (`F ==> correct p ABORT q`,
382 MATCH_ACCEPT_TAC CORRECT_ABORT);;
384 let VC_ASSERT = prove
385 (`p IMPLIES (b AND q) ==> correct p (ASSERT b) q`,
386 REWRITE_TAC[CORRECT_ASSERT]);;
388 (* ------------------------------------------------------------------------- *)
389 (* VCs for composite commands other than sequences. *)
390 (* ------------------------------------------------------------------------- *)
393 (`correct (p AND e) c1 q /\ correct (p AND NOT e) c2 q
394 ==> correct p (Ite e c1 c2) q`,
395 REWRITE_TAC[CORRECT_ITE]);;
398 (`correct (p AND e) c q /\ p AND NOT e IMPLIES q
399 ==> correct p (IF e c) q`,
400 REWRITE_TAC[CORRECT_IF]);;
402 let VC_AWHILE_VARIANT = prove
404 p IMPLIES invariant /\
405 (NOT e) AND invariant IMPLIES q /\
407 (invariant AND e AND (\s. X = s)) c (invariant AND (\s. s << X)))
408 ==> correct p (AWHILE invariant (<<) e c) q`,
409 REWRITE_TAC[AWHILE; CORRECT_WHILE]);;
411 let VC_AWHILE_MEASURE = prove
412 (`p IMPLIES invariant /\
413 (NOT e) AND invariant IMPLIES q /\
415 (invariant AND e AND (\s:S. X = m(s)))
417 (invariant AND (\s. m(s) < X)))
418 ==> correct p (AWHILE invariant (MEASURE m) e c) q`,
419 STRIP_TAC THEN MATCH_MP_TAC VC_AWHILE_VARIANT THEN
420 ASM_REWRITE_TAC[WF_MEASURE] THEN
421 X_GEN_TAC `X:S` THEN FIRST_ASSUM(MP_TAC o SPEC `(m:S->num) X`) THEN
422 REWRITE_TAC[correct; AND; IMPLIES; MEASURE] THEN MESON_TAC[]);;
424 let VC_ADO_VARIANT = prove
426 (e AND invariant) IMPLIES p /\
427 ((NOT e) AND invariant) IMPLIES q /\
429 (p AND (\s. X = s)) c (invariant AND (\s. s << X)))
430 ==> correct p (ADO invariant (<<) c e) q`,
431 REWRITE_TAC[ADO; CORRECT_DO]);;
433 let VC_ADO_MEASURE = prove
434 (`(e AND invariant) IMPLIES p /\
435 ((NOT e) AND invariant) IMPLIES q /\
437 (p AND (\s:S. X = m(s))) c (invariant AND (\s. m(s) < X)))
438 ==> correct p (ADO invariant (MEASURE m) c e) q`,
439 STRIP_TAC THEN MATCH_MP_TAC VC_ADO_VARIANT THEN
440 ASM_REWRITE_TAC[WF_MEASURE] THEN
441 X_GEN_TAC `X:S` THEN FIRST_ASSUM(MP_TAC o SPEC `(m:S->num) X`) THEN
442 REWRITE_TAC[correct; AND; IMPLIES; MEASURE] THEN MESON_TAC[]);;
444 (* ------------------------------------------------------------------------- *)
445 (* VCs for sequences of commands, using intelligence where possible. *)
446 (* ------------------------------------------------------------------------- *)
448 let VC_SEQ_ASSERT_LEFT = prove
449 (`p IMPLIES b /\ correct b c q ==> correct p (ASSERT b Seq c) q`,
450 MESON_TAC[CORRECT_SEQ; CORRECT_ASSERT; CORRECT_PRESTRENGTH;
451 PRED_TAUT `(p IMPLIES b) ==> (p IMPLIES b AND p)`]);;
453 let VC_SEQ_ASSERT_RIGHT = prove
454 (`correct p c b /\ b IMPLIES q ==> correct p (c Seq (ASSERT b)) q`,
455 MESON_TAC[CORRECT_SEQ; CORRECT_ASSERT;
456 PRED_TAUT `(p IMPLIES b) ==> (p IMPLIES p AND b)`]);;
458 let VC_SEQ_ASSERT_MIDDLE = prove
459 (`correct p c b /\ correct b c' q
460 ==> correct p (c Seq (ASSERT b) Seq c') q`,
461 MESON_TAC[CORRECT_SEQ; CORRECT_ASSERT; PRED_TAUT `b IMPLIES b AND b`]);;
463 let VC_SEQ_ASSIGN_LEFT = prove
464 (`(p o f = p) /\ (f o f = f) /\
465 correct (p AND (\s:S. s = f s)) c q
466 ==> correct p ((Assign f) Seq c) q`,
467 REWRITE_TAC[FUN_EQ_THM; o_THM] THEN STRIP_TAC THEN
468 MATCH_MP_TAC CORRECT_SEQ THEN EXISTS_TAC `p AND (\s:S. s = f s)` THEN
469 ASM_REWRITE_TAC[] THEN MATCH_MP_TAC VC_ASSIGN THEN
470 ASM_REWRITE_TAC[IMPLIES; AND; o_THM]);;
472 let VC_SEQ_ASSIGN_RIGHT = prove
473 (`correct p c (q o f) ==> correct p (c Seq (Assign f)) q`,
474 MESON_TAC[CORRECT_SEQ; VC_ASSIGN; PRED_TAUT `(p:S->bool) IMPLIES p`]);;
476 (* ------------------------------------------------------------------------- *)
477 (* Parser for correctness assertions. *)
478 (* ------------------------------------------------------------------------- *)
480 let rec dive_to_var ptm =
482 Varp(_,_) as vp -> vp | Typing(t,_) -> dive_to_var t | _ -> fail();;
484 let reserve_program_words,unreserve_program_words =
485 let words = ["var"; "end"; "skip"; "abort";
486 ":="; "if"; "then"; "else"; "while"; "do"] in
487 (fun () -> reserve_words words),
488 (fun () -> unreserve_words words);;
490 reserve_program_words();;
492 let parse_program,parse_program_assertion =
493 let assign_ptm = Varp("Assign",dpty)
494 and seq_ptm = Varp("Seq",dpty)
495 and ite_ptm = Varp("Ite",dpty)
496 and while_ptm = Varp("While",dpty)
497 and skip_ptm = Varp("SKIP",dpty)
498 and abort_ptm = Varp("ABORT",dpty)
499 and if_ptm = Varp("IF",dpty)
500 and do_ptm = Varp("DO",dpty)
501 and assert_ptm = Varp("ASSERT",dpty)
502 and awhile_ptm = Varp("AWHILE",dpty)
503 and ado_ptm = Varp("ADO",dpty) in
504 let pmk_pair(ptm1,ptm2) = Combp(Combp(Varp(",",dpty),ptm1),ptm2) in
506 match dive_to_var ptm with Varp(n,_) -> n | _ -> fail() in
507 let rec assign s v e =
509 Combp(Combp(pop,lptm),rptm) ->
510 if varname pop = "," then
511 Combp(Combp(pop,assign lptm v e),assign rptm v e)
513 | _ -> if varname s = v then e else s in
514 let lmk_assign s v e = Combp(assign_ptm,Absp(s,assign s v e))
516 if cs = [] then c else Combp(Combp(seq_ptm,c),hd cs)
517 and lmk_ite e c1 c2 = Combp(Combp(Combp(ite_ptm,e),c1),c2)
518 and lmk_while e c = Combp(Combp(while_ptm,e),c)
519 and lmk_skip _ = skip_ptm
520 and lmk_abort _ = abort_ptm
521 and lmk_if e c = Combp(Combp(if_ptm,e),c)
522 and lmk_do c e = Combp(Combp(do_ptm,c),e)
523 and lmk_assert e = Combp(assert_ptm,e)
524 and lmk_awhile i v e c = Combp(Combp(Combp(Combp(awhile_ptm,i),v),e),c)
525 and lmk_ado i v c e = Combp(Combp(Combp(Combp(ado_ptm,i),v),c),e) in
526 let lmk_gwhile al e c =
527 if al = [] then lmk_while e c
528 else lmk_awhile (fst(hd al)) (snd(hd al)) e c
530 if al = [] then lmk_do c e
531 else lmk_ado (fst(hd al)) (snd(hd al)) c e in
532 let expression s = parse_preterm >> (fun p -> Absp(s,p)) in
534 function ((Ident n)::rest) -> n,rest
535 | _ -> raise Noparse in
537 a (Ident "variant") ++ parse_preterm
539 || a (Ident "measure") ++ expression s
540 >> fun (_,m) -> Combp(Varp("MEASURE",dpty),m) in
542 a (Resword "[") ++ a (Ident "invariant") ++ expression s ++
543 a (Resword ";") ++ variant s ++ a (Resword "]")
544 >> fun (((((_,_),i),_),v),_) -> (i,v) in
545 let rec command s i =
546 (a (Resword "(") ++ commands s ++ a (Resword ")")
547 >> (fun ((_,c),_) -> c)
548 || a (Resword "skip")
550 || a (Resword "abort")
552 || a (Resword "if") ++ expression s ++ a (Resword "then") ++ command s ++
553 possibly (a (Resword "else") ++ command s >> snd)
554 >> (fun ((((_,e),_),c),cs) -> if cs = [] then lmk_if e c
555 else lmk_ite e c (hd cs))
556 || a (Resword "while") ++ expression s ++ a (Resword "do") ++
557 possibly (annotation s) ++ command s
558 >> (fun ((((_,e),_),al),c) -> lmk_gwhile al e c)
559 || a (Resword "do") ++ possibly (annotation s) ++
560 command s ++ a (Resword "while") ++ expression s
561 >> (fun ((((_,al),c),_),e) -> lmk_gdo al c e)
562 || a (Resword "{") ++ expression s ++ a (Resword "}")
563 >> (fun ((_,e),_) -> lmk_assert e)
564 || identifier ++ a (Resword ":=") ++ parse_preterm
565 >> (fun ((v,_),e) -> lmk_assign s v e)) i
567 (command s ++ possibly (a (Resword ";") ++ commands s >> snd)
568 >> (fun (c,cs) -> lmk_seq c cs)) i in
571 (a (Resword "var") ++ parse_preterm ++ a (Resword ";")) i in
572 let c,r' = (commands s ++ a (Resword "end") >> fst) r in
575 a (Ident "correct") ++ parse_preterm ++ program ++ parse_preterm
576 >> fun (((_,p),(s,c)),q) ->
577 Combp(Combp(Combp(Varp("correct",dpty),Absp(s,p)),c),Absp(s,q)) in
578 (program >> snd),assertion;;
580 (* ------------------------------------------------------------------------- *)
581 (* Introduce the variables in the VCs. *)
582 (* ------------------------------------------------------------------------- *)
585 let PAIR_CONV = REWR_CONV(GSYM PAIR) in
586 let rec repair vs v acc =
587 try let l,r = dest_pair vs in
588 let th = PAIR_CONV v in
589 let tm = rand(concl th) in
590 let rtm = rator tm in
591 let lth,acc1 = repair l (rand rtm) acc in
592 let rth,acc2 = repair r (rand tm) acc1 in
593 TRANS th (MK_COMB(AP_TERM (rator rtm) lth,rth)),acc2
594 with Failure _ -> REFL v,((v,vs)::acc) in
596 let abstm = find_term (fun t -> not (is_abs t) & is_gabs t) w in
597 let vs = fst(dest_gabs abstm) in
598 let v = genvar(type_of(fst(dest_forall w))) in
599 let th,gens = repair vs v [] in
600 (X_GEN_TAC v THEN SUBST1_TAC th THEN
601 MAP_EVERY SPEC_TAC gens THEN REPEAT GEN_TAC) (asl,w);;
604 let PAIR_CONV = REWR_CONV(GSYM PAIR) in
605 let rec repair vs v acc =
606 try let l,r = dest_pair vs in
607 let th = PAIR_CONV v in
608 let tm = rand(concl th) in
609 let rtm = rator tm in
610 let lth,acc1 = repair l (rand rtm) acc in
611 let rth,acc2 = repair r (rand tm) acc1 in
612 TRANS th (MK_COMB(AP_TERM (rator rtm) lth,rth)),acc2
613 with Failure _ -> REFL v,((v,vs)::acc) in
615 let abstm = find_term (fun t -> not (is_abs t) & is_gabs t) w in
616 let vs0 = fst(dest_gabs abstm) in
617 let vl0 = striplist dest_pair vs0 in
618 let vl = map (variant (variables (list_mk_conj(w::map (concl o snd) asl))))
620 let vs = end_itlist (curry mk_pair) vl in
621 let v = genvar(type_of(fst(dest_forall w))) in
622 let th,gens = repair vs v [] in
623 (X_GEN_TAC v THEN SUBST1_TAC th THEN
624 MAP_EVERY SPEC_TAC gens THEN REPEAT GEN_TAC) (asl,w);;
626 (* ------------------------------------------------------------------------- *)
627 (* Tidy up a verification condition. *)
628 (* ------------------------------------------------------------------------- *)
631 REWRITE_TAC[IMPLIES; o_THM; FALSE; TRUE; AND; OR; NOT; IMP] THEN
632 STATE_GEN_TAC THEN CONV_TAC(REDEPTH_CONV GEN_BETA_CONV) THEN
633 REWRITE_TAC[PAIR_EQ; GSYM CONJ_ASSOC];;
635 (* ------------------------------------------------------------------------- *)
636 (* Calculate a (pseudo-) weakest precondition for command. *)
637 (* ------------------------------------------------------------------------- *)
641 (map (snd o strip_forall o concl)
642 [WP_ASSIGN; WP_ITE; WP_SKIP; WP_ABORT; WP_IF; WP_ASSERT]) @
643 [`wp (AWHILE i v e c) q = i`; `wp (ADO i v c e) q = i`] in
645 tryfind (fun t -> rand (instantiate (term_match [] (lhand t) tm) t))
647 fun tm q -> conv(mk_comb(list_mk_icomb "wp" [tm],q));;
649 (* ------------------------------------------------------------------------- *)
650 (* Tools for automatic VC generation from annotated program. *)
651 (* ------------------------------------------------------------------------- *)
654 let is_seq = is_binary "Seq"
655 and strip_seq = striplist (dest_binary "Seq")
657 try fst(dest_const(rator tm)) = "ASSERT" with Failure _ -> false
659 try fst(dest_const(rator tm)) = "Assign" with Failure _ -> false
661 GEN_REWRITE_TAC I [FUN_EQ_THM] THEN STATE_GEN_TAC THEN
662 PURE_REWRITE_TAC[IMPLIES; o_THM; FALSE; TRUE; AND; OR; NOT; IMP] THEN
663 CONV_TAC(REDEPTH_CONV GEN_BETA_CONV) THEN
664 REWRITE_TAC[PAIR_EQ] THEN NO_TAC in
665 let ADJUST_TAC ptm ptm' ((_,w) as gl) =
666 let w' = subst [ptm',ptm] w in
667 let th = EQT_ELIM(REWRITE_CONV[correct; WP_SEQ] (mk_eq(w,w'))) in
668 GEN_REWRITE_TAC I [th] gl in
670 let cptm,q = dest_comb w in
671 let cpt,ptm = dest_comb cptm in
672 let ctm,p = dest_comb cpt in
673 let ptms = strip_seq ptm in
674 let seq = rator(rator ptm) in
675 try let atm = find is_assert ptms in
676 let i = index atm ptms in
678 let ptm' = mk_binop seq (hd ptms) (list_mk_binop seq (tl ptms)) in
679 (ADJUST_TAC ptm ptm' THEN
680 MATCH_MP_TAC VC_SEQ_ASSERT_LEFT THEN CONJ_TAC THENL
681 [VC_UNPACK_TAC; ALL_TAC]) (asl,w)
682 else if i = length ptms - 1 then
683 let ptm' = mk_binop seq (list_mk_binop seq (butlast ptms))
685 (ADJUST_TAC ptm ptm' THEN
686 MATCH_MP_TAC VC_SEQ_ASSERT_RIGHT THEN CONJ_TAC THENL
687 [ALL_TAC; VC_UNPACK_TAC]) (asl,w)
689 let l,mr = chop_list (index atm ptms) ptms in
690 let ptm' = mk_binop seq (list_mk_binop seq l)
691 (mk_binop seq (hd mr) (list_mk_binop seq (tl mr))) in
692 (ADJUST_TAC ptm ptm' THEN
693 MATCH_MP_TAC VC_SEQ_ASSERT_MIDDLE THEN CONJ_TAC) (asl,w)
694 with Failure "find" -> try
695 if is_assign (hd ptms) then
696 let ptm' = mk_binop seq (hd ptms) (list_mk_binop seq (tl ptms)) in
697 (ADJUST_TAC ptm ptm' THEN
698 MATCH_MP_TAC VC_SEQ_ASSIGN_LEFT THEN REPEAT CONJ_TAC THENL
699 [SIDE_TAC; SIDE_TAC; ALL_TAC]) (asl,w)
702 let ptm' = mk_binop seq
703 (list_mk_binop seq (butlast ptms)) (last ptms) in
704 let pwp = find_pwp (rand ptm') q in
705 (ADJUST_TAC ptm ptm' THEN MATCH_MP_TAC CORRECT_SEQ THEN
706 EXISTS_TAC pwp THEN CONJ_TAC)
709 (* ------------------------------------------------------------------------- *)
710 (* Tactic to apply a 1-step VC generation. *)
711 (* ------------------------------------------------------------------------- *)
717 MATCH_MP_TAC VC_SKIP THEN VC_UNPACK_TAC;
718 `correct p (ASSERT b) q`,
719 MATCH_MP_TAC VC_ASSERT THEN VC_UNPACK_TAC;
720 `correct p (Assign f) q`,
721 MATCH_MP_TAC VC_ASSIGN THEN VC_UNPACK_TAC;
722 `correct p (Ite e c1 c2) q`,
723 MATCH_MP_TAC VC_ITE THEN CONJ_TAC;
724 `correct p (IF e c) q`,
725 MATCH_MP_TAC VC_IF THEN CONJ_TAC THENL [ALL_TAC; VC_UNPACK_TAC];
726 `correct p (AWHILE i (MEASURE m) e c) q`,
727 MATCH_MP_TAC VC_AWHILE_MEASURE THEN REPEAT CONJ_TAC THENL
728 [VC_UNPACK_TAC; VC_UNPACK_TAC; GEN_TAC];
729 `correct p (AWHILE i v e c) q`,
730 MATCH_MP_TAC VC_AWHILE_VARIANT THEN REPEAT CONJ_TAC THENL
731 [ALL_TAC; VC_UNPACK_TAC; VC_UNPACK_TAC; STATE_GEN_TAC'];
732 `correct p (ADO i (MEASURE m) c e) q`,
733 MATCH_MP_TAC VC_ADO_MEASURE THEN REPEAT CONJ_TAC THENL
734 [VC_UNPACK_TAC; VC_UNPACK_TAC; STATE_GEN_TAC'];
735 `correct p (ADO i v c e) q`,
736 MATCH_MP_TAC VC_ADO_VARIANT THEN REPEAT CONJ_TAC THENL
737 [ALL_TAC; VC_UNPACK_TAC; VC_UNPACK_TAC; STATE_GEN_TAC'];
738 `correct p (c1 Seq c2) q`,
739 VC_SEQ_TAC] empty_net in
740 fun (asl,w) -> FIRST(lookup w tacnet) (asl,w);;
742 (* ------------------------------------------------------------------------- *)
743 (* Final packaging to strip away the program completely. *)
744 (* ------------------------------------------------------------------------- *)
746 let VC_TAC = REPEAT VC_STEP_TAC;;
748 (* ------------------------------------------------------------------------- *)
750 (* ------------------------------------------------------------------------- *)
752 install_parser ("correct",parse_program_assertion);;
754 let EXAMPLE_FACTORIAL = prove
760 while x < n do [invariant x <= n /\ (y = FACT x); measure n - x]
766 [STRIP_TAC THEN ASM_REWRITE_TAC[FACT; LE_0];
767 REWRITE_TAC[CONJ_ASSOC; NOT_LT; LE_ANTISYM] THEN MESON_TAC[];
768 REWRITE_TAC[GSYM ADD1; FACT] THEN STRIP_TAC THEN
769 ASM_REWRITE_TAC[MULT_AC] THEN UNDISCH_TAC `x < n` THEN ARITH_TAC]);;
771 delete_parser "correct";;