1(* ========================================================================= *) 2(* Tools for reasoning about wp and wlp. *) 3(* ========================================================================= *) 4 5signature wpTools = 6sig 7 8 (* A useful tactic for case-splitting conditionals *) 9 val if_cases_tac : Abbrev.thm_tactic -> Abbrev.tactic 10 11 (* A theorem tactic for use with if_cases_tac for wlp calculation *) 12 val wlp_assume_tac : Abbrev.thm_tactic 13 14 (* The main tactics for reducing Leq pre (wlp prog post) *) 15 val pure_wlp_tac : Abbrev.tactic 16 val leq_tac : Abbrev.tactic 17 val wlp_tac : Abbrev.tactic 18 19end 20