Extrategies

Extrategies is a set of strategy combinators and Lisp functions for writing and debugging 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. For details, see the Extrategies README at the PVS repository.

• The strategies included in Extrategies are:

  Printing and commenting	printf, commentf, quietly, error-msg, warning-msg
  Defining proof rules	deftactic, 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@, cond-match, if-match
  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, enable-debug-mode, disable-debug-mode, set-debug-mode, load-files

• 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