PVS 5.0 Release Notes

PVS 5.0 is a significant new release of PVS. The highlights include an SBCL port, the incorporation of the PVSio, Manip, Field, and ProofLite packages from NASA, a new theory interpretation implementation, new judgement forms, new support for Yices, and several bug fixes.

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 one of the pre-built CMU or SBCL Lisp images.

Note that we are no longer providing PVS for Solaris or PowerPC on the download page, as we have limited funds and the vast majority of our users have Intel Macs or Linux machines. If you do need either of these, let us know at pvs-sri@csl.sri.com. We will be keeping earlier versions available for the foreseeable future.

It’s important to note that the .prf format has changed. While PVS 5.0 can easily read earlier proof files, the new format will confuse earlier versions of PVS. Please make copies of any directories that you want to also use earlier versions of PVS on. This is especially helpful when trying to repair proofs that work in earlier versions.

New Features

Available Lisp/Platforms

There are now 64-bit and 32-bit versions available for Intel Mac and Linux for Allegro (version 8.2) and SBCL Common Lisp. 32-bit versions are also available for CMU Common Lisp.

PVS Invocation

The pvs shell script has been modified to support SBCL Common Lisp. In addition, the load and eval capabilities have been simplified, where -l and -e are for Emacs files and expressions, and -L and -E are for Common Lisp files. There was an earlier -L flag, but it loaded the file before PVS initialization, which is more difficult to use.

PVSio Integration

César Muñoz has provided further improvements for PVSio, which is now more fully integrated into PVS. PVSio provides

• an alternative interface to the ground evaluator, making it easier to interact
• Several semantic attachments that facilitate programming in PVS
• A defattach macro, allowing users to add their own semantic attachments
• A pvsio script, allowing PVS specifications to be run as scripts
• Adds the eval, eval-expr, and eval-formula rules for use in the prover

PVSio now starts up without the need for loading extra library files. The sematic attachments are pre-installed, and the supporting theories are in the prelude. For more details on how to use PVSio, see the manual in doc/PVSio-2.d.pdf, (but ignore the installation instructions).

Manip and Field

The NASA Manip and Field packages have similarly been integrated, and improved by their authors. The Manip package provides many features, including Emacs extensions, many new proof strategies, and a pattern matching facility that allows reference to subterms during proof. For more details, see doc/manip-guide.pdf (but ignore the install instructions).

The Field package builds on Manip, and adds several prover commands making it easier to reason about nonlinear formulas. See doc/extrategies.pdf for details.

ProofLite

César Muñoz has also provided his ProofLite extension as part of PVS. This allows proofs to be included directly in PVS specifications and run from them, allowing for a literate programming style of specification. See doc/ProofLite-4.2.pdf for details.

Theory Interpretations

Theory interpretations have been significantly modified. Previously a theory declaration would generate a separate theory. This caused all kinds of problems, as it couldn’t reference any declarations from the referencing theory. In some cases this could be handled by splitting theories into pieces, but even this doesn’t always work.

In the new treatment, theory declarations are simply expanded in place, with the theory declaration id prepended to the included theory declarations. This solves the problem with declaration references, but introduces new issues. First, since the expanded theory declaration may itself have theory declarations, names have been extended to include any number of periods, e.g., th1.th2.th3.d. In general, these are only needed to disambiguate, and even then a suffix of the full name usually suffices.

The prettyprint-theory-instance is no longer meaningful, simply use M-x prettyprint-expanded to see the included declarations.

Expression Judgements

A new Judgement form is available. This is still in the experimental stage, but we welcome any feedback. The judgement has the form of a subtype judgement, but with a preceding FORALL that gives the types of the variables, as well as making the parsing unambiguous. Within the forall, any expression is allowed. For example,

 judgement forall (x: real) = x*x has_type nnreal
 f: [nnreal -> real]
 foo: formula forall (y: real):
   f(f((y - 100) * (y - 100)) * f((y - 100) * (y - 100))) = 2

Without the judgement, foo generates 2 TCCs; with the judgement, none are generated for foo, just the one for the judgement itself, which is much simpler to understand. Note that the judgement mechanism has to be fast, and not itself generate proof obligations, so the matches are purely syntactic. Thus ‘(x - 1) * (-1 + x)‘ will still generate a TCC.

Yices Enhancements

There are improvements to the yices and yices-with-rewrites rules. Note that to use these commands you must install Yices from yices.csl.sri.com, and make certain the directory containing the yices executable is in your PATH environment variable before invoking PVS.

PVS Libraries Speedbar

A simple Emacs speedbar extension is now available. This makes browsing libraries easier, as it lists all directories on the PVS_LIBRARY_PATH as well as the built-in libraries in the PVS lib subdirectory. This is invoked with M-x pvs-speedbar-browser, and clicking on a given library shows the specification files within; clicking on one of them brings it up in an Emacs buffer. In the future we plan to include declaration lists within the speedbar display.

Incompatibilities

The changes lead to some incompatibilities, primarily in the proofs. This is due to a number of factors:

• A bug was fixed in the lift-if rule that could potentially lead to unsoundness. The fix means that the rule is no longer as aggressive, so proofs may need to be repaired. This is especially true for proofs with sequences of lift-ifs.
• Some bugs were fixed in which TCCs were missing.
• In general, judgement processing has been improved. Though this is almost always better for new proofs, it does tend to cause older proofs to fail, because the proof trees differ.
• PVS 5.0 uses a new format for .prf files. The reason for this is to remove some information (such as the time the last run took) that causes version control systems to think there is a change, making it difficult to keep developments in sync.
• Any reliance on NASA libraries is obviously different now that the NASA extensions are integrated into PVS. In practice, this has been relatively painless.
• In addition to adding theories from the NASA extensions, a number of minor changes have been made to the prelude. Two notable ones are that choose no longer has a definition, and singleton is no longer a conversion by default. If you really want choose to be epsilon, there is an axiom for that. The singleton conversion is often used unexpectedly, especially when bitvectors are involved. If you want it, simply add a conversion+ singleton where needed. Remember it’s imported, so it can be placed in a theory low in the hierarchy; it doesn’t have to be added to every theory. The rest of the changes are only likely to be a problem if they accidentally introduce ambiguities. These are usually easily resolved.

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.