Examples/prog.ml

   1 (* ========================================================================= *)
   2 (* Simple WHILE-language with relational semantics.                          *)
   3 (* ========================================================================= *)
   4
   5 prioritize_num();;
   6
   7 parse_as_infix("refined",(12,"right"));;
   8
   9 (* ------------------------------------------------------------------------- *)
  10 (* Logical operations "lifted" to predicates, for readability.               *)
  11 (* ------------------------------------------------------------------------- *)
  12
  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"));;
  17
  18 let FALSE = new_definition
  19   `FALSE = \x:S. F`;;
  20
  21 let TRUE = new_definition
  22   `TRUE = \x:S. T`;;
  23
  24 let NOT = new_definition
  25   `NOT p = \x:S. ~(p x)`;;
  26
  27 let AND = new_definition
  28   `p AND q = \x:S. p x /\ q x`;;
  29
  30 let OR = new_definition
  31   `p OR q = \x:S. p x \/ q x`;;
  32
  33 let ANDS = new_definition
  34   `ANDS P = \x:S. !p. P p ==> p x`;;
  35
  36 let ORS = new_definition
  37   `ORS P = \x:S. ?p. P p /\ p x`;;
  38
  39 let IMP = new_definition
  40   `p IMP q = \x:S. p x ==> q x`;;
  41
  42 (* ------------------------------------------------------------------------- *)
  43 (* This one is different, corresponding to "subset".                         *)
  44 (* ------------------------------------------------------------------------- *)
  45
  46 let IMPLIES = new_definition
  47   `p IMPLIES q <=> !x:S. p x ==> q x`;;
  48
  49 (* ------------------------------------------------------------------------- *)
  50 (* Simple procedure to prove tautologies at the predicate level.             *)
  51 (* ------------------------------------------------------------------------- *)
  52
  53 let PRED_TAUT =
  54   let tac =
  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);;
  58
  59 (* ------------------------------------------------------------------------- *)
  60 (* Some applications.                                                        *)
  61 (* ------------------------------------------------------------------------- *)
  62
  63 let IMPLIES_TRANS = PRED_TAUT
  64   `!p q r. p IMPLIES q /\ q IMPLIES r ==> p IMPLIES r`;;
  65
  66 (* ------------------------------------------------------------------------- *)
  67 (* Enumerated type of basic commands, and other derived commands.            *)
  68 (* ------------------------------------------------------------------------- *)
  69
  70 parse_as_infix("Seq",(26,"right"));;
  71
  72 let command_INDUCTION,command_RECURSION = define_type
  73   "command = Assign (S->S)
  74            | Seq command command
  75            | Ite (S->bool) command command
  76            | While (S->bool) command";;
  77
  78 let SKIP = new_definition
  79   `SKIP = Assign I`;;
  80
  81 let ABORT = new_definition
  82   `ABORT = While TRUE SKIP`;;
  83
  84 let IF = new_definition
  85   `IF e c = Ite e c SKIP`;;
  86
  87 let DO = new_definition
  88   `DO c e = c Seq (While e c)`;;
  89
  90 let ASSERT = new_definition
  91   `ASSERT g = Ite g SKIP ABORT`;;
  92
  93 (* ------------------------------------------------------------------------- *)
  94 (* Annotation commands, to allow insertion of loop (in)variants.             *)
  95 (* ------------------------------------------------------------------------- *)
  96
  97 let AWHILE = new_definition
  98   `AWHILE (i:S->bool) (v:S->S->bool) (e:S->bool) c = While e c`;;
  99
 100 let ADO = new_definition
 101   `ADO (i:S->bool) (v:S->S->bool) c (e:S->bool) = DO c e`;;
 102
 103 (* ------------------------------------------------------------------------- *)
 104 (* Useful properties of type constructors for commands.                      *)
 105 (* ------------------------------------------------------------------------- *)
 106
 107 let command_DISTINCT =
 108   distinctness "command";;
 109
 110 let command_INJECTIVE =
 111   injectivity "command";;
 112
 113 (* ------------------------------------------------------------------------- *)
 114 (* Relational semantics of commands.                                         *)
 115 (* ------------------------------------------------------------------------- *)
 116
 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'')`;;
 126
 127 (* ------------------------------------------------------------------------- *)
 128 (* A more "denotational" view of the semantics.                              *)
 129 (* ------------------------------------------------------------------------- *)
 130
 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[]);;
 135
 136 let SEM_SEQ = prove
 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[]);;
 140
 141 let SEM_ITE = prove
 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[]);;
 146
 147 let SEM_SKIP = prove
 148  (`sem(SKIP) s s' <=> (s' = s)`,
 149   REWRITE_TAC[SKIP; SEM_ASSIGN; I_THM]);;
 150
 151 let SEM_IF = prove
 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]);;
 154
 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[]);;
 160
 161 let SEM_ABORT = prove
 162  (`sem(ABORT) s s' <=> F`,
 163   let lemma = prove
 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
 168   MESON_TAC[lemma]);;
 169
 170 let SEM_DO = prove
 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]);;
 173
 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]);;
 177
 178 (* ------------------------------------------------------------------------- *)
 179 (* Proofs that all commands are deterministic.                               *)
 180 (* ------------------------------------------------------------------------- *)
 181
 182 let deterministic = new_definition
 183   `deterministic r <=> !s s1 s2. r s s1 /\ r s s2 ==> (s1 = s2)`;;
 184
 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
 194   ASM_MESON_TAC[]);;
 195
 196 (* ------------------------------------------------------------------------- *)
 197 (* Termination, weakest liberal precondition and weakest precondition.       *)
 198 (* ------------------------------------------------------------------------- *)
 199
 200 let terminates = new_definition
 201   `terminates c s <=> ?s'. sem c s s'`;;
 202
 203 let wlp = new_definition
 204   `wlp c q s <=> !s'. sem c s s' ==> q s'`;;
 205
 206 let wp = new_definition
 207   `wp c q s <=> terminates c s /\ wlp c q s`;;
 208
 209 (* ------------------------------------------------------------------------- *)
 210 (* Dijkstra's healthiness conditions (the last because of determinism).      *)
 211 (* ------------------------------------------------------------------------- *)
 212
 213 let WP_TOTAL = prove
 214  (`!c. (wp c FALSE = FALSE)`,
 215   REWRITE_TAC[FUN_EQ_THM; wp; wlp; terminates; FALSE] THEN MESON_TAC[]);;
 216
 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[]);;
 220
 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[]);;
 224
 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]);;
 229
 230 (* ------------------------------------------------------------------------- *)
 231 (* Weakest preconditions for the primitive and derived commands.             *)
 232 (* ------------------------------------------------------------------------- *)
 233
 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
 237   MESON_TAC[]);;
 238
 239 let WP_SEQ = prove
 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]);;
 243
 244 let WP_ITE = prove
 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
 247   MESON_TAC[]);;
 248
 249 let WP_WHILE = prove
 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]);;
 252
 253 let WP_SKIP = prove
 254  (`!q. wp SKIP q = q`,
 255   REWRITE_TAC[FUN_EQ_THM; SKIP; WP_ASSIGN; I_THM; o_THM]);;
 256
 257 let WP_ABORT = prove
 258  (`!q. wp ABORT q = FALSE`,
 259   REWRITE_TAC[FUN_EQ_THM; wp; wlp; terminates; SEM_ABORT; FALSE]);;
 260
 261 let WP_IF = prove
 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]);;
 264
 265 let WP_DO = prove
 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]);;
 268
 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
 272   MESON_TAC[]);;
 273
 274 (* ------------------------------------------------------------------------- *)
 275 (* Rules for total correctness.                                              *)
 276 (* ------------------------------------------------------------------------- *)
 277
 278 let correct = new_definition
 279   `correct p c q <=> p IMPLIES (wp c q)`;;
 280
 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]);;
 284
 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]);;
 288
 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]);;
 292
 293 let CORRECT_SEQ = prove
 294  (`!p q r c1 c2.
 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]);;
 298
 299 let CORRECT_ITE = prove
 300  (`!p e c1 c2 q.
 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[]);;
 304
 305 let CORRECT_WHILE = prove
 306  (`! (<<) p c q e invariant.
 307        WF(<<) /\
 308        p IMPLIES invariant /\
 309        (NOT e) AND invariant IMPLIES q /\
 310        (!X:S. correct
 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]);;
 327
 328 let CORRECT_SKIP = prove
 329  (`!p q. (p IMPLIES q) ==> correct p SKIP q`,
 330   REWRITE_TAC[correct; WP_SKIP]);;
 331
 332 let CORRECT_ABORT = prove
 333  (`!p q. F ==> correct p ABORT q`,
 334   REWRITE_TAC[]);;
 335
 336 let CORRECT_IF = prove
 337  (`!p e c q.
 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[]);;
 341
 342 let CORRECT_DO = prove
 343  (`! (<<) p q c invariant.
 344         WF(<<) /\
 345         (e AND invariant) IMPLIES p /\
 346         ((NOT e) AND invariant) IMPLIES q /\
 347         (!X:S. correct
 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[]]);;
 363
 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]);;
 367
 368 (* ------------------------------------------------------------------------- *)
 369 (* VCs for the basic commands (in fact only assign should be needed).        *)
 370 (* ------------------------------------------------------------------------- *)
 371
 372 let VC_ASSIGN = prove
 373  (`p IMPLIES (q o f) ==> correct p (Assign f) q`,
 374   REWRITE_TAC[o_DEF; CORRECT_ASSIGN]);;
 375
 376 let VC_SKIP = prove
 377  (`p IMPLIES q ==> correct p SKIP q`,
 378   REWRITE_TAC[CORRECT_SKIP]);;
 379
 380 let VC_ABORT = prove
 381  (`F ==> correct p ABORT q`,
 382   MATCH_ACCEPT_TAC CORRECT_ABORT);;
 383
 384 let VC_ASSERT = prove
 385  (`p IMPLIES (b AND q) ==> correct p (ASSERT b) q`,
 386   REWRITE_TAC[CORRECT_ASSERT]);;
 387
 388 (* ------------------------------------------------------------------------- *)
 389 (* VCs for composite commands other than sequences.                          *)
 390 (* ------------------------------------------------------------------------- *)
 391
 392 let VC_ITE = prove
 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]);;
 396
 397 let VC_IF = prove
 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]);;
 401
 402 let VC_AWHILE_VARIANT = prove
 403  (`WF(<<) /\
 404    p IMPLIES invariant /\
 405    (NOT e) AND invariant IMPLIES q /\
 406    (!X. correct
 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]);;
 410
 411 let VC_AWHILE_MEASURE = prove
 412  (`p IMPLIES invariant /\
 413    (NOT e) AND invariant IMPLIES q /\
 414    (!X. correct
 415           (invariant AND e AND (\s:S. X = m(s)))
 416           c
 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[]);;
 423
 424 let VC_ADO_VARIANT = prove
 425  (`WF(<<) /\
 426    (e AND invariant) IMPLIES p /\
 427    ((NOT e) AND invariant) IMPLIES q /\
 428    (!X. correct
 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]);;
 432
 433 let VC_ADO_MEASURE = prove
 434  (`(e AND invariant) IMPLIES p /\
 435    ((NOT e) AND invariant) IMPLIES q /\
 436    (!X. correct
 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[]);;
 443
 444 (* ------------------------------------------------------------------------- *)
 445 (* VCs for sequences of commands, using intelligence where possible.         *)
 446 (* ------------------------------------------------------------------------- *)
 447
 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)`]);;
 452
 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)`]);;
 457
 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`]);;
 462
 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]);;
 471
 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`]);;
 475
 476 (* ------------------------------------------------------------------------- *)
 477 (* Parser for correctness assertions.                                        *)
 478 (* ------------------------------------------------------------------------- *)
 479
 480 let rec dive_to_var ptm =
 481   match ptm with
 482     Varp(_,_) as vp -> vp | Typing(t,_) -> dive_to_var t | _ -> fail();;
 483
 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);;
 489
 490 reserve_program_words();;
 491
 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
 505   let varname ptm =
 506     match dive_to_var ptm with Varp(n,_) -> n | _ -> fail() in
 507   let rec assign s v e =
 508     match s with
 509       Combp(Combp(pop,lptm),rptm) ->
 510         if varname pop = "," then
 511           Combp(Combp(pop,assign lptm v e),assign rptm v e)
 512         else fail()
 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))
 515   and lmk_seq c cs =
 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
 529   and lmk_gdo al c e =
 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
 533   let identifier =
 534       function ((Ident n)::rest) -> n,rest
 535         | _ -> raise Noparse in
 536   let variant s =
 537      a (Ident "variant") ++ parse_preterm
 538      >> snd
 539   || a (Ident "measure") ++ expression s
 540      >> fun (_,m) -> Combp(Varp("MEASURE",dpty),m) in
 541   let annotation s =
 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")
 549        >> lmk_skip
 550     || a (Resword "abort")
 551        >> lmk_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
 566   and commands s i =
 567       (command s ++ possibly (a (Resword ";") ++ commands s >> snd)
 568        >> (fun (c,cs) -> lmk_seq c cs)) i in
 569   let program i =
 570     let ((_,s),_),r =
 571       (a (Resword "var") ++ parse_preterm ++ a (Resword ";")) i in
 572     let c,r' = (commands s ++ a (Resword "end") >> fst) r in
 573     (s,c),r' in
 574   let assertion =
 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;;
 579
 580 (* ------------------------------------------------------------------------- *)
 581 (* Introduce the variables in the VCs.                                       *)
 582 (* ------------------------------------------------------------------------- *)
 583
 584 let STATE_GEN_TAC =
 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
 595   fun (asl,w) ->
 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);;
 602
 603 let STATE_GEN_TAC' =
 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
 614   fun (asl,w) ->
 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))))
 619                  vl0 in
 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);;
 625
 626 (* ------------------------------------------------------------------------- *)
 627 (* Tidy up a verification condition.                                         *)
 628 (* ------------------------------------------------------------------------- *)
 629
 630 let VC_UNPACK_TAC =
 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];;
 634
 635 (* ------------------------------------------------------------------------- *)
 636 (* Calculate a (pseudo-) weakest precondition for command.                   *)
 637 (* ------------------------------------------------------------------------- *)
 638
 639 let find_pwp =
 640   let wptms =
 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
 644   let conv tm =
 645     tryfind (fun t -> rand (instantiate (term_match [] (lhand t) tm) t))
 646             wptms in
 647   fun tm q -> conv(mk_comb(list_mk_icomb "wp" [tm],q));;
 648
 649 (* ------------------------------------------------------------------------- *)
 650 (* Tools for automatic VC generation from annotated program.                 *)
 651 (* ------------------------------------------------------------------------- *)
 652
 653 let VC_SEQ_TAC =
 654   let is_seq = is_binary "Seq"
 655   and strip_seq = striplist (dest_binary "Seq")
 656   and is_assert tm =
 657     try fst(dest_const(rator tm)) = "ASSERT" with Failure _ -> false
 658   and is_assign tm =
 659      try fst(dest_const(rator tm)) = "Assign" with Failure _ -> false
 660   and SIDE_TAC =
 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
 669   fun (asl,w) ->
 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
 677         if i = 0 then
 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))
 684                                   (last ptms) in
 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)
 688         else
 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)
 700         else fail()
 701     with Failure _ ->
 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)
 707         (asl,w);;
 708
 709 (* ------------------------------------------------------------------------- *)
 710 (* Tactic to apply a 1-step VC generation.                                   *)
 711 (* ------------------------------------------------------------------------- *)
 712
 713 let VC_STEP_TAC =
 714   let tacnet =
 715   itlist (enter [])
 716    [`correct p SKIP q`,
 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);;
 741
 742 (* ------------------------------------------------------------------------- *)
 743 (* Final packaging to strip away the program completely.                     *)
 744 (* ------------------------------------------------------------------------- *)
 745
 746 let VC_TAC = REPEAT VC_STEP_TAC;;
 747
 748 (* ------------------------------------------------------------------------- *)
 749 (* Some examples.                                                            *)
 750 (* ------------------------------------------------------------------------- *)
 751
 752 install_parser ("correct",parse_program_assertion);;
 753
 754 let EXAMPLE_FACTORIAL = prove
 755  (`correct
 756    T
 757      var x,y,n;
 758        x := 0;
 759        y := 1;
 760        while x < n do [invariant x <= n /\ (y = FACT x); measure n - x]
 761         (x := x + 1;
 762          y := y * x)
 763      end
 764    y = FACT n`,
 765   VC_TAC THENL
 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]);;
 770
 771 delete_parser "correct";;