FIELD and EXTRA-TEGIES ----------------------- By Cesar Munoz http://research.nianet.org/~munoz/Field National Institute of Aerospace, February 2003 ICASE - NASA Langley Research Center Version: Field.2b (for PVS 3.1 and Manip 1.1) This package contains the strategies FIELD, CANCEL-BY, and other extra-tegies for arithmetic and logic manipulation of formulas. Most of the strategies in this package act on relational formulas having the form e <> f, where <> is one of =,<,<=,>,=>. REQUIREMENTS ------------ Field.2b requires PVS 3.1 and Manip 1.1. If you have PVS 2.4 you need Field.1h. BASIC INSTALLATION ------------------ 0. Install PVS 3.1 (http://pvs.csl.sri.com) and Manip 1.1 (http://shemesh.larc.nasa.gov/people/bld/manip.html). IMPORTANT: If you are upgrading from Manip 1 or Field.1h, do not forget to comment out any reference to these packages in your .pvsemacs and pvs-strategies files. Otherwise, Manip 1.1 and Field.2b won't work. 1. Unpack Field.2b, e.g., $ tar xfz Field.2b.tgz The Field distribution directory is /Field.2b. 2. Set the environment variable PVS_LIBRARY_PATH as explained in the Manip's README file. Check that $PVS_LIBRARY_PATH/Manip exists. If you do not set this variable, the installation procedure will assume that you have installed Manip, and want to install Field, at /lib. 3. Go to the distribution directory $ cd Field.2b and type (avoid a trailing '/') $ make -e PVS_DIR= If everything is OK, you will see: "Field.2b has been installed at $PVS_LIBRARY_PATH". Otherwise, go to the next section. 4. (Optional but Recommended) Test the package with $ make test -e PVS_DIR= This will take sometime and print several messages. Look for the lines: "field_examples: 39 proofs attempted, 39 proved in .. .. PVS Exited". 5. Go to Using the Field Package. EXPERT INSTALLATION ------------------- First, check that you have the right PVS version. Type $ /pvs --version If it outputs "PVS version 3.1" you are OK. If it outputs "PVS version 3.0", we strongly recommend upgrading to PVS 3.1. If you stick with PVS 3.0, you may still be able to use the Field package (see Troubleshooting Question 1). If you are upgrading from Manip 1 or Field.1h, *do not forget* to comment out any reference to these packages in your .pvsemacs and pvs-strategies files. Otherwise, Manip 1.1 and Field.2b won't work. After unpacking Field.2b.tgz, you should have the Field distribution directory at /Field.2b: README This file. lib/ Field package. examples/ Several examples. doc/ PS and PDF version of the ICASE Interim Report: Real Automation in the Field by C. Munoz and M. Mayero. Caveat: This report documents Field.1h. Makefile Makefile to install Field.2b. pvscontext.el PVS-Emacs code to recreate lib/.pvscontext. examples.el PVS-Emacs code to test the installation of Field.2b. The directory may be located wherever you want. The installation procedure will instruct you later how to install the directory /Field.2b/lib in PVS 3.1. Verify that you have set the environment variable PVS_LIBRARY_PATH. In most cases PVS_LIBRARY_PATH is a single directory. In order to install Field.2b in there, check that $PVS_LIBRARY_PATH/Manip does exist. However, PVS_LIBRARY_PATH may also be a list of directories rather than a single directory. It this is your case, you probably are a PVS expert and then you know what to do (see Troubleshooting Question 4). Now, you need to (a) recreate the .pvscontext file in Field.2b/lib and (b) install Field.2b/lib in PVS_LIBRARY_PATH. (a) Recreating Field.2b/lib/.pvscontext Go to the distribution directory and type (avoid a trailing '/') $ make pvscontext -e PVS_DIR= If you haven't set PVS_LIBRARY_PATH, the make installation procedure will look for /lib/Manip. Look for the the lines: "top: 9 proofs attempted, 9 proved in .. .. PVS Exited" Ignore the messages about baseline or baseline.log. Alternatively, go to Field.2b/lib and remove, if they exist, .pvscontext and *.bin files. Then, run $ /pvs -q The '-q' option tells PVS not to load ~/.pvsemacs. Open the file top.pvs and type the emacs command M-x prove-importchain top. Verify that PVS Status buffer reports "Grand Totals: 9 proofs, 9 attempted, 9 succeeded", and quit PVS. (b) Installing Field.2b/lib in PVS_LIBRARY_PATH. Go to the distribution directory and type (avoid a trailing '/') $ make install -e PVS_DIR= If you haven't set PVS_LIBRARY_PATH, the make installation procedure will try to install Field at /lib. You will see: "Field.2b has been installed at $PVS_LIBRARY_PATH". Alternatively, type $ ln -f -s /Field.2b/lib $PVS_LIBRARY_PATH/Field Finally, you may want to test the installation. Type (avoid a trailing '/') $ make test -e PVS_DIR= This will run PVS in the file examples/field_examples.pvs and redo all the proofs. Depending on your machine, it will take several minutes. Look for the lines: "field_examples: 39 proofs attempted, 39 proved in .. .. PVS Exited". You are ready to use the Field package. USING THE FIELD PACKAGE ----------------------- The first time you use Field and Extra-tegies in a working directory, you have to load the package with the emacs command: M-x load-prelude-library Field. This command saves the information concerning Field.2b (and Manip 1.1) in .pvscontext. Unless you erase .pvscontext, there is no need to retype the load-prelude-library command in the same working directory in further PVS sessions. If you are not sure what packages you have loaded in .pvscontext, type the emacs command: M-x list-prelude-libraries. Other than for recreating the .pvscontext file, you should never run PVS in Field.2b/lib (see Troubleshooting Question 2). QUICK DOCUMENTATION ------------------- FIELD and CANCEL-BY are the main strategies provided by this package. However, it also includes a set of strategies for arithmetic and logic manipulation of formulas. They are referred as "extra-tegies". FIELD is a simplification procedure for the field of real numbers. It was originally based on Field of Coq V7 (Mayero, Delahaye), but it has been extensively adapted to cope with PVS idiosyncrasies. First, it removes inverses, and then it simplifies using PVS decision procedures. It also tries to prove that inverses are not null. CANCEL-BY tries to eliminate a factor term of a relational formula. First, it divides the formula by the factor term, and then it simplifies the formula by using PVS decision procedures. It also tries to prove that the common term is not null. CANCEL-FORMULA combines Manip's FACTOR and CANCEL-BY to cancel common factors in a relational formula. GRIND-REALS : Applies GRIND with real_props. REAL-PROPS : Rewrites with real_props in a given formula (or set of formulas). REPLACES : Iterates REPLACE using a list of formulas. In contrast to REPLACE, HIDE? T is the default. NEG-FORMULA : Negates both sides of a relational formula. ADD-FORMULAS : Adds two relational formulas. SUB-FORMULAS : Subtracts two relational formulas. WRAP-FORMULA : Wraps both sides of a relational formula with a string. NAME-DISTRIB : Introduces new names to block distributive laws in a list of relational formulas. SPLASH : Splits, in an asymmetrical way, a conjunction in the consequent (or a disjunction in the antecedent). SKEEP : Introduces Skolem variables by keeping the original names of the quantified variables. CANCEL-FORMULA : Factorizes common terms in a formula and then cancels them. SKODEF : Instantiates quantified formulas appearing in the antecedent and having the form FORALL (..x..):x=... AND ... IMPLIES ... or in the consequent and having the form EXISTS (..x..):x=... AND .... SKODEF* iterates SKODEF. FIELD-ABOUT : Prints about-information of the field package. If you have ever used large let-in expressions and think that they are clumsy to manipulate, try the following new strategies: REDLET : Reduces, in a controlled way, let-in expressions. REDLET* iterates REDLET. SKOLETIN : Skolemizes let-in expressions. SKOLETIN* iterates SKOLETIN. EXAMPLES -------- Check the files in the directory /Field.2b/examples. RELATED LIBRARIES ----------------- Other than the Manip package, you do not need to install any additional library or package to work with Field.2b. However, for serious developments on real numbers, you may consider to install the NASA LaRC libraries "reals" and "trig", which are available at: http://shemesh.larc.nasa.gov/ftp/larc/PVS-library/pvslib.html. TROUBLESHOOTING --------------- 0. I am using RedHat 9.0 and Field installation does not work. PVS 3.1 is broken in RedHat 9.0. See: http://pvs.csl.sri.com/cgi-bin/pvs/pvs-bug?id=765 To install Field in RedHat 9.0, use make -e PVS_DIR='LD_ASSUME_KERNEL=2.4.1 LANG=C ' PVS_OPTIONS='-redhat 5' 1. I have PVS 3.0. Can I install/use Field.2b ? We strongly recommend PVS 3.1. However, if for some reason you cannot upgrade PVS 3.0, this is the trick: - Install Manip 1.1 and Field.2b in the regular way. - Type the emacs command M-x load-prelude-library Field before using the package. - Write IMPORTING Field@top in the scope of the PVS file where you are using the package. 2. PVS hangs when loading then Field package or exists with strange messages. What can I do? The file Field.2b/lib/.pvscontext is probably corrupted. Recreate Field.2b/lib/.pvcontext as explained in the expert installation. If this does not work, delete .pvscontext and *.bin files from your working directory and try again (do not forget to type the emacs command M-x load-prelude-library Field in the new context). 3. Is it possible to move the distribution directory to a different location? Yes, but before you can use the package, you need to install the new location of Field.2b/lib in PVS_LIBRARY_PATH as explained in the expert installation. 4. My environment variable PVS_LIBRARY_PATH points to a list of directories rather than a single directory. How can I install Field.2b? Pick any directory already in PVS_LIBRARY_PATH, let's say , and run make with the option '-e LIB_DIR='. Avoid a trailing '/'. REMARK: Makefile checks that - PVS_LIBRARY_PATH is defined, - $LIB_DIR is in $PVS_LIBRARY_PATH, and - Manip exists in $PVS_LIBRARY_PATH If you do not want any checking to be performed use make's option '-e OK=yes'. 5. Sometimes FIELD takes a long time to perform trivial simplifications. Is that normal? How can I stop it ? Despite the implementation of some heuristics, FIELD's algorithm is still exponential. The main difficulty is that FIELD has to prove that quotients are strictly positive or strictly negative. FIELD has no clue about this (even although, it may seem obvious from the premises). Hence, it tries both branches. You can help FIELD by making explicit all the information you know about quotients before using FIELD in a given formula. Finally, note that FIELD extensively uses REPLACE, ASSERT, and GRIND. Those strategies are known to fall in infinite loops in some cases. If FIELD does not report anything for a long period of time, this is probably the case. You may stop FIELD in the usual way C-c C-c C-d. 6. During the installation process, how can I tell make to run PVS with some particular options ? Use make's option -e to define PVS_OPTIONS. For instance to run PVS with XEmacs instead of Emacs, type make -e PVS_DIR= PVS_OPTIONS='-emacs xemacs' 7. How do I turn off the checking performed in Makefile ? If you know what you are doing, use make's options '-e OK=yes'. CHANGE LOG ---------- See file CHANGES. Cesar Munoz