Extrategies

Extrategies is a set of strategy combinators and Lisp functions for writting strategies in PVS. Extrategies also contains improved versions of standard PVS strategies for skolemizing, naming, labeling, replacing, splitting, etc.

Extrategies has been part of PVS since PVS 5.0 and is included in the latest release of PVS.

• The strategies included in Extrategies are:
  • Printing and commenting: printf, commentf, now, extrategies-about
  • Defining tactics, i.e., local strategies: deftactic
  • Defining oracles, i.e., trusted proof rules: deforacle
  • Labeling and naming: unlabel*, delabel, relabel, name-label, name-label*, name-replace*, discriminate
  • Copying formulas: copy*, protect, with-focus-on, with-focus-on@
  • Programming: mapstep, mapstep@, with-fresh-labels, with-fresh-labels@, with-fresh-names, with-fresh-names@
  • Control flow: try@, try-then, try-then@, finalize, finalize*, touch, for, for@, when, when@, unless, unless@, when-label, when-label@, unless-label, unless-label@, if-label, sklisp
  • Let-in: skoletin, skoletin*, redlet, redlet*
  • Quantifiers: skeep, skeep*, skodef, skodef*, insteep, insteep*, unroll
  • TCCs: tccs-expression, tccs-formula, tccs-formula*, tccs-step, if-tcc-sequent, with-tccs
  • Ground evaluation (PVSio): eval-formula, eval-formula*, eval-expr, eval
  • Miscellaneous: splash, replaces, rewrites, rewrite*, suffices
  • Strategy debugging (experts only): skip-steps, show-debug-mode, toggle-debug-mode
• Examples
• Real Automation in the Field, César Muñoz and Micaela Mayero, Contractor Report ICASE, NASA/CR-2001-211271, 2001. BibTex Reference

The tag identifies links that are outside the NASA domain