PVS 4.1 Release Notes

PVS 4.1 is primarily a bug fix release; there are few new features. Some of the changes do affect proofs, though our experience is that only a few proofs need adjustment, and most of these were quite easy to recognize and fix.

Installation Notes

The system is installed as usual; see the download pages at

http://pvs.csl.sri.com/download.shtml

We strongly suggest getting a pre-built Allegro version, unless you have concerns with the Allegro runtime click-though license, in which case get the pre-built CMU Lisp image.

The build process is largely untested outside of SRI. The process has been somewhat improved with this release, but please let us know of your experiences, and suggestions for improvement. Problems and solutions may be sent to pvs-bugs@csl.sri.com. If you are more ambitious, feel free to expand on the build description in the PVS Wiki (pvs-wiki.csl.sri.com).

PVS was recently moved from CVS to Subversion, and you can now access the system using svn:

svn checkout https://spartan.csl.sri.com/svn/public/pvs/trunk pvs

For now, this is read-only outside of SRI. If you wish to contribute code to PVS, please send it to pvs-sri@csl.sri.com, and we will assess and incorporate it.

Upgrades

• - PVS Now uses Allegro 8.1.
• - ILISP has been updated to version 5.12.0 - we include slightly modified sources of the ILISP files in pvs/emacs/emacs-src/ilisp/.
• - The pvs startup script has been modified to work with both Allegro and CMU Lisp. In particular, the ‘-L’ flag may be used to indicate a lisp file to be loaded after PVS starts.
• - Thanks to Jerry James (jamesj@acm.org, the BDD and WS1S source code have been brought up to date, and no longer generate warnings.
• - We have made minor additions to the prelude: A nonempty_set type, and the following lemmas: Union_member lemma, Union_emptyset_rew, Union_union_rew, Intersection_member, Intersection_intersection_rew, mod_wrap2, mod_inj1, mod_inj2, mod_wrap_inj_eq, mod_neg_limited, odd_mod, even_mod, and finite_Union_finite.
• - The prover instantiate command now allows “_” in the same way as the skolem command, allowing partial instantiation.
• - The prover copy command was a derived rule, and is now a primitive rule. This is to keep it from generating spurious TCCs.
• - The let-reduce? flag has been added to various strategies.
• - Various improvements have been made to the yices interface.
• - After struggling with making the bin files work with both case sensitive and case insensitive Lisps, we decided the simplest solution is to create separate bin files for each. Thus there is now a pvsbin subdirectory created for case sensitive Lisps (Allegro in this case), and PVSBIN for case-insensitive ones (CMU Lisp).

Incompatibilities

The bugs that have been fixed in 4.1 are mostly those reported since December 2002. Some of these fixes are to the judgement and TCC mechanism, so may have an impact on existing proofs. As usual, if it is not obvious why a proof is failing, it is often easiest to run it in parallel on an earlier version of PVS to see where it differs.

Some of the differences can be quite subtle, for example, one of the proofs that quit working used induct-and-simplify. There were two possible instantiations found in an underlying inst? command, and in version 3.0 one of these led to a nontrivial TCC, so the other was chosen. In version 4.1, a fix to the judgement mechanism meant that the TCC was no longer generated, resulting in a different instantiation. In this case the proof was repaired using :if-match all.

Most of the other incompatibilities are more obvious, and the proofs are easily repaired. If you have difficulties understanding why a proof has failed, or want help fixing it, send it to PVS bugs pvs-bugs@csl.sri.com.

This document was generated by Sam Owre on February 11, 2013 using texi2html 1.82.