Manip: A PVS Prover Strategy Package for Common Manipulations Version 1.2 --- Released 20 November 2007 --- For PVS 3.1 or higher http://shemesh.larc.nasa.gov/people/bld/manip.html Ben L. Di Vito 1 South Wright Street, MS 130 NASA Langley Research Center Hampton, VA 23681 USA b.divito@nasa.gov http://shemesh.larc.nasa.gov/people/bld ------------------------ 0. Quick-Start Installation To get up and running quickly, read this section and skip the rest. For readers who want the full story, see the remaining sections. 1. Make sure PVS (3.1 or higher) has been installed. 2. Create a directory, if necessary, to store PVS libraries/packages. Change to this directory and unpack the Manip distribution, e.g., via the command 'tar xvzf '. 3. Add a symbolic link for the name Manip: 'ln -s Manip-1.2 Manip'. 4. Change to a working directory to run PVS. Set the environment variable PVS_LIBRARY_PATH to the directory from step 2 (avoid a trailing '/'). 5. After PVS starts, issue M-x load-prelude-library, then type 'Manip' at the prompt. (If you are also installing Field, you may skip this step; Field will load Manip.) NOTE: Do not run PVS from the distribution directory, Manip-1.2. ------------------------ 1. Abstract Sequent manipulations for an interactive prover such as PVS can be labor intensive. We provide an approach to tactic-based proving for improved interactive deduction in specialized domains. This approach has been mechanized by the Manip package of strategies (tactics) and support functions. Although it was designed originally to reduce the tedium of low-level arithmetic manipulation, many of its newer features are suitable as general-purpose prover utilities. Besides strategies aimed at algebraic simplification of real-valued expressions, Manip includes term-access techniques applicable in arbitrary settings. 2. Package Files README Summary of distribution (this file) manip-guide.pdf User's manual pvs-lib.el Package start-up (Emacs Lisp) pvs-lib.lisp Package start-up (Common Lisp) pvs-prover-manip.el User interface functions and utilities manip-strategies.lisp Prover strategies for manipulation extended-expr.lisp Extended expression functions for Manip syntax-matching.lisp Functions for syntax matching feature manip-utilities.lisp Various support functions for package pregexp.lisp Generic regular expression package developed by Dorai Sitaram .pvscontext Context file for extension theory .pvscontext-backup Write-protected backup copy extra_real_props.pvs Additional real number lemmas extra_real_props.prf Proofs of additional lemmas test Subdirectory for test files test*.pvs Theories for strategy test cases test*.prf Proof steps for test theories pvs-strategies Used by some proofs in test*.prf debug-utils.lisp Debugging utilities for strategy writers debug-utils.el Optional Emacs support for utilities 3. Installation and Setup With the arrival of PVS 4.1, Manip 1.2 now works with both the Allegro Common Lisp and the CMU Common Lisp versions of PVS. One of the enhancements in PVS version 3.0 was an improved mechanism for extending the PVS prelude with user-supplied libraries. The term "library" may refer to diverse collections of artifacts, including PVS extension theories, prover strategies, support software (both Emacs Lisp and Common Lisp), and data files. The Manip package is organized for installation using the enhanced Load Prelude Library feature. The Field package developed by Cesar Munoz also uses this feature, calling on the services of Manip as a dependent package. PVS now allows users to set the environment variable PVS_LIBRARY_PATH to a directory (or list of directories) where packages or prelude libraries can be found. We recommend using a single directory to store extension libraries and packages you expect to invoke. PVS_LIBRARY_PATH will need to point to this extension repository. Unpack the Manip tar file into this library directory, which will create the subdirectory Manip-1.2. A symbolic link to Manip-1.2 called Manip should also be added to the repository. Before starting PVS, the PVS_LIBRARY_PATH variable needs to be set. This can be done using either standard shell commands or by a PVS startup script. Here is a sample script for bash shells; adjust as needed for other shells. #! /bin/bash # Run PVS with strategy packages. export PVS_LIBRARY_PATH=~/pvs-packages /pvs If you will be using the Field strategies as well as Manip, you will need to have PVS_LIBRARY_PATH set before you do the Field installation. It might be best simply to set this variable during shell initialization, e.g., within your .bashrc file. The first time you run PVS in a new context, you have to tell it to load the Manip package via the Emacs command M-x load-prelude-library. Give the name Manip when it prompts for a library name. From this point on, the context file will contain a pointer to the Manip library. When PVS is restarted in this same context, the library will be reloaded without any action on your part. Only when a new context is started will you need to issue M-x load-prelude-library. If you see the error message "Ill-formed rule/strategy:..." when you invoke Manip strategies, it probably means you forgot to load the library. If you would like Manip to be available whenever you start PVS, you can add the line (load-prelude-library "Manip") to your .pvsemacs file. This will load the library on every start-up, obviating the need for the interactive command M-x load-prelude-library. If the Field strategies are a standard part of your working environment, the setup for Field includes automatic loading of Manip, so it will be unnecessary to follow the load procedures above. Also, if you use the full version of the NASA Langley PVS libraries (set up for installation in /lib), then Field and Manip will be available automatically. In that case, PVS_LIBRARY_PATH would not be needed. Do not use the old setup method involving pvs-strategies and .pvsemacs files that was required by Manip version 1.0. Thanks to the new library mechanism, the 1.2 setup procedure allows for smoother operation, particularly when multiple packages are used simultaneously. Do not run PVS from the distribution directory, Manip-1.2. This directory contains a context file for the prelude extension theory. It is best not to contaminate it with other theories. If this happens, you can restore it from .pvscontext-backup. The extension theory extra_real_props will be loaded automatically by PVS. This means the lemmas of that theory will be found without having to explicitly import the theory. Small theories used for regression testing are included with the package (in subdirectory "test") to illustrate the various features. Formulas found in these theories are not theorems and their "proofs" will not lead anywhere. They are provided as a means to exercise assorted strategies and easily view the results. Stepping through the proofs will demonstration the major capabilities. 4. Caveats - This version of the package has been developed for and tested on PVS version 4.1 (1 Nov 2007). It should also work with PVS 4.0 (Allegro version only). It should also work with PVS 3.1, 3.2. Do not use the 3.0 release (19 Dec 2002). Manip 1.2 is not backward compatible with PVS 2.3/2.4; users of 2.3/2.4 should use Manip 1.0. - Error checking in Manip should be adequate but is not complete. Some erroneous user inputs will not be cited as such, but will result in strategies having no effect. Although applying a strategy could result in a Lisp error, this should be rare. If it happens, restore the prover's state (TAB-] or Ctrl-D is convenient for this purpose), review the strategy's input expressions for problems, and retry using modified inputs. - Because PVS 3.0 added the multiple proof instance feature, proof files (.prf extension) have a new format. Proof files created by older PVS versions will not work with Manip's M-x expand-strategy-steps command. Make sure PVS writes out a proof file in the new format before using this Emacs command. - Some strategies invoke name-replace as an internal step using names chosen by the strategy procedures. The naming convention followed is to use identifiers ending in a double underscore, e.g., x1__. Refrain from using such names to avoid conflicts. - Due to a limitation of the regular expression module being used, the pattern matching implementation does not recognize the length-one case for %d& text fields. - When using the higher-order strategies (e.g., invoke or for-each) with substitutions based on the full extended expression descriptors (e.g., $1, $2, etc.), the prover might reject the command. If this happens, try changing the parameterized command to its $-form. For example, instead of (invoke (swap-rel $1) (? - "<=")), try the nonatomic form (invoke (swap-rel$ $1) (? - "<=")). Changing $1 to $1n is another way to avoid this problem. 5. Final Remarks Manip is now fairly mature. It has been exercised successfully for over five years by users at NASA Langley and also at a few other sites. We expect to make future enhancements as the need arises. We are always open to refining Manip and making it more useful to a broad array of PVS users. Feedback of any kind is encouraged so that it might be improved. We also welcome users to build on these features when developing their own personal strategies. 6. Acknowledgments The need for this package and many initial ideas on its operation were inspired by Ricky Butler of NASA Langley. Additional ideas and useful suggestions have come from Cesar Munoz of NIA, and John Rushby and Sam Owre of SRI. We appreciate their insightful input and feedback. Special thanks go to Sam Owre for implementing the new prelude library features that have simplified package installation. 7. References http://research.nianet.org/~munoz/Field/ The Field package developed by Cesar Munoz (munoz@nianet.org). ------------------------- Changes from version 1.1: - A new type of search was introduced that allows users to match against syntax elements of PVS expressions. Match results can be used to display information about the sequent or invoke proof rule templates after substituting matched text. - New extended expressions and TAB-key sequences were added to support the syntax matching feature. Users can highlight an expression in the Emacs buffer *pvs* then ask Manip to generate a pattern that matches it. - TAB-y was revised to work with the *Proof* buffer created by the show-current-proof command in addition to the Proof buffer. - New strategies added: match, branch-back, unwind-protect. Changes from version 1.0: - Revised setup and installation procedure to use the new prelude library features of PVS 3.0/3.1. - Improved the factor strategy so it takes integer coefficients into account, e.g., 4ax + 6bx ==> 2x(2a + 3b). - Improved error checking on user inputs. Breaking into Lisp should now be rare. - Added global variable *suppress-manip-messages* to control the display of errors, warnings and status messages. Changes from version 0.9: - Revised installation and setup procedure. Slightly different file and directory setup. The environment variable PVSMANIP is no longer needed. - Files and features were added to support PVS 2.4. Still works with v2.3. - Changing PVS context now causes prelude extensions to be reloaded. - Added optional arguments to permute-mult, mult-cases strategies. - Enhanced several strategies to handle more conditions: mult-by, div-by, mult-cases, cancel-terms. - Added a few new division lemmas to extra_real_props. - Added special forms for complements of term/formula number lists (see sect. 3). - Minor enhancements to location reference and parameter substitution features. Added substitution shortcuts (sect 6.3). - Added various clarifications to user's manual. - For strategy writers only: added some debug utilities to trace strategy execution and display intermediate values.